cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2012-06-14	This commit:	Kshitij Bansal
	* enables decision heuristic (justification) for QF_BV and QF_AUFBV * disables a failing regression in aufbv (because of equality engine assert failure trigerred by above change) * moves around the init procedure smt_engine * destruction time issues because of moving this -- still to be fixed, currently get around by not destucting stuff in driver
2012-06-13	Make d_result in DE context dependent	Kshitij Bansal
	(fixes bugs in bv, others with JH on)
2012-06-08	Merge from decision branch (till r3663)	Kshitij Bansal
	(no performace or search behavior changes expected)
2012-05-13	fixing build warnings	Dejan Jovanović

2012-05-09	Merge from decision branch (ITE support)	Kshitij Bansal
	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.
2012-04-27	Fixed warning in decision_engine.h, minor tweak to caregraph function in	Clark Barrett
	arrays, fixed bug with equalities between constants in shared terms database
2012-04-23	Merge from decision branch -- partially working justification heuristic	Kshitij Bansal
	Overview of changes * command line option --decision={internal,justification} * justification heuristic handles all operators except ITEs revelant stats: decision::jh::* * if decisionEngine has solved the problem PropEngine returns unknown and smtEngine queries DE to get the answer relevant stat: smt::resultSource * there are known bugs Full list of commits being merged r3330 use CD data structures in JH r3329 add command-line option --decision=MODE r3328 timer stat, other fixes r3326 more trace r3325 enable implies, iff, xor (no further regression losses) r3324 feed decision engine lemmas, changes to quitting mechanism r3322 In progress r3321 more fixes... r3318 bugfix1 (69 more to go) r3317 Handle other boolean operators in JH (except ITE) r3316 mechanism for DE to stopSearch r3315 merge from trunk + JH translation continuation r3275 change option to enable JH by default[A
2012-04-17	A dummy decision engine. Expected performance impact: none.	Kshitij Bansal
	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