summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-04-30uncompiling new bv to bool liftinglianah
2013-04-30finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-30more work on boolean liftingLiana Hadarean
2013-04-30started work on bv1 to boolean liftinglianah
2013-04-30added support for dumping the SAT problem the sat solver is working onlianah
2013-04-30updated the author namelianah
2013-04-30Add option in quantifiers for clause splittingAndrew Reynolds
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt...lianah
2013-04-30add decision_attributes.h for make distKshitij Bansal
2013-04-30Adding has bound counts and tracking for rows.Tim King
2013-04-29Some fixes for GCC 4.2, and for Java on MacMorgan Deters
2013-04-29Merge pull request #9 from kbansal/masterKshitij Bansal
2013-04-29Fixes to FCSimplex for some versions of compilersMorgan Deters
2013-04-28Fixing the failure for make distcheck.Tim King
2013-04-26Merge experimental decisionweight branchKshitij Bansal
2013-04-26FCSimplex branch mergeTim King
2013-04-25added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-25Add ability to run different regression levels with "make check"Morgan Deters
2013-04-23Theory "alternates" supportMorgan Deters
2013-04-22add bit0 and bit1 constants to smt-lib v1 parserMorgan Deters
2013-04-21added some bv rewrite ruleslianah
2013-04-18Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-04-18making sure sat context is zero when user context is popped to 0 in SmtEngine...lianah
2013-04-18fixing destruction order in SmtEnginelianah
2013-04-17bool flatten: node num_children workaroundKshitij Bansal
2013-04-17innd examples are solved fast, but destruction assertion faillianah
2013-04-17boolean flatten: bug fix in dfs searchKshitij Bansal
2013-04-16boolean flatten rewrite: dont re-rewriteKshitij Bansal
2013-04-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
2013-04-16fixed compile errorLiana Hadarean
2013-04-16uncompiling new bv to bool liftinglianah
2013-04-12finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-11Improved speed of no redundant lemma assertion by using hash setClark Barrett
2013-04-11Fixes for getModelVal in bv theoryClark Barrett
2013-04-11Added check for infinite lemma loopClark Barrett
2013-04-10fixed getModelValue to only query the value of leaves and evaluate more compl...lianah
2013-04-10more work on boolean liftingLiana Hadarean
2013-04-09started work on bv1 to boolean liftinglianah
2013-04-09Change TPTP parser to not use the STRING type; this necessary to repurpose st...Morgan Deters
2013-04-08added support for dumping the SAT problem the sat solver is working onlianah
2013-04-05Fix unit test (compile error) for new SatSolver interfaceMorgan Deters
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
2013-04-03Prerelease versioning for master.Morgan Deters
2013-04-03Pre-release versioningMorgan Deters
2013-04-03Cutting release 1.1.1.1Morgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
2013-04-03updated NEWS to include inequality solverLiana Hadarean
2013-04-03abort quantifiers check if master equality engine is inconsistent.Andrew Reynolds
2013-04-02Making arithmetic model reversion on unsat checks an option.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback