summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-07Fixing a bug with TheoryArith::ppAssert() and shared terms.Tim King
2012-05-07Fixes a sign bug in the DioSolver.Tim King
2012-05-04Guard for expensive Debug traceClark Barrett
2012-05-04options: fail if the debug or trace tag specified doesn't exist (-d -t)François Bobot
2012-05-04fix: getNumTraceTags, getNumDebugTagsFrançois Bobot
2012-05-04- This fixes a problem where simplex produced the same conflict in the single...Tim King
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-05-02Changing d_sharedTermsExist to logicInfo.isSharingEnabled()Clark Barrett
2012-04-30Added map from skolem variables to new ite formulas in ite removal.Clark Barrett
2012-04-28New LogicInfo functionality.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-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-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-06processing assertions in bit-vectors even when in fullcheck (needed for sharing)Dejan Jovanović
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-02- Merged in the branch cdlist-cleanup.Tim King
2012-04-02fix for cvc4_logic dumpKshitij Bansal
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback