projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Reverting rewrite rule to working version
2012-06-15 Clark BarrettReverting rewrite rule to working version
 commit | commitdiff | tree
2012-06-15 Clark BarrettFixes some assertion failures
 commit | commitdiff | tree
2012-06-15 Clark BarrettFix for incompleteness bug with decision engine: repeated...
commit | commitdiff | tree
2012-06-14 Clark BarrettNew substitutions implementation - fixes performance...
commit | commitdiff | tree
2012-06-14 Clark BarrettRemoved an assertion, unneeded header file
 commit | commitdiff | tree
2012-06-13 Clark BarrettFixed failing assertion when EqualityEngine is in conflict
 commit | commitdiff | tree
2012-06-13 Clark BarrettFixed definition of bvsmod
 commit | commitdiff | tree
2012-06-13 Clark BarrettFixes more problems in bv rewrites
 commit | commitdiff | tree
2012-06-13 Clark BarrettFixes lots of problems in bv rewrite rules and adds...
commit | commitdiff | tree
2012-06-12 Clark BarrettMoved some things around in the preprocessor. Now...
commit | commitdiff | tree
2012-06-12 Clark BarrettFixed fuzzing bug
 commit | commitdiff | tree
2012-06-12 Clark BarrettChanged bitvector theory rewriter so that equalities...
commit | commitdiff | tree
2012-06-12 Clark BarrettFixed bug causing QF_LIA/solver_cvc4/incorrect1.smt...
commit | commitdiff | tree
2012-06-12 Clark BarrettFixed failing assertion in arrays for bug 347
 commit | commitdiff | tree
2012-06-12 Clark BarrettFixed compile error
 commit | commitdiff | tree
2012-06-12 Clark BarrettEnabling constant propagation
 commit | commitdiff | tree
2012-06-12 Clark BarrettAdding constant propagation code - needs more testing...
commit | commitdiff | tree
2012-06-11 Clark BarrettOK, now the rewrite issues are fixed
 commit | commitdiff | tree
2012-06-11 Clark BarrettFix for array bug with decision heuristic
 commit | commitdiff | tree
2012-06-11 Clark BarrettFixed bug 352
 commit | commitdiff | tree
2012-06-10 Clark BarrettFixed one more bug in rewriter
 commit | commitdiff | tree
2012-06-10 Clark BarrettAdded a very fruitful assertion to the rewriter: checks...
commit | commitdiff | tree
2012-06-09 Clark BarrettTurning on unconstrained simp for QF_AUFBV
 commit | commitdiff | tree
2012-06-07 Clark BarrettFixed performance issue with ite_simplifier on some...
commit | commitdiff | tree
2012-06-07 Clark BarrettAdded small test case for diseq propagation
 commit | commitdiff | tree
2012-06-06 Clark BarrettDon't ever call nonclausalSimplify if simplificationMode...
commit | commitdiff | tree
2012-06-06 Clark BarrettFixed assertion failures
 commit | commitdiff | tree
2012-06-06 Clark BarrettFixed broken test case, removed one that is a mistake
 commit | commitdiff | tree
2012-06-06 Clark BarrettFixed problem causing crash at destruction time
 commit | commitdiff | tree
2012-06-05 Clark BarrettMore clean-up
 commit | commitdiff | tree
2012-06-05 Clark BarrettFixed a performance issue with unconstrained simplifier
 commit | commitdiff | tree
2012-06-05 Clark BarrettAdding missing files...
 commit | commitdiff | tree
2012-06-04 Clark BarrettAdded preprocessing pass that propagates unconstrained...
commit | commitdiff | tree
2012-05-31 Clark BarrettFixed bug in bv: one more case where non-shared equality...
commit | commitdiff | tree
2012-05-30 Clark BarrettAdded BitwiseEq bitvector rewrite
 commit | commitdiff | tree
2012-05-30 Clark BarrettFixed problem with array queue growing too large
 commit | commitdiff | tree
2012-05-29 Clark BarrettEnabled SolveEq bv rewrite
 commit | commitdiff | tree
2012-05-28 Clark BarrettAdded some BV rewrites, fixed bugs in array theory...
commit | commitdiff | tree
2012-05-27 Clark BarrettAnother expensive function call in a Debug trace
 commit | commitdiff | tree
2012-05-27 Clark BarrettAnother expensive function call in a Debug line
 commit | commitdiff | tree
2012-05-25 Clark BarrettChecking in fix for bug 340 - somehow didn't get checked...
commit | commitdiff | tree
2012-05-15 Clark BarrettFixed several bugs in shared terms database
 commit | commitdiff | tree
2012-05-14 Clark BarrettFixed assertion failures in array theory
 commit | commitdiff | tree
2012-05-11 Clark BarrettDisabled arith-rewrite-equalities by default unless...
commit | commitdiff | tree
2012-05-11 Clark BarrettAdded some ITE rewrites,
 commit | commitdiff | tree
2012-05-04 Clark BarrettGuard for expensive Debug trace
 commit | commitdiff | tree
2012-05-02 Clark BarrettChanging d_sharedTermsExist to logicInfo.isSharingEnabled()
 commit | commitdiff | tree
2012-04-30 Clark BarrettAdded map from skolem variables to new ite formulas...
commit | commitdiff | tree
2012-04-27 Clark BarrettFixed warning in decision_engine.h, minor tweak to...
commit | commitdiff | tree
2012-04-20 Clark BarrettUpdates to array theory - much more lazy about introduction...
commit | commitdiff | tree
2012-04-14 Clark BarrettFixed bug in sharing with arrays of different types
 commit | commitdiff | tree
2011-07-11 Clark BarrettAdding static_fact_manager
 commit | commitdiff | tree
2011-07-11 Clark BarrettClark's work on array theory - can now solve all QF_AX...
commit | commitdiff | tree
2011-07-10 Clark BarrettReverting mistaken check-in
 commit | commitdiff | tree
2011-07-10 Clark BarrettFixed bug in default solve - wasn't returning when...
commit | commitdiff | tree
2011-04-11 Clark BarrettTransitive closure module is working
 commit | commitdiff | tree
2011-04-08 Clark BarrettAdded util class
 commit | commitdiff | tree
2010-07-07 Clark BarrettShared term manager tested and working
 commit | commitdiff | tree
2010-07-07 Clark BarrettUpdated headers
 commit | commitdiff | tree
2010-07-07 Clark BarrettAdded shared term manager. Basic mechanism for identifying...
commit | commitdiff | tree
2010-07-06 Clark BarrettMoved registration to theory engine
 commit | commitdiff | tree
2010-07-05 Clark BarrettAdded Cesare to list of authors
 commit | commitdiff | tree
2010-07-05 Clark BarrettChanged AUTHORS - removed references to earlier CVC...
commit | commitdiff | tree
2010-06-14 Clark BarrettStarted work on array theory
 commit | commitdiff | tree
2010-03-23 Clark BarrettDocumented that ContextObj::destroy() only restores...
commit | commitdiff | tree
2010-03-13 Clark BarrettFix for bug 45
 commit | commitdiff | tree
2010-02-10 Clark BarrettAdded calls to destructor in CDList plus optional flag...
commit | commitdiff | tree
2010-02-02 Clark BarrettFixed bug in context code
 commit | commitdiff | tree
2010-02-02 Clark BarrettFixed compile errors
 commit | commitdiff | tree
2010-02-02 Clark BarrettUpdates to context:
 commit | commitdiff | tree
2010-01-29 Clark Barrettone more bug
 commit | commitdiff | tree
2010-01-29 Clark BarrettFixed compile errors
 commit | commitdiff | tree
2010-01-29 Clark BarrettUpdate of context module
 commit | commitdiff | tree
2009-12-17 Clark BarrettMinor changes from code review
 commit | commitdiff | tree
2009-12-15 Clark BarrettAdded context_mm (haven't tested compilation yet...)
 commit | commitdiff | tree