From 46a299aa48bcb0bff64bdb607f61f75a05987962 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 31 May 2011 01:06:16 +0000 Subject: [PATCH] This commit contains the code for allowing arbitrary equalities in the 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. --- src/theory/arith/Makefile.am | 4 +- src/theory/arith/arith_prop_manager.cpp | 16 +- src/theory/arith/arith_prop_manager.h | 16 +- src/theory/arith/arith_rewriter.cpp | 5 +- ...unate_propagator.cpp => atom_database.cpp} | 70 ++++----- .../{unate_propagator.h => atom_database.h} | 27 ++-- src/theory/arith/theory_arith.cpp | 146 +++++++++++++++--- src/theory/arith/theory_arith.h | 26 +++- src/util/options.cpp | 12 +- src/util/options.h | 4 +- test/regress/regress0/arith/Makefile.am | 1 + test/regress/regress0/arith/fuzz_3-eq.smt | 46 ++++++ 12 files changed, 270 insertions(+), 103 deletions(-) rename src/theory/arith/{unate_propagator.cpp => atom_database.cpp} (84%) rename src/theory/arith/{unate_propagator.h => atom_database.h} (85%) create mode 100644 test/regress/regress0/arith/fuzz_3-eq.smt 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 similarity index 84% rename from src/theory/arith/unate_propagator.cpp rename to 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 @@ -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 similarity index 85% rename from src/theory/arith/unate_propagator.h rename to 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 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 - << " \\-> " - < " + < 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::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::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 +)))))))))))))))))))))))))))))))))))))) -- 2.30.2