projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9f74cfb) | patch
Merge from decision branch (ITE support)
authorKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 9 May 2012 05:45:36 +0000 (05:45 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 9 May 2012 05:45:36 +0000 (05:45 +0000)
commit6243fba11e0189891acf21de3c6daa072b038e13
tree8265abfa3e583831a972acdf97989930ae9c3592tree
parent9f74cfbd847663f80c362cf06bda7e749f0f694bcommit | diff
Merge from decision branch (ITE support)

Major changes from last merge
* ITEs supported
* Don't share theory lemmas to DE, only assertions

Should probably be noted that 'make regress' doesn't quite
pass with --decision=justification. Throws off search in couple
of arith benchmarks.

No serious performance changes expected. Keep an eye.
src/decision/decision_engine.cpp diff | blob | history
src/decision/decision_engine.h diff | blob | history
src/decision/decision_strategy.h diff | blob | history
src/decision/justification_heuristic.cpp diff | blob | history
src/decision/justification_heuristic.h diff | blob | history
src/prop/minisat/core/Solver.cc diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/ite_removal.h diff | blob | history