| 2012-05-15 |
Liana Hadarean | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaste... |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | removing all extended commands (as inspired by the... |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Fix QF_AUFLIA (resolves bug #331). |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | fixing warnings, grr |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | several bug fixes: in TheoryBV::NotifyClass missing... |
commit | commitdiff | tree |
| 2012-05-14 |
Dejan Jovanović | fixes for shared term registration. previously the... |
commit | commitdiff | tree |
| 2012-05-14 |
Clark Barrett | Fixed assertion failures in array theory |
commit | commitdiff | tree |
| 2012-05-14 |
Morgan Deters | in debug builds, -d can be used for trace tags that... |
commit | commitdiff | tree |
| 2012-05-14 |
Dejan Jovanović | fixing up preregistration again |
commit | commitdiff | tree |
| 2012-05-13 |
Dejan Jovanović | fixing build warnings |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix regex in Debug_tags and Trace_tags generation for... |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix typo in sed line |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | output a warning message when a function type (or datat... |
commit | commitdiff | tree |
| 2012-05-11 |
Clark Barrett | Disabled arith-rewrite-equalities by default unless... |
commit | commitdiff | tree |
| 2012-05-11 |
Clark Barrett | Added some ITE rewrites, |
commit | commitdiff | tree |
| 2012-05-11 |
Tim King | Partially fixes something-like-a-problem with TheoryAri... |
commit | commitdiff | tree |
| 2012-05-10 |
Tim King | Removing now unneeded (as of r3425) typenames from... |
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | fix an issue which breaks language bindings (so this... |
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | --disable-tracing at configure time now disables Trace... |
commit | commitdiff | tree |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
commit | commitdiff | tree |
| 2012-05-09 |
Kshitij Bansal | rm something for a future merge that sneaked in |
commit | commitdiff | tree |
| 2012-05-09 |
Kshitij Bansal | Merge from decision branch (ITE support) |
commit | commitdiff | tree |
| 2012-05-09 |
Dejan Jovanović | Fixing the debug tags generation and related methods... |
commit | commitdiff | tree |
| 2012-05-08 |
Liana Hadarean | Merging in bvprop branch, with proper bit-vector propag... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixing a bug with TheoryArith::ppAssert() and shared... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixes a sign bug in the DioSolver. |
commit | commitdiff | tree |
| 2012-05-04 |
Clark Barrett | Guard for expensive Debug trace |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | options: fail if the debug or trace tag specified doesn... |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | fix: getNumTraceTags, getNumDebugTags |
commit | commitdiff | tree |
| 2012-05-04 |
Tim King | - This fixes a problem where simplex produced the same... |
commit | commitdiff | tree |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
commit | commitdiff | tree |
| 2012-05-02 |
Clark Barrett | Changing d_sharedTermsExist to logicInfo.isSharingEnabled() |
commit | commitdiff | tree |
| 2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | New LogicInfo functionality. |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | require boost library (but not the threading support... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | undo, again |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | undo previous commit (as it will break a number of... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | fix parser logic-handling oversights: QF_UFBV should... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | break dependence on zlib-dev for now |
commit | commitdiff | tree |
| 2012-04-27 |
Clark Barrett | Fixed warning in decision_engine.h, minor tweak to... |
commit | commitdiff | tree |
| 2012-04-27 |
Tim King | This merges in the branch cvc4/branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | portfolio driver: respect parseOnly option |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | fix for de+lemmas |
commit | commitdiff | tree |
| 2012-04-24 |
Tim King | This commit merges in the branch branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-23 |
Kshitij Bansal | Merge from decision branch -- partially working justifi... |
commit | commitdiff | tree |
| 2012-04-20 |
Clark Barrett | Updates to array theory - much more lazy about introduc... |
commit | commitdiff | tree |
| 2012-04-19 |
Tim King | In the constructor of DecisionEngine, there were 2... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | add the missing BINARY variable in some test/regress... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | cout -> warning. Happening in portfolio |
commit | commitdiff | tree |
| 2012-04-18 |
Dejan Jovanović | disabling the problematic pragma in node_manager.h... |
commit | commitdiff | tree |
| 2012-04-17 |
Dejan Jovanović | Fix for thos annoying "array index" warnings in product... |
commit | commitdiff | tree |
| 2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
commit | commitdiff | tree |
| 2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
commit | commitdiff | tree |
| 2012-04-14 |
Clark Barrett | Fixed bug in sharing with arrays of different types |
commit | commitdiff | tree |
| 2012-04-13 |
Morgan Deters | Fix SExpr name qualification for swig, and #include... |
commit | commitdiff | tree |
| 2012-04-12 |
Morgan Deters | svn ignore Makefile.in for aufbv regression directory |
commit | commitdiff | tree |
| 2012-04-12 |
Tim King | Adds an operator<< to SExpr::SexprTypes. This fixes... |
commit | commitdiff | tree |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
commit | commitdiff | tree |
| 2012-04-06 |
François Bobot | * Smt2 printer for datatypes |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | fix distributed builds (and therefore the Debian nightl... |
commit | commitdiff | tree |
| 2012-04-06 |
Dejan Jovanović | processing assertions in bit-vectors even when in fullc... |
commit | commitdiff | tree |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions... |
commit | commitdiff | tree |
| 2012-04-04 |
Dejan Jovanović | some settings in bvminisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed BVMinisat options to use cc_min=0 in propagate... |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed ccmin_mode in BvMinisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
commit | commitdiff | tree |
| 2012-04-03 |
Tim King | Fix for make dist. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Fix for broken unit tests from the previous commit. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | - Merged in the branch cdlist-cleanup. |
commit | commitdiff | tree |
| 2012-04-02 |
Kshitij Bansal | fix for cvc4_logic dump |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Removing large and unused regress2 benchmarks to decrea... |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | some more build system fixes |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | fixing some build systme warnings |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is... |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fixes a linking problem with the new SatSolverConstruct... |
commit | commitdiff | tree |
| 2012-03-29 |
Dejan Jovanović | bringing cryptominisat into the main branch |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | enabling the --disable-arithmetic-propagation option... |
commit | commitdiff | tree |
| 2012-03-28 |
Morgan Deters | fix swig-ignored interface name; hopefully fixes Debian... |
commit | commitdiff | tree |
| 2012-03-28 |
Tim King | Update to the ArithRewriter to remove REWRITE_AGAIN_FUL... |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | Some renaming and refactoring in SAT |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | getting rid of a rewrite in uf sharing, speeds things... |
commit | commitdiff | tree |
| 2012-03-28 |
Liana Hadarean | fixed faulty bv rewrite rule |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | adding an extra cache check in the rewriter, speeds... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | Global registry of SAT solvers, where they are register... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | More cleaning up. |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | more datail from the build failure |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | with a small fix |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | forgot to commit this one, fixing build errors |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | moving minisat implementation into their respective... |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat_module.h,cpp -> sat_solver.h,cpp (as intended) |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) |
commit | commitdiff | tree |
| 2012-03-24 |
Dejan Jovanović | a cute script to make a video of development from the... |
commit | commitdiff | tree |
| 2012-03-23 |
Tim King | Removed the variableRemovalEnabled option and d_removed... |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | * improving arithmetic getEqualityStatus |
commit | commitdiff | tree |
| 2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface |
commit | commitdiff | tree |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog