summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/Makefile.am4
-rw-r--r--src/theory/arith/arith_prop_manager.cpp16
-rw-r--r--src/theory/arith/arith_prop_manager.h16
-rw-r--r--src/theory/arith/arith_rewriter.cpp5
-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.cpp146
-rw-r--r--src/theory/arith/theory_arith.h26
-rw-r--r--src/util/options.cpp12
-rw-r--r--src/util/options.h4
10 files changed, 223 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback