summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-04-28New LogicInfo functionality.Morgan Deters
2012-04-28require boost library (but not the threading support---that's only necessary ...Morgan Deters
2012-04-28undo, againMorgan Deters
2012-04-28adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration m...Morgan Deters
2012-04-27undo previous commit (as it will break a number of things without additional ...Morgan Deters
2012-04-27adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration m...Morgan Deters
2012-04-27fix parser logic-handling oversights: QF_UFBV should now be supportedMorgan Deters
2012-04-27break dependence on zlib-dev for nowMorgan Deters
2012-04-27Fixed warning in decision_engine.h, minor tweak to caregraph function inClark Barrett
2012-04-27This merges in the branch cvc4/branches/arithmetic/matrix into trunk.Tim King
2012-04-25portfolio driver: respect parseOnly optionKshitij Bansal
2012-04-25fix for de+lemmasKshitij Bansal
2012-04-24This commit merges in the branch branches/arithmetic/congruence into trunk. H...Tim King
2012-04-23Merge from decision branch -- partially working justification heuristicKshitij Bansal
2012-04-20Updates to array theory - much more lazy about introduction of readsClark Barrett
2012-04-19In the constructor of DecisionEngine, there were 2 pointers that were assumed...Tim King
2012-04-18add the missing BINARY variable in some test/regress makefilesKshitij Bansal
2012-04-18cout -> warning. Happening in portfolioKshitij Bansal
2012-04-18disabling the problematic pragma in node_manager.h on gcc < 4.6 until we figu...Dejan Jovanović
2012-04-17Fix for thos annoying "array index" warnings in production buildsDejan Jovanović
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-14Fixed bug in sharing with arrays of different typesClark Barrett
2012-04-13Fix SExpr name qualification for swig, and #include integer and rational head...Morgan Deters
2012-04-12svn ignore Makefile.in for aufbv regression directoryMorgan Deters
2012-04-12Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds,...Tim King
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06* Smt2 printer for datatypesFrançois Bobot
2012-04-06* Fix ITEs and functions in CVC language printer.Morgan Deters
2012-04-06fix distributed builds (and therefore the Debian nightly build) by ignoring M...Morgan Deters
2012-04-06processing assertions in bit-vectors even when in fullcheck (needed for sharing)Dejan Jovanović
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-04-04some settings in bvminisatDejan Jovanović
2012-04-04changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=...Liana Hadarean
2012-04-04changed ccmin_mode in BvMinisatLiana Hadarean
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-04-03Fix for make dist.Tim King
2012-04-02Fix for broken unit tests from the previous commit.Tim King
2012-04-02- Merged in the branch cdlist-cleanup.Tim King
2012-04-02fix for cvc4_logic dumpKshitij Bansal
2012-04-02Removing large and unused regress2 benchmarks to decrease the size of checkouts.Tim King
2012-03-30some more build system fixesDejan Jovanović
2012-03-30fixing some build systme warningsDejan Jovanović
2012-03-29Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers...Tim King
2012-03-29Fixes a linking problem with the new SatSolverConstructor on Mac.Tim King
2012-03-29bringing cryptominisat into the main branchDejan Jovanović
2012-03-28enabling the --disable-arithmetic-propagation option in the arithmetic code (...Dejan Jovanović
2012-03-28fix swig-ignored interface name; hopefully fixes Debian package nightly buildsMorgan Deters
2012-03-28Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AG...Tim King
2012-03-28Some renaming and refactoring in SATDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback