diff options
-rw-r--r-- | src/theory/arith/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arith/arith_prop_manager.cpp | 16 | ||||
-rw-r--r-- | src/theory/arith/arith_prop_manager.h | 16 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/atom_database.cpp (renamed from src/theory/arith/unate_propagator.cpp) | 70 | ||||
-rw-r--r-- | src/theory/arith/atom_database.h (renamed from src/theory/arith/unate_propagator.h) | 27 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 146 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 26 | ||||
-rw-r--r-- | src/util/options.cpp | 12 | ||||
-rw-r--r-- | src/util/options.h | 4 | ||||
-rw-r--r-- | test/regress/regress0/arith/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/arith/fuzz_3-eq.smt | 46 |
12 files changed, 270 insertions, 103 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index c5534560b..7f193b9e3 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -14,6 +14,8 @@ libarith_la_SOURCES = \ arith_prop_manager.h \ arith_prop_manager.cpp \ arithvar_node_map.h \ + atom_database.h \ + atom_database.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ @@ -29,8 +31,6 @@ libarith_la_SOURCES = \ arith_priority_queue.cpp \ simplex.h \ simplex.cpp \ - unate_propagator.h \ - unate_propagator.cpp \ theory_arith.h \ theory_arith.cpp diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 77d32ef0b..7f38c74a7 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -34,10 +34,10 @@ Node ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaR Node weaker = bound; do { if(largeEpsilon){ - weaker = d_propagator.getBestImpliedUpperBound(weaker); + weaker = d_atomDatabase.getBestImpliedUpperBound(weaker); largeEpsilon = false; }else{ - weaker = d_propagator.getWeakerImpliedUpperBound(weaker); + weaker = d_atomDatabase.getWeakerImpliedUpperBound(weaker); } }while(!weaker.isNull() && !isAsserted(weaker)); return weaker; @@ -54,10 +54,10 @@ Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaR Debug("ArithPropManager") << bound << b << endl; do { if(largeEpsilon){ - weaker = d_propagator.getBestImpliedLowerBound(weaker); + weaker = d_atomDatabase.getBestImpliedLowerBound(weaker); largeEpsilon = false; }else{ - weaker = d_propagator.getWeakerImpliedLowerBound(weaker); + weaker = d_atomDatabase.getWeakerImpliedLowerBound(weaker); } }while(!weaker.isNull() && !isAsserted(weaker)); Debug("ArithPropManager") << "res: " << weaker << endl; @@ -66,11 +66,11 @@ Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaR Node ArithPropManager::getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const{ Node bound = boundAsNode(false, v, b); - return d_propagator.getBestImpliedLowerBound(bound); + return d_atomDatabase.getBestImpliedLowerBound(bound); } Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const{ Node bound = boundAsNode(true, v, b); - return d_propagator.getBestImpliedUpperBound(bound); + return d_atomDatabase.getBestImpliedUpperBound(bound); } Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const { @@ -106,8 +106,8 @@ bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const De Node bAsNode = boundAsNode(upperbound, var ,b); Node bestImplied = upperbound ? - d_propagator.getBestImpliedUpperBound(bAsNode): - d_propagator.getBestImpliedLowerBound(bAsNode); + d_atomDatabase.getBestImpliedUpperBound(bAsNode): + d_atomDatabase.getBestImpliedLowerBound(bAsNode); Debug("ArithPropManager") << upperbound <<","<< var <<","<< b <<","<< reason << endl << bestImplied << endl; diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 55d8ae635..39bcb7477 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -6,7 +6,7 @@ #include "theory/valuation.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar_node_map.h" -#include "theory/arith/unate_propagator.h" +#include "theory/arith/atom_database.h" #include "theory/arith/delta_rational.h" #include "context/context.h" #include "context/cdlist.h" @@ -51,7 +51,7 @@ public: d_reasons.push_back(reason); d_propagated.push_back(n); - //std::cout << n << std::endl << "<="<< reason<< std::endl; + Debug("ArithPropManager") << n << std::endl << "<="<< reason<< std::endl; } bool hasMorePropagations() const { @@ -76,15 +76,15 @@ public: class ArithPropManager : public PropManager { private: const ArithVarNodeMap& d_arithvarNodeMap; - const ArithUnatePropagator& d_propagator; + const ArithAtomDatabase& d_atomDatabase; Valuation d_valuation; public: ArithPropManager(context::Context* c, const ArithVarNodeMap& map, - const ArithUnatePropagator& prop, + const ArithAtomDatabase& db, Valuation v): - PropManager(c), d_arithvarNodeMap(map), d_propagator(prop), d_valuation(v) + PropManager(c), d_arithvarNodeMap(map), d_atomDatabase(db), d_valuation(v) {} /** @@ -99,10 +99,10 @@ public: Node boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const; Node strictlyWeakerLowerBound(TNode n) const{ - return d_propagator.getWeakerImpliedLowerBound(n); + return d_atomDatabase.getWeakerImpliedLowerBound(n); } Node strictlyWeakerUpperBound(TNode n) const{ - return d_propagator.getWeakerImpliedUpperBound(n); + return d_atomDatabase.getWeakerImpliedUpperBound(n); } Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const; @@ -113,7 +113,7 @@ public: Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const; bool containsLiteral(TNode n) const { - return d_propagator.containsLiteral(n); + return d_atomDatabase.containsLiteral(n); } private: diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 09cfabdc8..bc8604e85 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -261,11 +261,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ }else if(reduction.getKind() == kind::LT){ Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]); reduction = currNM->mkNode(kind::NOT, geq); - }else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){ + } + /* BREADCRUMB : Move this rewrite into preprocessing + else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){ Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]); Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]); reduction = currNM->mkNode(kind::AND, geq, leq); } + */ return RewriteResponse(REWRITE_DONE, reduction); diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/atom_database.cpp index 2785f0773..5c3519435 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/atom_database.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file unate_propagator.cpp +/*! \file atom_database.cpp ** \verbatim ** Original author: taking ** Major contributors: none @@ -17,7 +17,7 @@ ** \todo document this file **/ -#include "theory/arith/unate_propagator.h" +#include "theory/arith/atom_database.h" #include "theory/arith/arith_utilities.h" #include <list> @@ -30,45 +30,45 @@ using namespace CVC4::kind; using namespace std; -ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : +ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) : d_arithOut(out), d_setsMap() { } -bool ArithUnatePropagator::leftIsSetup(TNode left) const{ +bool ArithAtomDatabase::leftIsSetup(TNode left) const{ return d_setsMap.find(left) != d_setsMap.end(); } -const ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left) const{ +const ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left) const{ Assert(leftIsSetup(left)); NodeToSetsMap::const_iterator i = d_setsMap.find(left); return i->second; } -ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left){ +ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left){ Assert(leftIsSetup(left)); NodeToSetsMap::iterator i = d_setsMap.find(left); return i->second; } -EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left){ +EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left){ Assert(leftIsSetup(left)); return getVariablesSets(left).d_eqValueSet; } -const EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left) const{ +const EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left) const{ Assert(leftIsSetup(left)); return getVariablesSets(left).d_eqValueSet; } -BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left){ +BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left){ Assert(leftIsSetup(left)); return getVariablesSets(left).d_boundValueSet; } -const BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left) const{ +const BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left) const{ Assert(leftIsSetup(left)); return getVariablesSets(left).d_boundValueSet; } -bool ArithUnatePropagator::hasAnyAtoms(TNode v) const{ +bool ArithAtomDatabase::hasAnyAtoms(TNode v) const{ Assert(!leftIsSetup(v) || !(getEqualValueSet(v)).empty() || !(getBoundValueSet(v)).empty()); @@ -76,20 +76,20 @@ bool ArithUnatePropagator::hasAnyAtoms(TNode v) const{ return leftIsSetup(v); } -void ArithUnatePropagator::setupLefthand(TNode left){ +void ArithAtomDatabase::setupLefthand(TNode left){ Assert(!leftIsSetup(left)); d_setsMap[left] = VariablesSets(); } -bool ArithUnatePropagator::containsLiteral(TNode lit) const{ +bool ArithAtomDatabase::containsLiteral(TNode lit) const{ switch(lit.getKind()){ case NOT: return containsAtom(lit[0]); default: return containsAtom(lit); } } -bool ArithUnatePropagator::containsAtom(TNode atom) const{ +bool ArithAtomDatabase::containsAtom(TNode atom) const{ switch(atom.getKind()){ case EQUAL: return containsEquality(atom); case LEQ: return containsLeq(atom); @@ -99,13 +99,13 @@ bool ArithUnatePropagator::containsAtom(TNode atom) const{ } } -bool ArithUnatePropagator::containsEquality(TNode atom) const{ +bool ArithAtomDatabase::containsEquality(TNode atom) const{ TNode left = atom[0]; const EqualValueSet& eqSet = getEqualValueSet(left); return eqSet.find(atom) != eqSet.end(); } -bool ArithUnatePropagator::containsLeq(TNode atom) const{ +bool ArithAtomDatabase::containsLeq(TNode atom) const{ TNode left = atom[0]; const Rational& value = rightHandRational(atom); @@ -119,7 +119,7 @@ bool ArithUnatePropagator::containsLeq(TNode atom) const{ } } -bool ArithUnatePropagator::containsGeq(TNode atom) const{ +bool ArithAtomDatabase::containsGeq(TNode atom) const{ TNode left = atom[0]; const Rational& value = rightHandRational(atom); @@ -133,7 +133,7 @@ bool ArithUnatePropagator::containsGeq(TNode atom) const{ } } -void ArithUnatePropagator::addAtom(TNode atom){ +void ArithAtomDatabase::addAtom(TNode atom){ TNode left = atom[0]; TNode right = atom[1]; @@ -189,7 +189,7 @@ void ArithUnatePropagator::addAtom(TNode atom){ } } -bool ArithUnatePropagator::hasBoundValueEntry(TNode atom){ +bool ArithAtomDatabase::hasBoundValueEntry(TNode atom){ TNode left = atom[0]; const Rational& value = rightHandRational(atom); BoundValueSet& bvSet = getBoundValueSet(left); @@ -212,7 +212,7 @@ bool rightHandRationalIsLT(TNode a, TNode b){ return RightHandRationalLT()(a,b); } -void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityValues(TNode atom){ +void ArithAtomDatabase::addImplicationsUsingEqualityAndEqualityValues(TNode atom){ Assert(atom.getKind() == EQUAL); TNode left = atom[0]; EqualValueSet& eqSet = getEqualValueSet(left); @@ -307,7 +307,7 @@ Node getLowerBound(const BoundValueSet& bvSet, const Rational& value, bool stric } } -void ArithUnatePropagator::addImplicationsUsingEqualityAndBoundValues(TNode atom){ +void ArithAtomDatabase::addImplicationsUsingEqualityAndBoundValues(TNode atom){ Assert(atom.getKind() == EQUAL); Node left = atom[0]; @@ -326,7 +326,7 @@ void ArithUnatePropagator::addImplicationsUsingEqualityAndBoundValues(TNode atom } } -void ArithUnatePropagator::addImplicationsUsingLeqAndBoundValues(TNode atom) +void ArithAtomDatabase::addImplicationsUsingLeqAndBoundValues(TNode atom) { Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); @@ -343,7 +343,7 @@ void ArithUnatePropagator::addImplicationsUsingLeqAndBoundValues(TNode atom) } } -void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityValues(TNode atom) { +void ArithAtomDatabase::addImplicationsUsingLeqAndEqualityValues(TNode atom) { Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); @@ -367,7 +367,7 @@ void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityValues(TNode atom) } -void ArithUnatePropagator::addImplicationsUsingGeqAndBoundValues(TNode atom){ +void ArithAtomDatabase::addImplicationsUsingGeqAndBoundValues(TNode atom){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); @@ -382,7 +382,7 @@ void ArithUnatePropagator::addImplicationsUsingGeqAndBoundValues(TNode atom){ addImplication(negation, ub); } } -void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityValues(TNode atom){ +void ArithAtomDatabase::addImplicationsUsingGeqAndEqualityValues(TNode atom){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); @@ -405,17 +405,17 @@ void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityValues(TNode atom){ } } -void ArithUnatePropagator::addImplication(TNode a, TNode b){ +void ArithAtomDatabase::addImplication(TNode a, TNode b){ Node imp = NodeBuilder<2>(IMPLIES) << a << b; - Debug("arith::unate") << "ArithUnatePropagator::addImplication" + Debug("arith::unate") << "ArithAtomDatabase::addImplication" << "(" << a << ", " << b <<")" << endl; d_arithOut.lemma(imp); } -Node ArithUnatePropagator::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const { +Node ArithAtomDatabase::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const { Assert(leq.getKind() == LEQ); Node left = leq[0]; @@ -428,7 +428,7 @@ Node ArithUnatePropagator::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) return ub; } -Node ArithUnatePropagator::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const { +Node ArithAtomDatabase::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const { Assert(lt.getKind() == NOT && lt[0].getKind() == GEQ); Node atom = lt[0]; Node left = atom[0]; @@ -441,7 +441,7 @@ Node ArithUnatePropagator::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) co return getUpperBound(bvSet, value, true, weaker); } -Node ArithUnatePropagator::getBestImpliedUpperBound(TNode upperBound) const { +Node ArithAtomDatabase::getBestImpliedUpperBound(TNode upperBound) const { Node result = Node::null(); if(upperBound.getKind() == LEQ ){ result = getImpliedUpperBoundUsingLeq(upperBound, false); @@ -459,7 +459,7 @@ Node ArithUnatePropagator::getBestImpliedUpperBound(TNode upperBound) const { return result; } -Node ArithUnatePropagator::getWeakerImpliedUpperBound(TNode upperBound) const { +Node ArithAtomDatabase::getWeakerImpliedUpperBound(TNode upperBound) const { Node result = Node::null(); if(upperBound.getKind() == LEQ ){ result = getImpliedUpperBoundUsingLeq(upperBound, true); @@ -477,7 +477,7 @@ Node ArithUnatePropagator::getWeakerImpliedUpperBound(TNode upperBound) const { return result; } -Node ArithUnatePropagator::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const { +Node ArithAtomDatabase::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const { Assert(gt.getKind() == NOT && gt[0].getKind() == LEQ); Node atom = gt[0]; Node left = atom[0]; @@ -490,7 +490,7 @@ Node ArithUnatePropagator::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) co return getLowerBound(bvSet, value, true, weaker); } -Node ArithUnatePropagator::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const { +Node ArithAtomDatabase::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const { Assert(geq.getKind() == GEQ); Node left = geq[0]; @@ -502,7 +502,7 @@ Node ArithUnatePropagator::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) return getLowerBound(bvSet, value, false, weaker); } -Node ArithUnatePropagator::getBestImpliedLowerBound(TNode lowerBound) const { +Node ArithAtomDatabase::getBestImpliedLowerBound(TNode lowerBound) const { Node result = Node::null(); if(lowerBound.getKind() == GEQ ){ result = getImpliedLowerBoundUsingGeq(lowerBound, false); @@ -519,7 +519,7 @@ Node ArithUnatePropagator::getBestImpliedLowerBound(TNode lowerBound) const { return result; } -Node ArithUnatePropagator::getWeakerImpliedLowerBound(TNode lowerBound) const { +Node ArithAtomDatabase::getWeakerImpliedLowerBound(TNode lowerBound) const { Node result = Node::null(); if(lowerBound.getKind() == GEQ ){ result = getImpliedLowerBoundUsingGeq(lowerBound, true); diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/atom_database.h index 8c2720aea..25020977a 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/atom_database.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file unate_propagator.h +/*! \file atom_database.h ** \verbatim ** Original author: taking ** Major contributors: none @@ -11,24 +11,26 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief ArithUnatePropagator constructs implications of the form + ** \brief ArithAtomDatabase keeps a database of the arithmetic atoms. + ** Importantly, ArithAtomDatabase also handles unate propagations, + ** i.e. it constructs implications of the form ** "if x < c and c < b, then x < b" (where c and b are constants). ** - ** ArithUnatePropagator detects unate implications amongst the atoms + ** ArithAtomDatabase detects unate implications amongst the atoms ** associated with the theory of arithmetic and informs the SAT solver of the ** implication. A unate implication is an implication of the form: ** "if x < c and c < b, then x < b" (where c and b are constants). ** Unate implications are always 2-SAT clauses. - ** ArithUnatePropagator sends the implications to the SAT solver in an + ** ArithAtomDatabase sends the implications to the SAT solver in an ** online fashion. ** This means that atoms may be added during solving or before. ** - ** ArithUnatePropagator maintains sorted lists containing all atoms associated + ** ArithAtomDatabase maintains sorted lists containing all atoms associated ** for each unique left hand side, the "x" in the inequality "x < c". ** The lists are sorted by the value of the right hand side which must be a ** rational constant. ** - ** ArithUnatePropagator tries to send out a minimal number of additional + ** ArithAtomDatabase tries to send out a minimal number of additional ** lemmas per atom added. Let (x < a), (x < b), (x < c) be arithmetic atoms s.t. ** a < b < c. ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then @@ -45,8 +47,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H -#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H +#ifndef __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H +#define __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H #include "expr/node.h" #include "context/context.h" @@ -60,7 +62,7 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithUnatePropagator { +class ArithAtomDatabase { private: /** * OutputChannel for the theory of arithmetic. @@ -73,12 +75,11 @@ private: EqualValueSet d_eqValueSet; }; - /** TODO: justify making this a TNode. */ typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap; NodeToSetsMap d_setsMap; public: - ArithUnatePropagator(context::Context* cxt, OutputChannel& arith); + ArithAtomDatabase(context::Context* cxt, OutputChannel& arith); /** * Adds an atom to the propagator. @@ -118,7 +119,7 @@ private: /** * The addImplicationsUsingKAndJList(...) - * functions are the work horses of ArithUnatePropagator. + * functions are the work horses of the unate part of ArithAtomDatabase. * These take an atom of the kind K that has just been added * to its associated list, and the ordered list of Js associated with the lhs, * and uses these to deduce unate implications. @@ -162,4 +163,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */ +#endif /* __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 7c72b5a28..8e8064b7f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -38,7 +38,7 @@ #include "theory/arith/arithvar_set.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/unate_propagator.h" +#include "theory/arith/atom_database.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" @@ -66,11 +66,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu d_diseq(c), d_tableau(), d_restartsCounter(0), - d_presolveHasBeenCalled(false), + d_rowHasBeenAdded(false), d_tableauResetDensity(1.6), d_tableauResetPeriod(10), - d_propagator(c, out), - d_propManager(c, d_arithvarNodeMap, d_propagator, valuation), + d_atomDatabase(c, out), + d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation), d_simplex(d_propManager, d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() @@ -169,6 +169,18 @@ void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; Kind k = n.getKind(); + /* BREADCRUMB: I am using this bool to compile time enable testing for arbitrary equalities. */ + static bool turnOffEqualityPreRegister = false; + if(turnOffEqualityPreRegister){ + if(k == LEQ || k == LT || k == GT || k == GEQ){ + TNode left = n[0]; + delayedSetupPolynomial(left); + + d_atomDatabase.addAtom(n); + } + return; + } + bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n); if(isStrictlyVarList){ @@ -184,9 +196,7 @@ void TheoryArith::preRegisterTerm(TNode n) { if(isRelationOperator(k)){ Assert(Comparison::isNormalAtom(n)); - //cout << n << endl; - - d_propagator.addAtom(n); + d_atomDatabase.addAtom(n); TNode left = n[0]; TNode right = n[1]; @@ -247,6 +257,8 @@ void TheoryArith::setupSlack(TNode left){ ++(d_statistics.d_statSlackVariables); left.setAttribute(Slack(), true); + d_rowHasBeenAdded = true; + ArithVar varSlack = requestArithVar(left, true); Polynomial polyLeft = Polynomial::parsePolynomial(left); @@ -306,15 +318,86 @@ Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){ return conflict; } +void TheoryArith::delayedSetupMonomial(const Monomial& mono){ + + Debug("arith::delay") << "delayedSetupMonomial(" << mono.getNode() << ")" << endl; + + Assert(!mono.isConstant()); + VarList vl = mono.getVarList(); + + if(!d_arithvarNodeMap.hasArithVar(vl.getNode())){ + for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){ + Variable var = *i; + Node n = var.getNode(); + + ++(d_statistics.d_statUserVariables); + ArithVar varN = requestArithVar(n,false); + setupInitialValue(varN); + } + + if(!vl.singleton()){ + d_out->setIncomplete(); + + Node n = vl.getNode(); + ++(d_statistics.d_statUserVariables); + ArithVar varN = requestArithVar(n,false); + setupInitialValue(varN); + } + } +} + +void TheoryArith::delayedSetupPolynomial(TNode polynomial){ + Debug("arith::delay") << "delayedSetupPolynomial(" << polynomial << ")" << endl; + + Assert(Polynomial::isMember(polynomial)); + // if d_nodeMap.hasArithVar() all of the variables and it are setup + if(!d_arithvarNodeMap.hasArithVar(polynomial)){ + Polynomial poly = Polynomial::parsePolynomial(polynomial); + Assert(!poly.containsConstant()); + for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){ + Monomial mono = *i; + delayedSetupMonomial(mono); + } + + if(polynomial.getKind() == PLUS){ + Assert(!polynomial.getAttribute(Slack()), + "Polynomial has slack attribute but not does not have arithvar"); + setupSlack(polynomial); + } + } +} + +void TheoryArith::delayedSetupEquality(TNode equality){ + Debug("arith::delay") << "delayedSetupEquality(" << equality << ")" << endl; + + Assert(equality.getKind() == EQUAL); + + TNode left = equality[0]; + delayedSetupPolynomial(left); +} + +bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){ + Assert(equality.getKind() == EQUAL); + return d_arithvarNodeMap.hasArithVar(equality[0]); +} + Node TheoryArith::assertionCases(TNode assertion){ Kind simpKind = simplifiedKind(assertion); Assert(simpKind != UNDEFINED_KIND); + if(simpKind == EQUAL || simpKind == DISTINCT){ + Node eq = (simpKind == DISTINCT) ? assertion[0] : assertion; + + if(!canSafelyAvoidEqualitySetup(eq)){ + delayedSetupEquality(eq); + } + } + ArithVar x_i = determineLeftVariable(assertion, simpKind); DeltaRational c_i = determineRightConstant(assertion, simpKind); - Debug("arith_assertions") << "arith assertion(" << assertion - << " \\-> " - <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; + Debug("arith::assertions") << "arith assertion(" << assertion + << " \\-> " + <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; switch(simpKind){ case LEQ: if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { @@ -601,18 +684,18 @@ void TheoryArith::notifyRestart(){ uint32_t currSize = d_tableau.size(); uint32_t copySize = d_smallTableauCopy.size(); - //d_statistics.d_tableauSizeHistory << currSize; if(debugResetPolicy){ cout << "curr " << currSize << " copy " << copySize << endl; } - if(d_presolveHasBeenCalled && copySize == 0 && currSize > 0){ + if(d_rowHasBeenAdded){ if(debugResetPolicy){ - cout << "initial copy " << d_restartsCounter << endl; + cout << "row has been added must copy " << d_restartsCounter << endl; } - d_smallTableauCopy = d_tableau; // The initial copy + d_smallTableauCopy = d_tableau; + d_rowHasBeenAdded = false; } - if(d_presolveHasBeenCalled && d_restartsCounter >= RESET_START){ + if(!d_rowHasBeenAdded && d_restartsCounter >= RESET_START){ if(copySize >= currSize * 1.1 ){ ++d_statistics.d_smallerSetToCurr; d_smallTableauCopy = d_tableau; @@ -644,6 +727,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ // It appears that this can happen after other variables have been removed! // Tread carefullty with this one. + Assert(Options::current()->variableRemovalEnabled); + bool noRow = false; if(!d_tableau.isBasic(v)){ @@ -681,14 +766,27 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ void TheoryArith::presolve(){ TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime); - typedef std::vector<Node>::const_iterator VarIter; - for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ - Node variableNode = *i; - ArithVar var = d_arithvarNodeMap.asArithVar(variableNode); - if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){ - //The user variable is unconstrained. - //Remove this variable permanently - permanentlyRemoveVariable(var); + /* BREADCRUMB : Turn this on for QF_LRA/QF_RDL problems. + * + * The big problem for adding things back is that if they are readded they may + * need to be assigned an initial value at ALL context values. + * This is unsupported with our current datastructures. + * + * A better solution is to KNOW when the permantent removal is safe. + * This is true for single query QF_LRA/QF_RDL problems. + * Maybe a mechanism to ask "the sharing manager" + * if this variable/row can be used in sharing? + */ + if(Options::current()->variableRemovalEnabled){ + typedef std::vector<Node>::const_iterator VarIter; + for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ + Node variableNode = *i; + ArithVar var = d_arithvarNodeMap.asArithVar(variableNode); + if(d_userVariables.isMember(var) && !d_atomDatabase.hasAnyAtoms(variableNode)){ + //The user variable is unconstrained. + //Remove this variable permanently + permanentlyRemoveVariable(var); + } } } @@ -700,7 +798,5 @@ void TheoryArith::presolve(){ Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; learner.clear(); - - d_presolveHasBeenCalled = true; check(FULL_EFFORT); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1c8955d35..dc5cd2050 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -33,7 +33,7 @@ #include "theory/arith/tableau.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" -#include "theory/arith/unate_propagator.h" +#include "theory/arith/atom_database.h" #include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_prop_manager.h" @@ -108,7 +108,7 @@ private: * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau * is set to d_initialTableau. */ - bool d_presolveHasBeenCalled; + bool d_rowHasBeenAdded; double d_tableauResetDensity; uint32_t d_tableauResetPeriod; static const uint32_t s_TABLEAU_RESET_INCREMENT = 5; @@ -119,10 +119,16 @@ private: */ Tableau d_smallTableauCopy; - ArithUnatePropagator d_propagator; + /** + * The atom database keeps track of the atoms that have been preregistered. + * Used to add unate propagations. + */ + ArithAtomDatabase d_atomDatabase; + /** This manager keeps track of information needed to propagate. */ ArithPropManager d_propManager; + /** This implements the Simplex decision procedure. */ SimplexDecisionProcedure d_simplex; public: @@ -183,6 +189,20 @@ private: /** Initial (not context dependent) sets up for a new slack variable.*/ void setupSlack(TNode left); + /** + * Performs *permanent* static setup for equalities that have not been + * preregistered. + * Currently these MUST be introduced by combination. + */ + void delayedSetupEquality(TNode equality); + + void delayedSetupPolynomial(TNode polynomial); + void delayedSetupMonomial(const Monomial& mono); + + /** + * Performs a check to see if it is definitely true that setup can be avoided. + */ + bool canSafelyAvoidEqualitySetup(TNode equality); /** * Handles the case splitting for check() for a new assertion. diff --git a/src/util/options.cpp b/src/util/options.cpp index f68b64ab6..337eba9b6 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -82,7 +82,7 @@ Options::Options() : replayFilename(""), replayStream(NULL), replayLog(NULL), - rewriteArithEqualities(false), + variableRemovalEnabled(false), arithPropagation(false), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value @@ -123,7 +123,7 @@ static const string optionsDescription = "\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ - --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\ + --variable-removal-enables enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --enable-arithmetic-propagation turns on arithmetic propagation\n\ --incremental enable incremental solving\n"; @@ -213,7 +213,7 @@ enum OptionValue { PIVOT_RULE, RANDOM_FREQUENCY, RANDOM_SEED, - REWRITE_ARITHMETIC_EQUALITIES, + ENABLE_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION };/* enum OptionValue */ @@ -282,7 +282,7 @@ static struct option cmdlineOptions[] = { { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, - { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES }, + { "enable-variable-removel", no_argument, NULL, ENABLE_VARIABLE_REMOVAL }, { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -532,8 +532,8 @@ throw(OptionException) { #endif /* CVC4_REPLAY */ break; - case REWRITE_ARITHMETIC_EQUALITIES: - rewriteArithEqualities = true; + case ENABLE_VARIABLE_REMOVAL: + variableRemovalEnabled = true; break; case ARITHMETIC_PROPAGATION: diff --git a/src/util/options.h b/src/util/options.h index d9d9c8567..b8d21f2b0 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -159,8 +159,8 @@ struct CVC4_PUBLIC Options { /** Log to write replay instructions to; NULL if not logging. */ std::ostream* replayLog; - /** Whether to rewrite equalities in arithmetic theory */ - bool rewriteArithEqualities; + /** Determines whether arithmetic will try to variables. */ + bool variableRemovalEnabled; /** Turn on and of arithmetic propagation. */ bool arithPropagation; diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index a039f028b..700c59b8e 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -8,6 +8,7 @@ TESTS = \ arith.02.cvc \ arith.03.cvc \ delta-minimized-row-vector-bug.smt \ + fuzz_3-eq.smt \ leq.01.smt \ miplibtrick.smt diff --git a/test/regress/regress0/arith/fuzz_3-eq.smt b/test/regress/regress0/arith/fuzz_3-eq.smt new file mode 100644 index 000000000..ef44444b7 --- /dev/null +++ b/test/regress/regress0/arith/fuzz_3-eq.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_LRA +:extrafuns ((v0 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v1 Real)) +:status sat +:formula +(let (?n1 2) +(let (?n2 (* ?n1 ?n1)) +(let (?n3 (~ v0)) +(let (?n4 (* ?n1 ?n3)) +(let (?n5 (- ?n1 ?n1)) +(let (?n6 (- ?n5 v0)) +(let (?n7 (- ?n4 ?n6)) +(flet ($n8 (= ?n2 ?n7)) +(flet ($n9 false) +(let (?n10 (ite $n9 ?n1 v1)) +(let (?n11 (+ ?n1 v2)) +(flet ($n12 (= ?n10 ?n11)) +(let (?n13 (ite $n9 v0 ?n2)) +(let (?n14 (~ ?n1)) +(let (?n15 (ite $n9 ?n14 ?n1)) +(flet ($n16 (= ?n13 ?n15)) +(flet ($n17 (= ?n1 ?n7)) +(let (?n18 (+ ?n1 ?n1)) +(flet ($n19 (= v2 ?n18)) +(let (?n20 (ite $n19 v2 ?n1)) +(let (?n21 (ite $n17 ?n18 ?n20)) +(flet ($n22 (= ?n21 ?n2)) +(let (?n23 (ite $n9 ?n21 ?n2)) +(flet ($n24 (= ?n23 ?n1)) +(flet ($n25 (= ?n7 ?n2)) +(flet ($n26 (iff $n24 $n25)) +(let (?n27 (~ ?n7)) +(flet ($n28 (= ?n27 ?n1)) +(let (?n29 (ite $n28 ?n1 ?n1)) +(flet ($n30 (= ?n1 ?n29)) +(flet ($n31 (implies $n26 $n30)) +(flet ($n32 (implies $n9 $n9)) +(flet ($n33 (if_then_else $n22 $n31 $n32)) +(flet ($n34 (and $n9 $n33)) +(flet ($n35 (if_then_else $n16 $n34 $n9)) +(flet ($n36 (iff $n12 $n35)) +(flet ($n37 (and $n8 $n36)) +$n37 +)))))))))))))))))))))))))))))))))))))) |