summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-21Updating equality manager to handle tagged trigger terms. Notifications are ↵Dejan Jovanović
pushed out for relationships between terms tagged with the same tag. No performance impact.
2012-05-19- The array type rules were fixed to use isSubtypeOf.Tim King
- The type of (kind::DIVISION x y) is RealType. - A reference to util/pseudoboolean.i was removed. - rec5.cvc is disabled for now. The type of 2 is Integer which is not a subtype of [0..11].
2012-05-18This commit adds TypeNode::leastCommonTypeNode(). The special case for ↵Tim King
arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339
2012-05-18This commit removes the dead psuedoboolean code.Tim King
2012-05-17This fixes a fascinating segfault. This is the sequence of events:Tim King
1) A restart occurs 2) A shared term is registered to arithmetic. 3) Arithmetic sets this up. 4) No new linear relations are added to arithmetic. 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has not had a row added since the last restart. 7) A new variable is added. 8) This exceeds the size of the column vector of the saved tableau by exactly one. 9) segfault
2012-05-15This commit removes the CONST_INTEGER kind from nodes. This code comes from ↵Tim King
the branch arithmetic/remove_const_int.
2012-05-14fixes for shared term registration. previously the type was not considered ↵Dejan Jovanović
when looking at theories of the term and for a term like read(a, f(x)) the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.
2012-05-11Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().Tim King
2012-05-09* simplifying equality engine interfaceDejan Jovanović
* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations
2012-05-07Fixing a bug with TheoryArith::ppAssert() and shared terms.Tim King
2012-05-07Fixes a sign bug in the DioSolver.Tim King
2012-05-04- This fixes a problem where simplex produced the same conflict in the ↵Tim King
single check call. - This increases the number of substitutions that ppAssert can solve on integer equations.
2012-05-03Some cleanup starting off from trying to understand the sharing code. ↵Dejan Jovanović
Changes include * fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles * moved the LogicInfo into the theory constructor
2012-04-27This merges in the branch cvc4/branches/arithmetic/matrix into trunk.Tim King
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau. - Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code. - No performance loss!
2012-04-24This commit merges in the branch branches/arithmetic/congruence into trunk. ↵Tim King
Here are a summary of the changes: - Adds CDMaybe and CDRaised in cdmaybe.h - Add test for congruence over arithmetic terms and constants - Renames DifferenceManager to CongruenceManager - Changes a number of internal details for CongruenceManager
2012-04-18cout -> warning. Happening in portfolioKshitij Bansal
rest of the search go through, but still should be investigated
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
Adds DecisionEngine and an abstract class DecisionStrategy which other strategies will derive from eventually. Full revision summary of merged commits: r3241 merge from trunk r3240 fix r3239 WIP r3238 JH, CVC3 code: 5% done -- 5% translated r3237 JH groundwork r3236 make make regrss pass r3234 hueristic->heuristic r3229 JustificationHeuristic: EOD-WIP r3228 DecisionEngine: hookup assetions r3227 move ITE outside simplifyAssertions r3226 DecisionStrategy abstract class r3222 DecisionEngine: begin
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. ↵Tim King
Below is a highlight of the changes: - This introduces a new normal form to arithmetic. -- Equalities and disequalities are in solved form. Roughly speaking this means: (= x (+ y z)) is in normal form. (See the comments in normal_form.h for what this formally requires.) -- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ. Integer atoms always use GEQ. - Constraint was added to TheoryArith. -- A constraint is a triple of (k x v) where: --- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality), --- x is an ArithVar, and --- v is a DeltaRational value. -- Constraints are always attached to a ConstraintDatabase. -- A Constraint has its negation in the ConstraintDatabase [at least for now]. -- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values. -- This set can be iterated over and provides efficient access to other constraints for this variable. -- A literal may be attached to a constraint. -- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent). -- Constraints can be propagated. -- Every constraint has a proof (sat context dependent). -- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.) -- Equalities and disequalities can be marked as being split (user context dependent) - This removes and replaces: -- src/theory/arith/arith_prop_manager.* -- src/theory/arith/atom_database.* -- src/theory/arith/ordered_set.h - Added isZero(), isOne() and isNegativeOne() to Rational and Integer. - Added operator+ to CDList::const_iterator. - Added const_iterator to CDQueue. - Changes to regression tests.
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-02- Merged in the branch cdlist-cleanup.Tim King
- This adds a CleanUp template argument to CDList. - CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator. - CDVector<T> has been simplified and improved. - The expected performance impact is negligible.
2012-03-28enabling the --disable-arithmetic-propagation option in the arithmetic code ↵Dejan Jovanović
(it wasn't used)
2012-03-28Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit ↵Tim King
REWRITE_AGAIN calls.
2012-03-23Removed the variableRemovalEnabled option and d_removedRows from ↵Tim King
TheoryArith. This had been disabled for several months.
2012-03-22* improving arithmetic getEqualityStatusDejan Jovanović
* some sharing improvements based on model
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions. Removing one test case from the integer regress0.
2012-03-02This commit merges in the changes from branches/arithmetic/refactor0Tim King
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
2012-03-02CDMap -> CDHashMapDejan Jovanović
CDSet -> CDHashSet
2012-03-02Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to ↵Tim King
function names and documentation.
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2012-03-01Fixed a copy paste error where a lower bound was looked up instead of an ↵Tim King
upper bound.
2012-02-28This commit merges in branches/arithmetic/internalbb up to revision 2831. ↵Tim King
This is a significant refactoring of code. - r2820 -- Refactors Simplex so that it does significantly fewer functions. -- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model. -- Some of the code for propagation has moved to TheoryArith. -r2826 -- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound(). - r2827 -- Adds isZero() to Rational. Adds cmp to DeltaRational. - r2831 -- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp. -- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
2012-02-28Improves the arithmetic difference manager to delay any work until a shared ↵Tim King
term is added.
2012-02-25ppAsert -> ppAssertDejan Jovanović
2012-02-24Theory interface changes:Dejan Jovanović
solve -> ppAsert staticLearning -> ppStaticLearn preprocess -> ppRewrite SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*) via Eclipse refactoring magic.
2012-02-22Fix for bug 305.Tim King
2012-02-22Fixes to documentation / fixes for MacOSMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have ↵Tim King
manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from ↵Tim King
r2650 to r2779. - This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
2011-12-15Partial fix to bug 295.Tim King
2011-12-15Fix to the previous commit.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially ↵Tim King
resolves bug 289. Adds failing tests to regress1.
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody ↵Dejan Jovanović
merged-in * since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic ↵Tim King
now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
2011-10-28Adding a check in Polynomial::parsePolynomial to better enforce the ↵Tim King
arithmetic normal form when assertions are enabled.
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans.
2011-10-19Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 ↵Tim King
into trunk. Arithmetic should now be closer to being able to support push and pop.
2011-10-17Sharing workDejan Jovanović
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback