projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
This commit merges the branch arithmetic/propagation-again into trunk.
[cvc5.git]
/
src
/
theory
/
arith
/
theory_arith.h
2011-04-18
Tim King
This commit merges the branch arithmetic/propagation...
blob
|
commitdiff
|
raw
2011-04-04
Tim King
Reverts previous commit r1636.
blob
|
commitdiff
|
raw
|
diff to current
2011-04-02
Tim King
Delayed the addition of unate propagation lemmas until...
blob
|
commitdiff
|
raw
|
diff to current
2011-04-01
Morgan Deters
This commit is a merge from the "betterstats" branch...
blob
|
commitdiff
|
raw
|
diff to current
2011-03-30
Tim King
Merged the branch sparse-tableau into trunk.
blob
|
commitdiff
|
raw
|
diff to current
2011-03-25
Morgan Deters
This is a merge from the "theoryfixes+cdattrhash" branc...
blob
|
commitdiff
|
raw
|
diff to current
2011-03-17
Tim King
SimplexDecisionProcedure no longer takes an OutputChann...
blob
|
commitdiff
|
raw
|
diff to current
2011-03-17
Tim King
- Removes arith_constants.h
blob
|
commitdiff
|
raw
|
diff to current
2011-03-15
Morgan Deters
Merge from cudd branch. This mostly just adds support...
blob
|
commitdiff
|
raw
|
diff to current
2011-03-07
Tim King
Merges branches/arithmetic/tableau-reset into the trunk...
blob
|
commitdiff
|
raw
|
diff to current
2011-03-03
Tim King
Merged the tableau-copy branch into trunk. This adds...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-27
Tim King
- Adds a path for Theory to be passed a reference to...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-26
Morgan Deters
Merge from theory-break-dependences branch to break...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-19
Tim King
Changes:
blob
|
commitdiff
|
raw
|
diff to current
2011-02-18
Tim King
Changes:
blob
|
commitdiff
|
raw
|
diff to current
2011-02-17
Tim King
Removed ActivityMonitor from arithmetic. This was only...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-16
Tim King
Overview of the changes:
blob
|
commitdiff
|
raw
|
diff to current
2011-02-13
Tim King
3 heuristics were added to arithmetic. A heuristic...
blob
|
commitdiff
|
raw
|
diff to current
2011-01-05
Dejan Jovanović
Commit for the theory engine and rewriter changes....
blob
|
commitdiff
|
raw
|
diff to current
2010-11-16
Tim King
Added Theory::presolve().
blob
|
commitdiff
|
raw
|
diff to current
2010-11-15
Tim King
This commit merges the arith-prop-opt branch into the...
blob
|
commitdiff
|
raw
|
diff to current
2010-11-09
Dejan Jovanović
Lemmas on demand work, push-pop, some cleanup.
blob
|
commitdiff
|
raw
|
diff to current
2010-10-29
Tim King
Factors out the QF_LRA decision procedure from TheoryAr...
blob
|
commitdiff
|
raw
|
diff to current
2010-10-23
Tim King
Removed slack.h, and arith_activity.h. Replaced IsBasic...
blob
|
commitdiff
|
raw
|
diff to current
2010-10-22
Tim King
Code cleanup for TheoryArith.
blob
|
commitdiff
|
raw
|
diff to current
2010-10-09
Morgan Deters
Model generation for arith, boolean, and uf theories via
blob
|
commitdiff
|
raw
|
diff to current
2010-10-02
Tim King
branches/arith-indexed-variables merged into the main...
blob
|
commitdiff
|
raw
|
diff to current
2010-09-21
Morgan Deters
part of review (bug #197): coding conventions, file...
blob
|
commitdiff
|
raw
|
diff to current
2010-09-13
Tim King
* New normal form for arithmetic is in place.
blob
|
commitdiff
|
raw
|
diff to current
2010-07-07
Clark Barrett
Added shared term manager. Basic mechanism for identif...
blob
|
commitdiff
|
raw
|
diff to current
2010-07-04
Morgan Deters
With "-d extra-checking", rewrites are now checked...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-30
Morgan Deters
* theory "tree" rewriting implemented and works
blob
|
commitdiff
|
raw
|
diff to current
2010-06-29
Tim King
This commit merges the decaying-rows branch into the...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-29
Tim King
Merging the unate-propagator branch into the trunk...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-18
Tim King
Merging the statistics branch into the main trunk....
blob
|
commitdiff
|
raw
|
diff to current
2010-06-16
Tim King
Added the experimental. +bool TheoryArith::AssertEquali...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-16
Tim King
More assorted changes to arithmetic in preparation...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-06
Tim King
Some assorted fixes and local optimizations for theory...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-04
Tim King
Changed how assignments are saved during check. These...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-04
Morgan Deters
** Don't fear the files-changed list, almost all change...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-03
Tim King
Fixes 2 issues with assignments. The first is construct...
blob
|
commitdiff
|
raw
|
diff to current
2010-05-27
Tim King
Preregistration has been turned on. Highly experimental...
blob
|
commitdiff
|
raw
|
diff to current
2010-05-20
Tim King
Added the division symbol to the parser, and minimal...
blob
|
commitdiff
|
raw
|
diff to current
2010-05-19
Tim King
Significant revision to theory/arith. The new draft...
blob
|
commitdiff
|
raw
|
diff to current
2010-04-28
Tim King
Merging the arithmetic theory draft (lra-init) back...
blob
|
commitdiff
|
raw
|
diff to current
2010-04-04
Morgan Deters
* Node::isAtomic() now looks at an "atomic" attribute...
blob
|
commitdiff
|
raw
|
diff to current
2010-02-26
Morgan Deters
* test/unit/context/context_black.h: Test CDList<>...
blob
|
commitdiff
|
raw
|
diff to current
2010-02-25
Morgan Deters
* src/expr/node.h: add a copy constructor. Apparently...
blob
|
commitdiff
|
raw
|
diff to current