projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Merging the unate-propagator branch into the trunk. This is a big update so expect...
2010-06-29
Tim King
Merging the unate-propagator branch into the trunk...
commit
|
commitdiff
|
tree
2010-06-24
Tim King
Added post_mortem.py a statistics collector for user...
commit
|
commitdiff
|
tree
2010-06-22
Tim King
Made ~Stat() virtual. Added some additional statistics...
commit
|
commitdiff
|
tree
2010-06-18
Tim King
Merging the statistics branch into the main trunk....
commit
|
commitdiff
|
tree
2010-06-16
Tim King
Added the experimental. +bool TheoryArith::AssertEquality...
commit
|
commitdiff
|
tree
2010-06-16
Tim King
More assorted changes to arithmetic in preparation...
commit
|
commitdiff
|
tree
2010-06-16
Tim King
This commit just contains miscellaneous arithmetic...
commit
|
commitdiff
|
tree
2010-06-15
Tim King
I made a documentation change to get() to make explicit...
commit
|
commitdiff
|
tree
2010-06-14
Tim King
Fix to arith to make sure it only attempts to report...
commit
|
commitdiff
|
tree
2010-06-06
Tim King
Some assorted fixes and local optimizations for theory...
commit
|
commitdiff
|
tree
2010-06-06
Tim King
Adding += and *= to Rational.
commit
|
commitdiff
|
tree
2010-06-04
Tim King
Changed how assignments are saved during check. These...
commit
|
commitdiff
|
tree
2010-06-04
Tim King
Changed several arguments to const references.
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Fixes 2 issues with assignments. The first is constructing...
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Adds toString to DeltaRational
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Fixes a bug where registration occurs before preregistration.
commit
|
commitdiff
|
tree
2010-06-01
Tim King
This commit adds a debugTagIsOn() guard around some...
commit
|
commitdiff
|
tree
2010-06-01
Tim King
This commit is a fix for a bug in removeITEs(). The...
commit
|
commitdiff
|
tree
2010-06-01
Tim King
Fixed a bug in partial_model.cpp where the data was...
commit
|
commitdiff
|
tree
2010-05-29
Tim King
Adding a couple of example from fuzzsmt to regress1.
commit
|
commitdiff
|
tree
2010-05-29
Tim King
Couple of fixes to theory arith. pivotAndUpdate now...
commit
|
commitdiff
|
tree
2010-05-29
Tim King
After blasting the disjuncts, TheoryEngine rewrite...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
This update enables TheoryArith to accept assertions...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Bug fixes for combining coefficients of rewritten nodes.
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Added printModel() to src/theory/arith/partial_model...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
A few changes to the organization of TheoryEngine rewriting...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Moving the ITE removal from CnfStream to TheoryEngine...
commit
|
commitdiff
|
tree
2010-05-27
Tim King
Reverting this file to not include any comments. (Morgan...
commit
|
commitdiff
|
tree
2010-05-27
Tim King
Preregistration has been turned on. Highly experimental...
commit
|
commitdiff
|
tree
2010-05-26
Tim King
. '+Outstanding case split in theory arith'
commit
|
commitdiff
|
tree
2010-05-26
Tim King
Fix for bug 131. Added some additional debugging assertions...
commit
|
commitdiff
|
tree
2010-05-25
Tim King
Added Rational constructors that only take a numerator...
commit
|
commitdiff
|
tree
2010-05-21
Tim King
Small fixes to TheoryArith. Added a hack to make Integers...
commit
|
commitdiff
|
tree
2010-05-20
Tim King
Added the division symbol to the parser, and minimal...
commit
|
commitdiff
|
tree
2010-05-19
Tim King
Significant revision to theory/arith. The new draft...
commit
|
commitdiff
|
tree
2010-04-28
Tim King
Merging the arithmetic theory draft (lra-init) back...
commit
|
commitdiff
|
tree
2010-04-28
Tim King
Added theory/arith/kind and enabled the smt parser...
commit
|
commitdiff
|
tree
2010-04-07
Tim King
This update contains more black-box tests as part of...
commit
|
commitdiff
|
tree
2010-04-02
Tim King
Fixed the 32 bit vs. 64 bit problem in the rational...
commit
|
commitdiff
|
tree
2010-03-28
Tim King
Improved the documentation and testing for Rational.
commit
|
commitdiff
|
tree
2010-03-26
Tim King
Added GMP backed Rational and Integer classes, and...
commit
|
commitdiff
|
tree
2010-03-23
Tim King
Fixed some memory cleanup and destruction issues with...
commit
|
commitdiff
|
tree
2010-03-11
Tim King
Added some hand generated UF tests. Unfortunartely...
commit
|
commitdiff
|
tree
2010-03-09
Tim King
Fixed non-debug build problems
commit
|
commitdiff
|
tree
2010-03-08
Tim King
Improved output for theory uf
commit
|
commitdiff
|
tree
2010-03-04
Tim King
Committing a bug fix from Dejan. This resolves an issue...
commit
|
commitdiff
|
tree
2010-03-01
Tim King
Added theory black box test.
commit
|
commitdiff
|
tree
2010-03-01
Tim King
Node builder tests that targetted properly detecting...
commit
|
commitdiff
|
tree
2010-03-01
Tim King
Added some documentation to theory_uf.
commit
|
commitdiff
|
tree
2010-02-28
Tim King
TheoryUFWhite is passing. I fixed 2 errors. Unfortunately...
commit
|
commitdiff
|
tree
2010-02-26
Tim King
TheoryUFWhite tests are added. There are also accompanying...
commit
|
commitdiff
|
tree
2010-02-26
Tim King
Fixed a bug in CDList reallocation. (Also corrected...
commit
|
commitdiff
|
tree
2010-02-25
Tim King
Updated uf to reflect APPLY structure after conversation...
commit
|
commitdiff
|
tree
2010-02-25
Tim King
Created basic node builder and kind tests. Also fixed...
commit
|
commitdiff
|
tree
2010-02-24
Tim King
Cleaned up and documented ecdata and theory_uf.
commit
|
commitdiff
|
tree
2010-02-24
Tim King
Committing small changes to attribute, and theory to...
commit
|
commitdiff
|
tree
2010-02-17
Tim King
Initial draft of TheoryUF. Should compile without problems...
commit
|
commitdiff
|
tree
2010-02-04
Tim King
Changed mapping from atoms to literals in the prop...
commit
|
commitdiff
|
tree
2010-02-04
Tim King
Moved regressions into various levels based on running...
commit
|
commitdiff
|
tree
2010-02-04
Tim King
Fixes to the cnf converter. Also a barebones utility...
commit
|
commitdiff
|
tree
2010-02-03
Tim King
By popular demand, I also added a printAst to Expr.
commit
|
commitdiff
|
tree
2010-02-03
Tim King
I hacked in a temporary way to restart minisat for...
commit
|
commitdiff
|
tree
2010-02-03
Tim King
Within node I added printAst(..) for general purpose...
commit
|
commitdiff
|
tree
2010-02-03
Tim King
Enabled more regress tests. Takes 26s on my machine...
commit
|
commitdiff
|
tree
2010-02-02
Tim King
Switched cnf conversion to go through CnfStream.
commit
|
commitdiff
|
tree
2010-02-01
Tim King
Added this test back to avoid make check problems.
commit
|
commitdiff
|
tree
2010-01-30
Tim King
Checking in small test fixes for node_black
commit
|
commitdiff
|
tree
2010-01-27
Tim King
Added additional tests to node_black.h. CVC4 currently...
commit
|
commitdiff
|
tree
2010-01-26
Tim King
Undoing stupid commit mistake. Rolling back to -r...
commit
|
commitdiff
|
tree
2010-01-26
Tim King
Added test/regress/boolean.cvc
commit
|
commitdiff
|
tree
2010-01-23
Tim King
Added pure PL regression tests. Mostly CNF
commit
|
commitdiff
|
tree
2010-01-22
Tim King
Added regression test
commit
|
commitdiff
|
tree
2009-12-16
Tim King
Small refactoring changes for the expr package.
commit
|
commitdiff
|
tree