Smaller and greater
flocor
I'm trying to run OpenSMT with my Solver for QF_NRA. If the input
formula contains a constraint with the relation "<" or ">" OpenSMT
convertes it to ">=" resp. "<=". Maybe it inverts these constraints,
but nevertheless the result gets faulty.
The following example should be UNSAT:
(set-logic QF_NRA)
(set-info :source |
Harald Roman Zankl <Harald...@uibk.ac.at>
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= a 2))
(assert (= (* b b) 2))
(assert (> b a))
(check-sat)
(exit)
This is how OpenSMT processes this input:
>call: belongsToT
>end: belongsToT
>call: inform (<= b a)
>end: inform
>call: belongsToT
>end: belongsToT
>call: inform (= 2 (* b b))
>end: inform
>call: belongsToT
>end: belongsToT
>call: inform (= a 2)
>end: inform
>call: pushBacktrackPoint
>end: pushBacktrackPoint
>call: assertLit (<= b a)
>*** addConstraint: -b+a>=0
>end: assertLit
>call: pushBacktrackPoint
>end: pushBacktrackPoint
>call: assertLit (= 2 (* b b))
>*** addConstraint: -2+b^2=0
>end: assertLit
>call: pushBacktrackPoint
>end: pushBacktrackPoint
>call: assertLit (= a 2)
>*** addConstraint: -2+a=0
>end: assertLit
>call: check
>*** Try: isConsistent( -b+a>=0 and -2+b^2=0 and -2+a=0 );
>*** True.
>end: check
>call: check
>*** Try: isConsistent( -b+a>=0 and -2+b^2=0 and -2+a=0 );
>*** True.
>end: check
>call: popBacktrackPoint
>end: popBacktrackPoint
>call: popBacktrackPoint
>end: popBacktrackPoint
>call: popBacktrackPoint
>end: popBacktrackPoint
>
>sat
Greetz,
Florian
Aliaksei Tsitovich
Could you please provide more details on your implementation of QF_NRA
solver. In particular, how it make use of other solvers and/or
preprocessing calls?
Kind regards,
Aliaksei
> --
> You received this message because you are subscribed to the Google Groups "opensmt" group.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to opensmt+u...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.
>
>
Roberto Bruttomesso
yes OpenSMT converts all into <=, following these rewrites
(>= a b) --> (<= b a)
(< a b) --> (not (<= b a))
(> a b) --> (not (<= a b))
what I see from the trace is not necessarily incorrect because
polarity is not taken into account. OpenSMT always communicates
"positive" constraints, i.e., will never communicate (not (<= b a)).
The polarity information is stored in enode::getPolarity( ) method,
which could be l_True (positive) or l_False (negative). So this call
>>call: assertLit (<= b a)
may actually mean
>>call: assertLit (not (<= b a))
If "e" is an enode, try to use the following printout for assertLit
cerr << ( e->getPolarity( ) == l_True ? " " : "not " ) << e << endl;
and you should see that maybe that constraint was actually pushed negatively
I hope I have spotted the bug, if not let me know
Cheers,
Roberto
On Fri, Jun 24, 2011 at 1:11 PM, flocor <corz...@cs.rwth-aachen.de> wrote:
> --
> You received this message because you are subscribed to the Google Groups "opensmt" group.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to opensmt+u...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.
>
>
--
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70
flocor
there is just my implementation of the virtual substitution method as
back end.
Greetz,
Florian
On Jun 24, 2:26 pm, Aliaksei Tsitovich <aliaksei.tsitov...@gmail.com>
wrote:
> Could you please provide more details on your implementation of QF_NRA
> solver. In particular, how it make use of other solvers and/or
> preprocessing calls?
>
> Kind regards,
> Aliaksei
>
>
>
>
>
>
>
> On Fri, Jun 24, 2011 at 1:11 PM, flocor <corzil...@cs.rwth-aachen.de> wrote:
> > Hello,
>
> > I'm trying to run OpenSMT with my Solver for QF_NRA. If the input
> > formula contains a constraint with the relation "<" or ">" OpenSMT
> > convertes it to ">=" resp. "<=". Maybe it inverts these constraints,
> > but nevertheless the result gets faulty.
>
> > The following example should be UNSAT:
>
> > (set-logic QF_NRA)
> > (set-info :source |
flocor
thank you for the amazingly fast response. As I understand, it means,
that I have to invert constraints with negative polarity before adding
them to the set of constraints, whose consistency I check for. I'll
try this.
I'm currently running the "--disable-optimization" configuration.
There are some examples, which I can run bugfree, but instead of the
OpenSMT-output "sat" or "unsat" it communicates "error". Shall I try
the "--enable-pedantic_debug" configuration or do you already have an
idea?
Cheers,
Florian
On Jun 24, 2:32 pm, Roberto Bruttomesso
Aliaksei Tsitovich
I'm currently running the "--disable-optimization" configuration.
There are some examples, which I can run bugfree, but instead of the
OpenSMT-output "sat" or "unsat" it communicates "error". Shall I try
the "--enable-pedantic_debug" configuration or do you already have an
idea?
Roberto Bruttomesso
> Hello Roberto,
>
> thank you for the amazingly fast response. As I understand, it means,
> that I have to invert constraints with negative polarity before adding
> them to the set of constraints, whose consistency I check for. I'll
> try this.
correct
>
> I'm currently running the "--disable-optimization" configuration.
> There are some examples, which I can run bugfree, but instead of the
> OpenSMT-output "sat" or "unsat" it communicates "error". Shall I try
> the "--enable-pedantic_debug" configuration or do you already have an
> idea?
I don't think that pedantic_debug will help here. Just to add a bit
more to what Aliaksei said, if OpenSMT answers "error" it is because
1) the benchmark contains the :status flag (e.g., (set-info :status sat))
2) the final "internal" answer of OpenSMT is the opposite (e.g., unsat)
therefore instead of returning the wrong answer it just says "error".
You can see this by removing the flag from the benchmark
I think that once you fix your solver, which I assume is still unsound
given that you do not consider correct polarities, than it will
hopefully agree with set-status flag
Cheers,
R
> For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.
flocor
once again: thank you! It is exactly the answer I liked to hear :) I
just started to work with SMT-lib, so maybe I should start reading the
tutorial more carefully.
Have a nice weekend!
Florian
On Jun 24, 6:34 pm, Aliaksei Tsitovich <aliaksei.tsitov...@gmail.com>
wrote: