projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2012-06-12
Dejan Jovanović
missing problems
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong answer for bv
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Moved some things around in the preprocessor. Now...
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Fixed fuzzing bug
commit
|
commitdiff
|
tree
2012-06-12
Tim King
Fix to yesterday's change in arithmetic.
commit
|
commitdiff
|
tree
2012-06-12
Kshitij Bansal
bv reduced with decision: sat instead of unsat
commit
|
commitdiff
|
tree
2012-06-12
Kshitij Bansal
Assert fail equaility_engine.cpp: hasTerm(node) with...
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
bufixes and the bugs
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
conflicts from theories are removable
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Changed bitvector theory rewriter so that equalities...
commit
|
commitdiff
|
tree
2012-06-12
Kshitij Bansal
cleanup of exit mechanism when decisionEngine is on...
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt...
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Fixed failing assertion in arrays for bug 347
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
more breakage in aufbv
commit
|
commitdiff
|
tree
2012-06-12
Morgan Deters
minor cleanup, and replace a "private:" in equality...
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Fixed compile error
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Enabling constant propagation
commit
|
commitdiff
|
tree
2012-06-12
Morgan Deters
fix a few compatibility bindings issues
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong answer benchmarks
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong result benchmark
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
tests for the
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
test cases for the
commit
|
commitdiff
|
tree
2012-06-12
Clark Barrett
Adding constant propagation code - needs more testing...
commit
|
commitdiff
|
tree
2012-06-12
Tim King
Adding incorrect qf_lia result.
commit
|
commitdiff
|
tree
2012-06-12
Morgan Deters
fix ordering issue of --dump-to and --default-dag-thres...
commit
|
commitdiff
|
tree
2012-06-11
Tim King
Fix to term normalization of integer equalities. Adds...
commit
|
commitdiff
|
tree
2012-06-11
Tim King
Fixing type comparision assertion in getEqualityStatus().
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
another benchmark that used to fail
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
fixing bitvector bugs
commit
|
commitdiff
|
tree
2012-06-11
Morgan Deters
mark a quantifiers global var as "static" so we can...
commit
|
commitdiff
|
tree
2012-06-11
Clark Barrett
OK, now the rewrite issues are fixed
commit
|
commitdiff
|
tree
2012-06-11
Morgan Deters
distribute an .expect file. fixes a "make check" failu...
commit
|
commitdiff
|
tree
2012-06-11
Morgan Deters
Merge from quantifiers2-trunkmerge branch.
commit
|
commitdiff
|
tree
2012-06-11
Clark Barrett
Fix for array bug with decision heuristic
commit
|
commitdiff
|
tree
2012-06-11
Morgan Deters
fix issue referred to in bug 352 regarding infinite...
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
failing bv examples
commit
|
commitdiff
|
tree
2012-06-11
Clark Barrett
Fixed bug 352
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
some failing examples
commit
|
commitdiff
|
tree
2012-06-10
Clark Barrett
Fixed one more bug in rewriter
commit
|
commitdiff
|
tree
2012-06-10
Clark Barrett
Added a very fruitful assertion to the rewriter: checks...
commit
|
commitdiff
|
tree
2012-06-10
Dejan Jovanović
adding an assertion to trigger the problem of bug349...
commit
|
commitdiff
|
tree
2012-06-10
Dejan Jovanović
fixes for bug347
commit
|
commitdiff
|
tree
2012-06-09
Clark Barrett
Turning on unconstrained simp for QF_AUFBV
commit
|
commitdiff
|
tree
2012-06-09
Morgan Deters
Cleanup and comments for the dag-ifier. Also some...
commit
|
commitdiff
|
tree
2012-06-09
Morgan Deters
Dagification of output expressions.
commit
|
commitdiff
|
tree
2012-06-08
Morgan Deters
The option --arith-presolve-lemmas had previously been...
commit
|
commitdiff
|
tree
2012-06-08
Morgan Deters
Extend Printer infrastructure also to the "Result"...
commit
|
commitdiff
|
tree
2012-06-08
Morgan Deters
minor fixes, for Mac OS
commit
|
commitdiff
|
tree
2012-06-08
Dejan Jovanović
very small fast example for the bv fail
commit
|
commitdiff
|
tree
2012-06-08
Morgan Deters
Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri...
commit
|
commitdiff
|
tree
2012-06-08
Kshitij Bansal
handle BitVectorSignExtend in pickler
commit
|
commitdiff
|
tree
2012-06-08
Kshitij Bansal
threadlocal
commit
|
commitdiff
|
tree
2012-06-08
Kshitij Bansal
Merge from decision branch (till r3663)
commit
|
commitdiff
|
tree
2012-06-08
Dejan Jovanović
small fuzz examples where bv fails
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
fixing the wrong results. arrays equality adaptor had...
commit
|
commitdiff
|
tree
2012-06-07
Morgan Deters
LogicInfo locking implemented, and some initialization...
commit
|
commitdiff
|
tree
2012-06-07
Clark Barrett
Fixed performance issue with ite_simplifier on some...
commit
|
commitdiff
|
tree
2012-06-07
Morgan Deters
Adding EchoCommand and associated printer and parser...
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
cleaning up the expample for the future
commit
|
commitdiff
|
tree
2012-06-07
Clark Barrett
Added small test case for diseq propagation
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
fixing some bugs in propagation of disequalities
commit
|
commitdiff
|
tree
2012-06-06
Clark Barrett
Don't ever call nonclausalSimplify if simplificationMod...
commit
|
commitdiff
|
tree
2012-06-06
Clark Barrett
Fixed assertion failures
commit
|
commitdiff
|
tree
2012-06-06
Morgan Deters
removing std::cout from trunk
commit
|
commitdiff
|
tree
2012-06-06
Morgan Deters
also remove now-incorrect comment from makefile
commit
|
commitdiff
|
tree
2012-06-06
Clark Barrett
Fixed broken test case, removed one that is a mistake
commit
|
commitdiff
|
tree
2012-06-06
Morgan Deters
unconstrained regressions are now run with "make check...
commit
|
commitdiff
|
tree
2012-06-06
Morgan Deters
Fixing numerous issues with tests and "make dist":
commit
|
commitdiff
|
tree
2012-06-06
Dejan Jovanović
disabling a super-expensive assertions to speed up...
commit
|
commitdiff
|
tree
2012-06-06
Dejan Jovanović
Changes to the combination mechanism, lots of details...
commit
|
commitdiff
|
tree
2012-06-06
Clark Barrett
Fixed problem causing crash at destruction time
commit
|
commitdiff
|
tree
2012-06-05
Clark Barrett
More clean-up
commit
|
commitdiff
|
tree
2012-06-05
Clark Barrett
Fixed a performance issue with unconstrained simplifier
commit
|
commitdiff
|
tree
2012-06-05
Clark Barrett
Adding missing files...
commit
|
commitdiff
|
tree
2012-06-04
Clark Barrett
Added preprocessing pass that propagates unconstrained...
commit
|
commitdiff
|
tree
2012-06-01
Morgan Deters
add a global user-context push/pop in smt engine, just...
commit
|
commitdiff
|
tree
2012-05-31
Clark Barrett
Fixed bug in bv: one more case where non-shared equalit...
commit
|
commitdiff
|
tree
2012-05-31
Morgan Deters
svn:ignore a parallel-tests driver file that automake...
commit
|
commitdiff
|
tree
2012-05-31
Morgan Deters
pass JAVA_CPPFLAGS properly
commit
|
commitdiff
|
tree
2012-05-30
Clark Barrett
Added BitwiseEq bitvector rewrite
commit
|
commitdiff
|
tree
2012-05-30
Clark Barrett
Fixed problem with array queue growing too large
commit
|
commitdiff
|
tree
2012-05-30
Morgan Deters
remove unused/broken check build target
commit
|
commitdiff
|
tree
2012-05-29
Morgan Deters
removing now-unused TheoryEngine::setLogic() interface...
commit
|
commitdiff
|
tree
2012-05-29
Clark Barrett
Enabled SolveEq bv rewrite
commit
|
commitdiff
|
tree
2012-05-28
Clark Barrett
Added some BV rewrites, fixed bugs in array theory...
commit
|
commitdiff
|
tree
2012-05-27
Dejan Jovanović
some reordering to keep invariants
commit
|
commitdiff
|
tree
2012-05-27
Dejan Jovanović
Committing the work on equality engine, I need to see...
commit
|
commitdiff
|
tree
2012-05-27
Clark Barrett
Another expensive function call in a Debug trace
commit
|
commitdiff
|
tree
2012-05-27
Clark Barrett
Another expensive function call in a Debug line
commit
|
commitdiff
|
tree
2012-05-25
Kshitij Bansal
init bug fix
commit
|
commitdiff
|
tree
2012-05-25
Clark Barrett
Checking in fix for bug 340 - somehow didn't get checke...
commit
|
commitdiff
|
tree
2012-05-24
Dejan Jovanović
Separating the subtheory implementations in the bitvect...
commit
|
commitdiff
|
tree
2012-05-24
Dejan Jovanović
Significant changes to the internals of the equality...
commit
|
commitdiff
|
tree
2012-05-22
Tim King
This commit merges in the branch arithmetic/cprop.
commit
|
commitdiff
|
tree
2012-05-21
Dejan Jovanović
Updating equality manager to handle tagged trigger...
commit
|
commitdiff
|
tree
2012-05-21
Morgan Deters
main() no longer catches non-CVC4 exceptions. This...
commit
|
commitdiff
|
tree
2012-05-19
Tim King
Adding regress test for bug 341.
commit
|
commitdiff
|
tree
2012-05-19
Tim King
- The array type rules were fixed to use isSubtypeOf.
commit
|
commitdiff
|
tree
2012-05-18
Tim King
This commit adds TypeNode::leastCommonTypeNode(). ...
commit
|
commitdiff
|
tree
2012-05-18
Tim King
This commit removes the dead psuedoboolean code.
commit
|
commitdiff
|
tree
next