projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Delayed the addition of unate propagation lemmas until propagation is called. The...
2011-04-02
Tim King
Delayed the addition of unate propagation lemmas until...
commit
|
commitdiff
|
tree
2011-03-31
Tim King
Fixes to Valuation.
commit
|
commitdiff
|
tree
2011-03-30
Tim King
Moved the constructor for Options out of the header...
commit
|
commitdiff
|
tree
2011-03-30
Tim King
Added the command line flag --rewrite-arithmetic-equalities...
commit
|
commitdiff
|
tree
2011-03-30
Tim King
Merged the branch sparse-tableau into trunk.
commit
|
commitdiff
|
tree
2011-03-22
Tim King
Merges the small changes on the queue-period branch...
commit
|
commitdiff
|
tree
2011-03-19
Tim King
Merges the pqueue-set branch into trunk. During VarOrder...
commit
|
commitdiff
|
tree
2011-03-18
Tim King
- The learned clauses from the miplib trick were being...
commit
|
commitdiff
|
tree
2011-03-17
Tim King
Switched SimplexDecisionProcedure::d_delayedLemmas...
commit
|
commitdiff
|
tree
2011-03-17
Tim King
SimplexDecisionProcedure no longer takes an OutputChannel...
commit
|
commitdiff
|
tree
2011-03-17
Tim King
- Removes arith_constants.h
commit
|
commitdiff
|
tree
2011-03-17
Tim King
Adds debugging output to EngineOutputChannel::lemma.
commit
|
commitdiff
|
tree
2011-03-17
Tim King
Fix for the bug introduced in 1477. The stuff that...
commit
|
commitdiff
|
tree
2011-03-16
Tim King
- Turns on the excluded middle assertions during the...
commit
|
commitdiff
|
tree
2011-03-16
Tim King
- Turns on the miplibTrick. This detects during the...
commit
|
commitdiff
|
tree
2011-03-08
Tim King
- Merges queue-interrogation branch into the trunk...
commit
|
commitdiff
|
tree
2011-03-07
Tim King
Merges branches/arithmetic/tableau-reset into the trunk...
commit
|
commitdiff
|
tree
2011-03-05
Tim King
- Adds PermissiveBackArithVarSet. This is very similar...
commit
|
commitdiff
|
tree
2011-03-05
Tim King
Enables the PreferenceFunction minBoundAndRowCount.
commit
|
commitdiff
|
tree
2011-03-05
Tim King
- Adds "PreferenceFunction" to SimplexDecisionProcedure...
commit
|
commitdiff
|
tree
2011-03-05
Tim King
- Made Rational::sgn() function const.
commit
|
commitdiff
|
tree
2011-03-03
Tim King
- Creates a queue for lemmas discovered during the...
commit
|
commitdiff
|
tree
2011-03-03
Tim King
Merged the tableau-copy branch into trunk. This adds...
commit
|
commitdiff
|
tree
2011-02-27
Tim King
- Adds a path for Theory to be passed a reference to...
commit
|
commitdiff
|
tree
2011-02-27
Tim King
- Makes VarCoeffPair a class instead of a typedef of...
commit
|
commitdiff
|
tree
2011-02-27
Tim King
- Adds a buffer to the ReducedRowVector addRowTimesConstant...
commit
|
commitdiff
|
tree
2011-02-26
Tim King
- Merged RowVector and ReducedRowVector.
commit
|
commitdiff
|
tree
2011-02-25
Tim King
- This commit adds some debugging information to ArithPriori...
commit
|
commitdiff
|
tree
2011-02-24
Tim King
- Adds an additional round of checks for a conflict...
commit
|
commitdiff
|
tree
2011-02-24
Tim King
- Adds an additional mode to ArithPriorityQueue, Collection...
commit
|
commitdiff
|
tree
2011-02-24
Tim King
- Changes ArithPriorityQueue to use stl::vector<>'s...
commit
|
commitdiff
|
tree
2011-02-22
Tim King
- Adds column based iterators.
commit
|
commitdiff
|
tree
2011-02-21
Tim King
- Adds the ArithPriorityQueue class. The ArithPriorityQueue...
commit
|
commitdiff
|
tree
2011-02-21
Tim King
- Adds the statistic d_avgNumRowsNotContainingOnPivot.
commit
|
commitdiff
|
tree
2011-02-19
Tim King
Changes:
commit
|
commitdiff
|
tree
2011-02-18
Tim King
Changes:
commit
|
commitdiff
|
tree
2011-02-17
Tim King
This commit merges the branch branches/arithmetic/quick...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
This commit is the promised clean up after removing...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
Removed ActivityMonitor from arithmetic. This was only...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
Row ejection is now completely disabled. Another commit...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
Removed vestigial normal form notes file from src/theory...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
I replaced the pattern "x = x + y;" with "x += y;"...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
Updates based on the group code review of arithmetic...
commit
|
commitdiff
|
tree
2011-02-17
Tim King
Deleting depricated files.
commit
|
commitdiff
|
tree
2011-02-16
Tim King
Overview of the changes:
commit
|
commitdiff
|
tree
2011-02-14
Tim King
Reverses the order of the d_possiblyInconsistent queue...
commit
|
commitdiff
|
tree
2011-02-13
Tim King
3 heuristics were added to arithmetic. A heuristic...
commit
|
commitdiff
|
tree
2010-11-16
Tim King
Added Theory::presolve().
commit
|
commitdiff
|
tree
2010-11-15
Tim King
Changes to Solver and PropEngine to support lemmasOnDemand...
commit
|
commitdiff
|
tree
2010-11-15
Tim King
This commit merges the arith-prop-opt branch into the...
commit
|
commitdiff
|
tree
2010-11-04
Tim King
Moving the post_mortem.py script out of contrib and...
commit
|
commitdiff
|
tree
2010-11-04
Tim King
Updates post_mortem.py script to be able to handle...
commit
|
commitdiff
|
tree
2010-11-04
Tim King
This commit adds the ejected and un-ejected statistics.
commit
|
commitdiff
|
tree
2010-11-03
Tim King
Adds size() to RowVector.
commit
|
commitdiff
|
tree
2010-11-03
Tim King
Adds statistics for the number of Uservariables and...
commit
|
commitdiff
|
tree
2010-11-03
Tim King
Adds AverageStat to stats.h.
commit
|
commitdiff
|
tree
2010-10-30
Tim King
Adds a hueristic from Alberto's thesis. For a fixed...
commit
|
commitdiff
|
tree
2010-10-29
Tim King
Fix for a problem caused by using a != instead of ...
commit
|
commitdiff
|
tree
2010-10-29
Tim King
Adds a very small test that triggers a bug. The bug...
commit
|
commitdiff
|
tree
2010-10-29
Tim King
Fixes RowVector::has().
commit
|
commitdiff
|
tree
2010-10-29
Tim King
Factors out the QF_LRA decision procedure from TheoryArith...
commit
|
commitdiff
|
tree
2010-10-28
Tim King
The Row implementation has no been replaced by RowVector...
commit
|
commitdiff
|
tree
2010-10-23
Tim King
Removed slack.h, and arith_activity.h. Replaced IsBasicManag...
commit
|
commitdiff
|
tree
2010-10-22
Tim King
Code cleanup for TheoryArith.
commit
|
commitdiff
|
tree
2010-10-22
Tim King
Fixes to getValue for TheoryArith.
commit
|
commitdiff
|
tree
2010-10-14
Tim King
Fixed computation of infinitesimals for arithmetic...
commit
|
commitdiff
|
tree
2010-10-13
Tim King
Removed vector<Monomial> monos from Polynomial. Now...
commit
|
commitdiff
|
tree
2010-10-13
Tim King
Added test/regress/regress1/arith and populated it...
commit
|
commitdiff
|
tree
2010-10-12
Tim King
IDENTITY has been removed.
commit
|
commitdiff
|
tree
2010-10-07
Tim King
Small tableau optimization.
commit
|
commitdiff
|
tree
2010-10-04
Tim King
Fix to bug 211. ArithVar is now typedefed to uint32_t.
commit
|
commitdiff
|
tree
2010-10-02
Tim King
branches/arith-indexed-variables merged into the main...
commit
|
commitdiff
|
tree
2010-09-27
Tim King
- This update adds DynamicArray<T>. This is a bare...
commit
|
commitdiff
|
tree
2010-09-16
Tim King
Bug fix to CVC4::theory::arith::VarList as well as...
commit
|
commitdiff
|
tree
2010-09-14
Tim King
* added test/regress/regress0/arith for easy arithmetic...
commit
|
commitdiff
|
tree
2010-09-13
Tim King
* New normal form for arithmetic is in place.
commit
|
commitdiff
|
tree
2010-07-22
Tim King
Added test file for fuzzsmt bug, bug187.smt2.
commit
|
commitdiff
|
tree
2010-07-08
Tim King
I am adding my smt-crunch scripts to source control...
commit
|
commitdiff
|
tree
2010-07-08
Tim King
Updates to the post_mortem.py script.
commit
|
commitdiff
|
tree
2010-07-07
Tim King
Fixes arith rewriter to allow for division by a constant...
commit
|
commitdiff
|
tree
2010-07-06
Tim King
Fixed exit status for competition mode.
commit
|
commitdiff
|
tree
2010-07-02
Tim King
Merges the cln-test branch into the main branch.
commit
|
commitdiff
|
tree
2010-06-29
Tim King
This commit merges the decaying-rows branch into the...
commit
|
commitdiff
|
tree
2010-06-29
Tim King
Update to stats.h is now back into the trunk. The...
commit
|
commitdiff
|
tree
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
next