summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.cpp
AgeCommit message (Collapse)Author
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-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-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-03-28enabling the --disable-arithmetic-propagation option in the arithmetic code ↵Dejan Jovanović
(it wasn't used)
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-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-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-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-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
2011-09-15tim's fixes for context-dependent pre-registrationDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-08-24Simplification of the preregister and register throught a NodeVisitor class. ↵Dejan Jovanović
The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.
2011-07-06Fixing two bugs:Dejan Jovanović
1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution 2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's ↵Morgan Deters
more than one "real" theory (not BUILTIN or BOOL) active
2011-05-31This commit contains the code for allowing arbitrary equalities in the ↵Tim King
theory of arithmetic. * This code has been partially tested. (My testing situation is currently not so great.) The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures. This does pass make regress as well as a fresh checkout does. (The Mac version has issues.) * I need to disable the permanent row removal heuristic by default. We need to discuss why this needs to happen. We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done. * I have disabled the arithmetic rewrite equality flag. This code needs to be added to the parser. * For all of the above changes, I have annotated the code with the key word BREADCRUMB. * I have renamed ArithUnatePropagator to ArithAtomDatabase.
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-04-18Removing dead code that came in on commit r1740.Tim King
2011-04-18This commit merges the branch arithmetic/propagation-again into trunk.Tim King
- This adds code for bounds refinement, and conflict weakening. - This adds util/boolean_simplification.h. - This adds a propagation manager to theory of arithmetic. - Propagation is disabled by default. - Propagation can be enabled by the command line flag "--enable-arithmetic-propagation" - Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
2011-04-04Reverts previous commit r1636.Tim King
2011-04-02Delayed the addition of unate propagation lemmas until propagation is ↵Tim King
called. The OutputChannel is now untouched by TheoryArith during preregistration.
2011-03-30Merged the branch sparse-tableau into trunk.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback