Re: About an opensmt question

[Roberto Bruttomesso]

Hello,

I think that what you write makes sense

Roberto

On Wed, Sep 12, 2012 at 4:22 PM, Alex <alex.jo...@gmail.com> wrote:
> Hello,
> I want to replace Minisat with other incomplete SAT algorithm in
> opensmt.Here is my thoughts:
> Firstly,we will set the value of all the vars (it may be sat on the SAT
> layer).
> Secondly,we invoke the checktheory(true) function to check the
> consistency in Tsolvers by changing the code in assertLits():
> e->setPolarity( (x(v)==0 ? l_False : l_True)
> );////it will pass the value of Vars to E-nodes
> Thirdly,if checktheory() returns 1,it mean t-solvers sat,otherwise returns 0
> if unsat.
> but i dont know whether my thoughts is right?
>
>
> --
> 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/-/rW52NvEWLWQJ.
> 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

[Alex]

Hi,Roberto

    will it invoke T-solvers correctly?

Roberto於 2012年9月12日星期三UTC+8下午10時42分58秒寫道：

[Roberto Bruttomesso]

It depends, you have to tell the Tsolvers which atoms to process, not
only their polarity. See code in THandler::assertLit for that

Roberto

> https://groups.google.com/d/msg/opensmt/-/V6Ddq-6ZUvYJ.

[johns alex]

Yes, I get all Vars from original opensmt, and tell the Tsolvers that the e-node relatively the var to process by using the statement "res = core_solver.assertLit( e );" in the THandler::assertLits.

But I confused about a instance of UF:

  if the program just ran one time,the result correct(it show unsat in T-solver).

 if it ran circularly (it will invoke checktheory constantly),the result wrong(it show true) under the same value of Vars that show unsat just one time.

I must miss something.I could show the code in my program if you need.

Thanks for helping.

2012/9/12 Roberto Bruttomesso <roberto.b...@gmail.com>

[Roberto Bruttomesso]

maybe an easier thing to do is to push literals on the minisat
"trail", and let THandler::assertLit handle the call to Tsolvers
directly

R

[johns alex]

Hi,Roberto,

   Thank you for your advice.Your writing helps me a lot!

2012/9/14 Roberto Bruttomesso <roberto.b...@gmail.com>