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
/
Makefile.am
2011-04-18
Tim King
This commit merges the branch arithmetic/propagation...
blob
|
commitdiff
|
raw
2011-03-30
Tim King
Merged the branch sparse-tableau into trunk.
blob
|
commitdiff
|
raw
|
diff to current
2011-03-17
Tim King
- Removes arith_constants.h
blob
|
commitdiff
|
raw
|
diff to current
2011-02-21
Tim King
- Adds the ArithPriorityQueue class. The ArithPriorityQ...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-17
Tim King
Removed vestigial normal form notes file from src/theor...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-17
Tim King
Updates based on the group code review of arithmetic...
blob
|
commitdiff
|
raw
|
diff to current
2011-02-16
Tim King
Overview of the changes:
blob
|
commitdiff
|
raw
|
diff to current
2010-11-15
Morgan Deters
cleanup from today's commits: delegate as-yet-unimpleme...
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-10-29
Tim King
Factors out the QF_LRA decision procedure from TheoryAr...
blob
|
commitdiff
|
raw
|
diff to current
2010-10-28
Tim King
The Row implementation has no been replaced by RowVecto...
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-02
Tim King
branches/arith-indexed-variables merged into the main...
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-04
Morgan Deters
make dist && make distcheck functional, other fixes
blob
|
commitdiff
|
raw
|
diff to current
2010-07-03
Morgan Deters
With this commit come a number of changes to build...
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-15
Morgan Deters
fix last commit gcc options (-wunknown-pragmas ==>...
blob
|
commitdiff
|
raw
|
diff to current
2010-06-15
Morgan Deters
remove warnings about unknown #pragma GCC diagnostic...
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-05-04
Dejan Jovanović
Type-checking classes and hooks (not tested yet).
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-25
Morgan Deters
* src/expr/node.h: add a copy constructor. Apparently...
blob
|
commitdiff
|
raw
|
diff to current
2010-02-04
Morgan Deters
Added theory output channel interfaces and "Interrupted...
blob
|
commitdiff
|
raw
|
diff to current