diff options
author | Tim King <taking@cs.nyu.edu> | 2012-02-15 21:52:16 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-02-15 21:52:16 +0000 |
commit | 9a0a59d5c85c4a1d2469f43e9d2b433e156810ba (patch) | |
tree | ba66b1c5cdeec062ce4144a463ec0b61a83e3cc6 /src/theory/arith/theory_arith.h | |
parent | 093fa1757392e7bfc18493f2daa87ff540aeea86 (diff) |
This commit merges into trunk the branch branches/arithmetic/integers2 from 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.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 89 |
1 files changed, 76 insertions, 13 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 6255efbbc..6b14ae6ff 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -12,8 +12,7 @@ ** information.\endverbatim ** ** \brief Arithmetic theory. - ** - ** Arithmetic theory. + ** ** Arithmetic theory. **/ #include "cvc4_private.h" @@ -59,6 +58,8 @@ namespace arith { class TheoryArith : public Theory { private: + bool d_hasDoneWorkSinceCut; + /** * The set of atoms that are currently in the context. * This is exactly the union of preregistered atoms and @@ -108,10 +109,40 @@ private: /** - * List of the types of variables in the system. - * "True" means integer, "false" means (non-integer) real. + * (For the moment) the type hierarchy goes as: + * PsuedoBoolean <: Integer <: Real + * The type number of a variable is an integer representing the most specific + * type of the variable. The possible values of type number are: */ - std::vector<short> d_integerVars; + enum ArithType + { + ATReal = 0, + ATInteger = 1, + ATPsuedoBoolean = 2 + }; + + std::vector<ArithType> d_variableTypes; + inline ArithType nodeToArithType(TNode x) const { + return x.getType().isPseudoboolean() ? ATPsuedoBoolean : + (x.getType().isInteger() ? ATInteger : ATReal); + } + + /** Returns true if x is of type Integer or PsuedoBoolean. */ + inline bool isInteger(ArithVar x) const { + return d_variableTypes[x] >= ATInteger; + } + /** Returns true if x is of type PsuedoBoolean. */ + inline bool isPsuedoBoolean(ArithVar x) const { + return d_variableTypes[x] == ATPsuedoBoolean; + } + + /** This is the set of variables initially introduced as slack variables. */ + std::vector<bool> d_slackVars; + + /** Returns true if the variable was initially introduced as a slack variable. */ + inline bool isSlackVariable(ArithVar x) const{ + return d_slackVars[x]; + } /** * On full effort checks (after determining LA(Q) satisfiability), we @@ -123,6 +154,21 @@ private: ArithVar d_nextIntegerCheckVar; /** + * Queue of Integer variables that are known to be equal to a constant. + */ + context::CDList<ArithVar> d_constantIntegerVariables; + /** Iterator over d_constantIntegerVariables. */ + context::CDO<unsigned int> d_CivIterator; + + Node callDioSolver(); + Node dioCutting(); + + Comparison mkIntegerEqualityFromAssignment(ArithVar v); + + #warning "DO NOT COMMIT TO TRUNK, USE MORE EFFICIENT CHECK INSTEAD" + CDArithVarSet d_varsInDioSolver; + + /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that * can be used to determine the value of n using getValue(). @@ -136,11 +182,6 @@ private: ArithPartialModel d_partialModel; /** - * Set of ArithVars that were introduced via preregisteration. - */ - ArithVarSet d_userVariables; - - /** * List of all of the inequalities asserted in the current context. */ context::CDSet<Node, NodeHashFunction> d_diseq; @@ -246,15 +287,37 @@ private: */ ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); - /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */ - void splitDisequalities(); + /** + * Splits the disequalities in d_diseq that are violated using lemmas on demand. + * returns true if any lemmas were issued. + * returns false if all disequalities are satisified in the current model. + */ + bool splitDisequalities(); + + + + /** + * Looks for the next integer variable without an integer assignment in a round robin fashion. + * Changes the value of d_nextIntegerCheckVar. + * + * If this returns false, d_nextIntegerCheckVar does not have an integer assignment. + * If this returns true, all integer variables have an integer assignment. + */ + bool hasIntegerModel(); + + /** + * Issues branches for non-slack integer variables with non-integer assignments. + * Returns a cut for a lemma. + * If there is an integer model, this returns Node::null(). + */ + Node roundRobinBranch(); /** * This requests a new unique ArithVar value for x. * This also does initial (not context dependent) set up for a variable, * except for setting up the initial. */ - ArithVar requestArithVar(TNode x, bool basic); + ArithVar requestArithVar(TNode x, bool slack); /** Initial (not context dependent) sets up for a variable.*/ void setupInitialValue(ArithVar x); |