Re: OpenSMT and its IDL implementation

[Roberto Bruttomesso]

Hello,

first of all thank you for your interest in OpenSMT. I think that the
assertion triggers because we use internally a special node, call it
"zero" node, which should be used to transform atoms of the form

s_0 <= 0

into

s_0 - zero <=0

to keep the problem into the form

x - y <= c

Now, if I remember correclty, we use "NULL" to mean the node "zero"
... that's why you get that bad assertion I guess

and yes, the values may be shifted because they have to be
"normalized" with the value of "zero"

I do not work any longer on OpenSMT and so I have left behind bugs
that I cannot fix, but I also left behind some slides here

http://www.oprover.org/roberto/teaching/smt/

if you are interested you can have a look at them, especially lecture 9

Regards,
Roberto

On Tue, Oct 23, 2012 at 6:35 PM, Joan Espasa <cat.os....@gmail.com> wrote:
> Hi Roberto!
>
> I'm a student tinkering with OpenSMT. I'm writing this post as I am
> interested in the IDL implementation, but I'm facing some problems. when I
> use OpenSMT to execute some trivial instances, give strange results or it
> segfaults. I understand that the solver was aimed at knowing if a valid
> model exist, and thus most of the effort was at finding efficiently if a
> solution exist or not. As the code names you as the main author of the IDL
> solver, I hope you can shed some light in this matter. First at all, excuse
> me if I'm doing or talking nonsense, as I'm still a newborn in this topics.
>
> I am trying to get consistent models from the IDL t-solver. I found this
> thread: (
> https://groups.google.com/forum/?fromgroups=#!topic/opensmt/o1S3lbgv1rE )
> where I got the get-value implementation too, and simplified the presented
> problem a bit:
>
> -------------------------------------- %<
> --------------------------------------
> (set-logic QF_IDL)
> (set-info :smt-lib-version 2.0)
> (set-option :produce-models true)
> (declare-fun s_0 () Int)
> (declare-fun s_1 () Int)
> (assert (and
> (or (= s_0 0) (= s_0 1))
> (or (= s_1 0) (= s_1 1))
> (> s_1 s_0)
> ))
> (check-sat)
> (get-value (s_0 s_1))
> (exit)
> -------------------------------------- %<
> --------------------------------------
>
> I've activated the "dump_formula" in the config file, and thus when
> OpenSMTContext::staticCheckSAT is called, it dumps for me the pre and
> post-processed file. As the logic is IDL, some constraints are transformed
> to an IDL form, granting a (seems to me) correct "presolve.smt2".
>
> Then, after the (check-sat) I know that the method
> DLSolver<T>::computeModel( ) is called, so I think I can assume that
> internally the DLSolver should has a consistent state. From this problem in
> particular, I get a correct SAT response, so now I know that a model exists.
> Regarding the other thread, I've traced the problem with bad values to the
> IDL graph itself. As any solution to a set of DL literals can be shifted, I
> think that this could be the problem in that case.
>
> Anyway, when I'm trying to get the values from the problem, it gives strange
> results, so I tried to dump the graph using some already provided methods,
> but it segfaults if I compile without asserts. I'm calling the method
> DLGraph<T>::printDeducedAsDotty() to a file, and added some couts there to
> try to debug, but it fails in the following way:
>
> -------------------------------------- %<
> --------------------------------------
> $ : opensmt_build_trunk/build/opensmt --config=config_verbose.cnf
> smt2/reified_example.smt2
> # Warning: pedantic assertion checking enabled (very slow)
> # Warning: this binary is compiled with optimizations disabled (slow)
> [Dumped original.smt2]
> [Dumped presolve.smt2]
> Heavy Edges size: 0
> adjList id: 0 size:2
> s_0 --[-1]--> s_1
> s_0 --[1]--> opensmt: ../../../src/egraph/Enode.h:330: std::ostream&
> operator<<(std::ostream&, Enode*): Assertion `e' failed.
> Aborted
> $ :
> -------------------------------------- %<
> --------------------------------------
>
> For this output, it seems that when its printing the adjacency list, one
> edge is pointing to an invalid vertex? Am I making some conceptual mistake?
>
> Many thanks for your time, patience and source code :)
>
> Joan
>
> --
> You received this message because you are subscribed to the Google Groups
> "opensmt" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/opensmt/-/UN4d6hwIJ3EJ.
> 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