A dummy decision engine. Expected performance impact: none.
authorKshitij Bansal <kshitij@cs.nyu.edu>
Tue, 17 Apr 2012 17:20:37 +0000 (17:20 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Tue, 17 Apr 2012 17:20:37 +0000 (17:20 +0000)
commit7742c4211f765c2ba2637a211265c20789b861ee
tree05622a9df5dc2c900608b8e2ac5611d70e3208c6
parentccd77233892ace44fd4852999e66534d1c2283ea
A dummy decision engine. Expected performance impact: none.

Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.

Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
20 files changed:
src/Makefile.am
src/decision/Makefile [new file with mode: 0644]
src/decision/Makefile.am [new file with mode: 0644]
src/decision/decision_engine.cpp [new file with mode: 0644]
src/decision/decision_engine.h [new file with mode: 0644]
src/decision/decision_strategy.h [new file with mode: 0644]
src/decision/justification_heuristic.cpp [new file with mode: 0644]
src/decision/justification_heuristic.h [new file with mode: 0644]
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/sat_solver_types.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/arith/arith_priority_queue.h
src/theory/arith/simplex.cpp
src/theory/arith/simplex.h
src/util/options.cpp
src/util/options.h