Theory solver calls
Florian Corzilius
I ran a small example. The output might be interesting for everyone
embedding a theory solver into OpenSMT. There are also a few things I
do not understand.
The example is:
..
(declare-fun a () Real)
(declare-fun b () Real)
(assert (and (or (= (+ (* a a) 2) 4) (= (* b b) 3)) (or (= (* a a) 2)
(= (* b b) 3))))
(check-sat)
and OpenSMT acts as follows: (I wrote some comments behind the output)
call: belongsToT
end: belongsToT
call: inform (= (+ (* a a) 2) 4)
end: inform
call: belongsToT
end: belongsToT
call: inform (= (* b b) 3)
end: inform
call: belongsToT
end: belongsToT
call: inform (= (* a a) 2)
end: inform
call: check
Try: isConsistent( ) //I do not understand, why calling
check before any constraint is asserted.
-> True.
end: check
call: pushBacktrackPoint
end: pushBacktrackPoint
call: assertLit (= (+ (* a a) 2) 4)
polarity is True
add to theory solver: -2+a^2=0
end: assertLit
call: pushBacktrackPoint
end: pushBacktrackPoint
call: assertLit (= (* a a) 2)
polarity is True
add to theory solver: -2+a^2=0
end: assertLit
call: pushBacktrackPoint
end: pushBacktrackPoint
call: assertLit (= (* b b) 3)
polarity is True
add to theory solver: -3+b^2=0 //I do not understand, why this
constraint gets asserted.
end: assertLit
call: check
Try: isConsistent( -2+a^2=0 and -2+a^2=0 and -3+b^2=0 )
-> True.
end: check
call: popBacktrackPoint
end: popBacktrackPoint
call: popBacktrackPoint
end: popBacktrackPoint
call: popBacktrackPoint
end: popBacktrackPoint
sat
My explanation: OpenSMT considers the Boolean skeleton (A or B) and
(A' or B) and checks the assignment A=A'=B=True. I expected, according
DPLL, that it first checks, let's say, A followed by A' or even better
just B.
BTW: Does OpenSMT see, that (= (+ (* a a) 2) 4) is the same as (= (* a
a) 2) and abstract them to one Boolean variable?
Regards,
Florian
Roberto Bruttomesso
consistency is always checked initially as some theory atoms might be
forced since the very beginning. In your case this does not happen and
check is indeed useless
> end: check
> call: pushBacktrackPoint
> end: pushBacktrackPoint
> call: assertLit (= (+ (* a a) 2) 4)
> polarity is True
> add to theory solver: -2+a^2=0
> end: assertLit
> call: pushBacktrackPoint
> end: pushBacktrackPoint
> call: assertLit (= (* a a) 2)
> polarity is True
> add to theory solver: -2+a^2=0
> end: assertLit
> call: pushBacktrackPoint
> end: pushBacktrackPoint
> call: assertLit (= (* b b) 3)
> polarity is True
> add to theory solver: -3+b^2=0 //I do not understand, why this
> constraint gets asserted.
this is due to a heuristic inside OpenSMT: it first tries to see if
there is a Boolean model of the problem. So initially pushes
everything that leads to a satisfiable Boolean model. That's why you
get everything asserted. That behaviour could be disabled by setting
to false the parameter first_boolean_model somewhere in
src/smtsolvers/CoreSMTSolver.C before search is called
> end: assertLit
> call: check
> Try: isConsistent( -2+a^2=0 and -2+a^2=0 and -3+b^2=0 )
> -> True.
> end: check
> call: popBacktrackPoint
> end: popBacktrackPoint
> call: popBacktrackPoint
> end: popBacktrackPoint
> call: popBacktrackPoint
> end: popBacktrackPoint
> sat
>
> My explanation: OpenSMT considers the Boolean skeleton (A or B) and
> (A' or B) and checks the assignment A=A'=B=True. I expected, according
> DPLL, that it first checks, let's say, A followed by A' or even better
> just B.
that's true for old-fashioned DPLL, moder solvers privilege Boolean
Constraint Propagation, so things are a bit different. In general you
don't get that specific behavior, but one according to BCP, Decide,
and Theory Propagation mechanisms
>
> BTW: Does OpenSMT see, that (= (+ (* a a) 2) 4) is the same as (= (* a
> a) 2) and abstract them to one Boolean variable?
no it does not. There is no way OpenSMT data-structures can guess that
two syntactically different atoms are semantically equivalent (apart
from some simple cases like 1 + 2 which is simplified as 3). So you
have to do this simplification "manually" and as a preprocessing step.
I strongly recommend you to do so. For standard OpenSMT this happens
by means of class LAExpression in LA.C, which normalizes polynomes as
a_1 x_1 + a_2 x_2 + ... + a_n x_n. You should do something similar for
non-linear arithmetic, in such a way that syntactically equivalent
expressions correspond (as much as possible) to semantically
equivalent ones. You can try to modify the functions in LA.C to adapt
them to your normal form.
Cheers,
Roberto
>
> Regards,
>
> Florian
>
> --
> 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
Florian Corzilius
I hoped that such a parameter as first_boolean_model exists. I also
think that a preprocessing, which normalizes the constraints, impacts
the performance a lot, since it decreases the number of later theory
calls.
Thanks for your comments.
Regards,
Florian
On Jun 27, 7:58 pm, Roberto Bruttomesso