summaryrefslogtreecommitdiff
path: root/src/theory/arith/atom_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/atom_database.cpp')
-rw-r--r--src/theory/arith/atom_database.cpp542
1 files changed, 0 insertions, 542 deletions
diff --git a/src/theory/arith/atom_database.cpp b/src/theory/arith/atom_database.cpp
deleted file mode 100644
index 3476eb8f5..000000000
--- a/src/theory/arith/atom_database.cpp
+++ /dev/null
@@ -1,542 +0,0 @@
-/********************* */
-/*! \file atom_database.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/atom_database.h"
-#include "theory/arith/arith_utilities.h"
-
-#include <list>
-
-using namespace std;
-using namespace CVC4::kind;
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) :
- d_arithOut(out), d_setsMap()
-{ }
-
-bool ArithAtomDatabase::leftIsSetup(TNode left) const{
- return d_setsMap.find(left) != d_setsMap.end();
-}
-
-const ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left) const{
- Assert(leftIsSetup(left));
- NodeToSetsMap::const_iterator i = d_setsMap.find(left);
- return i->second;
-}
-ArithAtomDatabase::VariablesSets& ArithAtomDatabase::getVariablesSets(TNode left){
- Assert(leftIsSetup(left));
- NodeToSetsMap::iterator i = d_setsMap.find(left);
- return i->second;
-}
-EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left){
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_eqValueSet;
-}
-
-const EqualValueSet& ArithAtomDatabase::getEqualValueSet(TNode left) const{
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_eqValueSet;
-}
-
-BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left){
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_boundValueSet;
-}
-
-const BoundValueSet& ArithAtomDatabase::getBoundValueSet(TNode left) const{
- Assert(leftIsSetup(left));
- return getVariablesSets(left).d_boundValueSet;
-}
-
-bool ArithAtomDatabase::hasAnyAtoms(TNode v) const{
- Assert(!leftIsSetup(v)
- || !(getEqualValueSet(v)).empty()
- || !(getBoundValueSet(v)).empty());
-
- return leftIsSetup(v);
-}
-
-void ArithAtomDatabase::setupLefthand(TNode left){
- Assert(!leftIsSetup(left));
-
- d_setsMap[left] = VariablesSets();
-}
-
-bool ArithAtomDatabase::containsLiteral(TNode lit) const{
- switch(lit.getKind()){
- case NOT: return containsAtom(lit[0]);
- default: return containsAtom(lit);
- }
-}
-
-bool ArithAtomDatabase::containsAtom(TNode atom) const{
- switch(atom.getKind()){
- case EQUAL: return containsEquality(atom);
- case LEQ: return containsLeq(atom);
- case GEQ: return containsGeq(atom);
- default:
- Unreachable();
- }
-}
-
-bool ArithAtomDatabase::containsEquality(TNode atom) const{
- TNode left = atom[0];
- const EqualValueSet& eqSet = getEqualValueSet(left);
- return eqSet.find(atom) != eqSet.end();
-}
-
-bool ArithAtomDatabase::containsLeq(TNode atom) const{
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
-
- const BoundValueSet& bvSet = getBoundValueSet(left);
- BoundValueSet::const_iterator i = bvSet.find(value);
- if(i == bvSet.end()){
- return false;
- }else{
- const BoundValueEntry& entry = i->second;
- return entry.hasLeq();
- }
-}
-
-bool ArithAtomDatabase::containsGeq(TNode atom) const{
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
-
- const BoundValueSet& bvSet = getBoundValueSet(left);
- BoundValueSet::const_iterator i = bvSet.find(value);
- if(i == bvSet.end()){
- return false;
- }else{
- const BoundValueEntry& entry = i->second;
- return entry.hasGeq();
- }
-}
-
-void ArithAtomDatabase::addAtom(TNode atom){
- TNode left = atom[0];
- TNode right = atom[1];
-
- if(!leftIsSetup(left)){
- setupLefthand(left);
- }
-
- const Rational& value = rightHandRational(atom);
-
- switch(atom.getKind()){
- case EQUAL:
- {
- Assert(!containsEquality(atom));
- addImplicationsUsingEqualityAndEqualityValues(atom);
- addImplicationsUsingEqualityAndBoundValues(atom);
-
- pair<EqualValueSet::iterator, bool> res = getEqualValueSet(left).insert(atom);
- Assert(res.second);
- break;
- }
- case LEQ:
- {
- addImplicationsUsingLeqAndEqualityValues(atom);
- addImplicationsUsingLeqAndBoundValues(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- if(hasBoundValueEntry(atom)){
- BoundValueSet::iterator i = bvSet.find(value);
- BoundValueEntry& inSet = i->second;
- inSet.addLeq(atom);
- }else{
- bvSet.insert(make_pair(value, BoundValueEntry::mkFromLeq(atom)));
- }
- break;
- }
- case GEQ:
- {
- addImplicationsUsingGeqAndEqualityValues(atom);
- addImplicationsUsingGeqAndBoundValues(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- if(hasBoundValueEntry(atom)){
- BoundValueSet::iterator i = bvSet.find(value);
- BoundValueEntry& inSet = i->second;
- inSet.addGeq(atom);
- }else{
- bvSet.insert(make_pair(value, BoundValueEntry::mkFromGeq(atom)));
- }
- break;
- }
- default:
- Unreachable();
- }
-}
-
-bool ArithAtomDatabase::hasBoundValueEntry(TNode atom){
- TNode left = atom[0];
- const Rational& value = rightHandRational(atom);
- BoundValueSet& bvSet = getBoundValueSet(left);
- return bvSet.find(value) != bvSet.end();
-}
-
-bool rightHandRationalIsEqual(TNode a, TNode b){
- TNode secondA = a[1];
- TNode secondB = b[1];
-
- const Rational& qA = secondA.getConst<Rational>();
- const Rational& qB = secondB.getConst<Rational>();
-
- return qA == qB;
-}
-
-
-bool rightHandRationalIsLT(TNode a, TNode b){
- //This version is sticking around because it is easier to read!
- return RightHandRationalLT()(a,b);
-}
-
-void ArithAtomDatabase::addImplicationsUsingEqualityAndEqualityValues(TNode atom){
- Assert(atom.getKind() == EQUAL);
- TNode left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- for(EqualValueSet::iterator eqIter = eqSet.begin(), endIter = eqSet.end();
- eqIter != endIter; ++eqIter){
- TNode eq = *eqIter;
- Assert(eq != atom);
- addImplication(eq, negation);
- }
-}
-
-// if weaker, do not return an equivalent node
-// if strict, get the strongest bound implied by (< x value)
-// if !strict, get the strongest bound implied by (<= x value)
-Node getUpperBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
- BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
- if(bv == bvSet.end()){
- return Node::null();
- }
-
- if((bv->second).getValue() == value){
- const BoundValueEntry& entry = bv->second;
- if(strict && entry.hasGeq() && !weaker){
- return NodeBuilder<1>(NOT) << entry.getGeq();
- }else if(entry.hasLeq() && (strict || !weaker)){
- return entry.getLeq();
- }
- }
- ++bv;
- if(bv == bvSet.end()){
- return Node::null();
- }
- Assert(bv->second.getValue() > value);
- const BoundValueEntry& entry = bv->second;
- if(entry.hasGeq()){
- return NodeBuilder<1>(NOT) << entry.getGeq();
- }else{
- Assert(entry.hasLeq());
- return entry.getLeq();
- }
-}
-
-
-
-
-// if weaker, do not return an equivalent node
-// if strict, get the strongest bound implied by (> x value)
-// if !strict, get the strongest bound implied by (>= x value)
-Node getLowerBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
- static int time = 0;
- ++time;
-
- if(bvSet.empty()){
- return Node::null();
- }
- Debug("getLowerBound") << "getLowerBound" << bvSet.size() << " " << value << " " << strict << weaker << endl;
-
- BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
- if(bv == bvSet.end()){
- Debug("getLowerBound") << "got end " << value << " " << (bvSet.rbegin()->second).getValue() << endl;
- Assert(value > (bvSet.rbegin()->second).getValue());
- }else{
- Debug("getLowerBound") << value << ", " << bv->second.getValue() << endl;
- Assert(value <= bv->second.getValue());
- }
-
- if(bv != bvSet.end() && (bv->second).getValue() == value){
- const BoundValueEntry& entry = bv->second;
- Debug("getLowerBound") << entry.hasLeq() << entry.hasGeq() << endl;
- if(strict && entry.hasLeq() && !weaker){
- return NodeBuilder<1>(NOT) << entry.getLeq();
- }else if(entry.hasGeq() && (strict || !weaker)){
- return entry.getGeq();
- }
- }
- if(bv == bvSet.begin()){
- return Node::null();
- }else{
- --bv;
- // (and (>= x v) (>= v v')) then (> x v')
- Assert(bv->second.getValue() < value);
- const BoundValueEntry& entry = bv->second;
- if(entry.hasLeq()){
- return NodeBuilder<1>(NOT) << entry.getLeq();
- }else{
- Assert(entry.hasGeq());
- return entry.getGeq();
- }
- }
-}
-
-void ArithAtomDatabase::addImplicationsUsingEqualityAndBoundValues(TNode atom){
- Assert(atom.getKind() == EQUAL);
- Node left = atom[0];
-
- const Rational& value = rightHandRational(atom);
-
- BoundValueSet& bvSet = getBoundValueSet(left);
- Node ub = getUpperBound(bvSet, value, false, false);
- Node lb = getLowerBound(bvSet, value, false, false);
-
- if(!ub.isNull()){
- addImplication(atom, ub);
- }
-
- if(!lb.isNull()){
- addImplication(atom, lb);
- }
-}
-
-void ArithAtomDatabase::addImplicationsUsingLeqAndBoundValues(TNode atom)
-{
- Assert(atom.getKind() == LEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- Node ub = getImpliedUpperBoundUsingLeq(atom, false);
- Node lb = getImpliedLowerBoundUsingGT(negation, false);
-
- if(!ub.isNull()){
- addImplication(atom, ub);
- }
-
- if(!lb.isNull()){
- addImplication(negation, lb);
- }
-}
-
-void ArithAtomDatabase::addImplicationsUsingLeqAndEqualityValues(TNode atom) {
- Assert(atom.getKind() == LEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- TNode left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- //TODO Improve this later
- for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
- TNode eq = *eqIter;
- if(rightHandRationalIsEqual(atom, eq)){
- // (x = b' /\ b = b') => x <= b
- addImplication(eq, atom);
- }else if(rightHandRationalIsLT(atom, eq)){
- // (x = b' /\ b' > b) => x > b
- addImplication(eq, negation);
- }else{
- // (x = b' /\ b' < b) => x <= b
- addImplication(eq, atom);
- }
- }
-}
-
-
-void ArithAtomDatabase::addImplicationsUsingGeqAndBoundValues(TNode atom){
- Assert(atom.getKind() == GEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
- Node lb = getImpliedLowerBoundUsingGeq(atom, false); //What is implied by (>= left value)
- Node ub = getImpliedUpperBoundUsingLT(negation, false);
-
- if(!lb.isNull()){
- addImplication(atom, lb);
- }
-
- if(!ub.isNull()){
- addImplication(negation, ub);
- }
-}
-void ArithAtomDatabase::addImplicationsUsingGeqAndEqualityValues(TNode atom){
-
- Assert(atom.getKind() == GEQ);
- Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
- Node left = atom[0];
- EqualValueSet& eqSet = getEqualValueSet(left);
-
- //TODO Improve this later
- for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
- TNode eq = *eqIter;
- if(rightHandRationalIsEqual(atom, eq)){
- // (x = b' /\ b = b') => x >= b
- addImplication(eq, atom);
- }else if(rightHandRationalIsLT(eq, atom)){
- // (x = b' /\ b' < b) => x < b
- addImplication(eq, negation);
- }else{
- // (x = b' /\ b' > b) => x >= b
- addImplication(eq, atom);
- }
- }
-}
-
-void ArithAtomDatabase::addImplication(TNode a, TNode b){
- Node imp = NodeBuilder<2>(IMPLIES) << a << b;
-
- Debug("arith::unate") << "ArithAtomDatabase::addImplication"
- << "(" << a << ", " << b <<")" << endl;
-
- d_arithOut.lemma(imp);
-}
-
-
-Node ArithAtomDatabase::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const {
- Assert(leq.getKind() == LEQ);
- Node left = leq[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(leq);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- Node ub = getUpperBound(bvSet, value, false, weaker);
- return ub;
-}
-
-Node ArithAtomDatabase::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const {
- Assert(lt.getKind() == NOT && lt[0].getKind() == GEQ);
- Node atom = lt[0];
- Node left = atom[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(atom);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getUpperBound(bvSet, value, true, weaker);
-}
-
-Node ArithAtomDatabase::getBestImpliedUpperBound(TNode upperBound) const {
- Node result = Node::null();
- if(upperBound.getKind() == LEQ ){
- result = getImpliedUpperBoundUsingLeq(upperBound, false);
- }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
- result = getImpliedUpperBoundUsingLT(upperBound, false);
- }else if(upperBound.getKind() == LT){
- Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
- Node lt = NodeBuilder<1>(NOT) << geq;
- result = getImpliedUpperBoundUsingLT(lt, false);
- }else{
- Unreachable();
- }
-
- Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithAtomDatabase::getWeakerImpliedUpperBound(TNode upperBound) const {
- Node result = Node::null();
- if(upperBound.getKind() == LEQ ){
- result = getImpliedUpperBoundUsingLeq(upperBound, true);
- }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
- result = getImpliedUpperBoundUsingLT(upperBound, true);
- }else if(upperBound.getKind() == LT){
- Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
- Node lt = NodeBuilder<1>(NOT) << geq;
- result = getImpliedUpperBoundUsingLT(lt, true);
- }else{
- Unreachable();
- }
- Assert(upperBound != result);
- Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithAtomDatabase::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const {
- Assert(gt.getKind() == NOT && gt[0].getKind() == LEQ);
- Node atom = gt[0];
- Node left = atom[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(atom);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getLowerBound(bvSet, value, true, weaker);
-}
-
-Node ArithAtomDatabase::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const {
- Assert(geq.getKind() == GEQ);
- Node left = geq[0];
-
- if(!leftIsSetup(left)) return Node::null();
-
- const Rational& value = rightHandRational(geq);
- const BoundValueSet& bvSet = getBoundValueSet(left);
-
- return getLowerBound(bvSet, value, false, weaker);
-}
-
-Node ArithAtomDatabase::getBestImpliedLowerBound(TNode lowerBound) const {
- Node result = Node::null();
- if(lowerBound.getKind() == GEQ ){
- result = getImpliedLowerBoundUsingGeq(lowerBound, false);
- }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
- result = getImpliedLowerBoundUsingGT(lowerBound, false);
- }else if(lowerBound.getKind() == GT){
- Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
- Node gt = NodeBuilder<1>(NOT) << leq;
- result = getImpliedLowerBoundUsingGT(gt, false);
- }else{
- Unreachable();
- }
- Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
- return result;
-}
-
-Node ArithAtomDatabase::getWeakerImpliedLowerBound(TNode lowerBound) const {
- Node result = Node::null();
- if(lowerBound.getKind() == GEQ ){
- result = getImpliedLowerBoundUsingGeq(lowerBound, true);
- }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
- result = getImpliedLowerBoundUsingGT(lowerBound, true);
- }else if(lowerBound.getKind() == GT){
- Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
- Node gt = NodeBuilder<1>(NOT) << leq;
- result = getImpliedLowerBoundUsingGT(gt, true);
- }else{
- Unreachable();
- }
- Assert(result != lowerBound);
-
- Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
- return result;
-}
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback