summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.cpp
AgeCommit message (Expand)Author
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. Than...Morgan Deters
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2013-10-07fixed some bugsLiana Hadarean
2013-05-08rm decision/relevancyKshitij Bansal
2013-05-07fix for nonterminating model-based array loopMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-11-26fixup for incremental solvingDejan Jovanović
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-14Fix a few minor issues in options processing, improving usability, consistenc...Morgan Deters
2012-09-08Some minor changes after reviewing the portfolio "unified driver" commit.Morgan Deters
2012-09-08Single driver for both sequential and portfolioKshitij Bansal
2012-07-31Options merge. This commit:Morgan Deters
2012-06-14This commit:Kshitij Bansal
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-06-07LogicInfo locking implemented, and some initialization-order issues in SmtEng...Morgan Deters
2012-05-09Merge from decision branch (ITE support)Kshitij Bansal
2012-04-30Added map from skolem variables to new ite formulas in ite removal.Clark Barrett
2012-04-25fix for de+lemmasKshitij Bansal
2012-04-23Merge from decision branch -- partially working justification heuristicKshitij Bansal
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-04-11merge from arrays-clark branchMorgan Deters
2012-03-26More cleaning up.Dejan Jovanović
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-25sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)Dejan Jovanović
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2012-02-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my...Morgan Deters
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic no...Tim King
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t...Morgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-08-17new implementation of lemmas on demandDejan Jovanović
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback