libarith_la_SOURCES = \
theory_arith_type_rules.h \
- next_arith_rewriter.h \
- next_arith_rewriter.cpp \
+ arith_rewriter.h \
+ arith_rewriter.cpp \
normal_form.h\
normal_form.cpp \
arith_utilities.h \
arith_constants.h \
- arith_activity.h \
delta_rational.h \
delta_rational.cpp \
partial_model.h \
partial_model.cpp \
ordered_bounds_list.h \
- basic.h \
- slack.h \
+ arithvar_dense_set.h \
tableau.h \
tableau.cpp \
arith_propagator.h \
+++ /dev/null
-/********************* */
-/*! \file arith_activity.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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 "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
-#define __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
-
-#include "expr/node.h"
-#include "expr/attribute.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-
-class ActivityMonitor {
-private:
- std::vector<uint64_t> d_activities;
-
-public:
- const static uint64_t ACTIVITY_THRESHOLD = 100;
-
- ActivityMonitor() : d_activities() {}
-
- void resetActivity(ArithVar var){
- d_activities[var] = 0;
- }
-
- void initActivity(ArithVar var){
- Assert(var == d_activities.size());
- d_activities.push_back(0);
- }
-
- uint64_t getActivity(ArithVar var) const{
- return d_activities[var];
- }
-
- inline void increaseActivity(ArithVar var, uint64_t x){
- d_activities[var] += x;
- }
-
-};
-
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-
-#endif
--- /dev/null
+/********************* */
+/*! \file arith_rewriter.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 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/theory.h"
+#include "theory/arith/normal_form.h"
+#include "theory/arith/arith_rewriter.h"
+#include "theory/arith/arith_utilities.h"
+
+#include <vector>
+#include <set>
+#include <stack>
+
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+bool isVariable(TNode t){
+ return t.getMetaKind() == kind::metakind::VARIABLE;
+}
+
+RewriteResponse ArithRewriter::rewriteConstant(TNode t){
+ Assert(t.getMetaKind() == kind::metakind::CONSTANT);
+ Node val = coerceToRationalNode(t);
+
+ return RewriteComplete(val);
+}
+
+RewriteResponse ArithRewriter::rewriteVariable(TNode t){
+ Assert(isVariable(t));
+
+ return RewriteComplete(t);
+}
+
+RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
+ Assert(t.getKind()== kind::MINUS);
+
+ if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE);
+
+ Node noMinus = makeSubtractionNode(t[0],t[1]);
+ if(pre){
+ return RewriteComplete(noMinus);
+ }else{
+ return FullRewriteNeeded(noMinus);
+ }
+}
+
+RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
+ Assert(t.getKind()== kind::UMINUS);
+
+ Node noUminus = makeUnaryMinusNode(t[0]);
+ if(pre)
+ return RewriteComplete(noUminus);
+ else
+ return RewriteAgain(noUminus);
+}
+
+RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
+ if(t.getMetaKind() == kind::metakind::CONSTANT){
+ return rewriteConstant(t);
+ }else if(isVariable(t)){
+ return rewriteVariable(t);
+ }else if(t.getKind() == kind::MINUS){
+ return rewriteMinus(t, true);
+ }else if(t.getKind() == kind::UMINUS){
+ return rewriteUMinus(t, true);
+ }else if(t.getKind() == kind::DIVISION){
+ if(t[0].getKind()== kind::CONST_RATIONAL){
+ return rewriteDivByConstant(t, true);
+ }else{
+ return RewriteComplete(t);
+ }
+ }else if(t.getKind() == kind::PLUS){
+ return preRewritePlus(t);
+ }else if(t.getKind() == kind::MULT){
+ return preRewriteMult(t);
+ }else{
+ Unreachable();
+ }
+}
+RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
+ if(t.getMetaKind() == kind::metakind::CONSTANT){
+ return rewriteConstant(t);
+ }else if(isVariable(t)){
+ return rewriteVariable(t);
+ }else if(t.getKind() == kind::MINUS){
+ return rewriteMinus(t, false);
+ }else if(t.getKind() == kind::UMINUS){
+ return rewriteUMinus(t, false);
+ }else if(t.getKind() == kind::DIVISION){
+ return rewriteDivByConstant(t, false);
+ }else if(t.getKind() == kind::PLUS){
+ return postRewritePlus(t);
+ }else if(t.getKind() == kind::MULT){
+ return postRewriteMult(t);
+ }else{
+ Unreachable();
+ }
+}
+
+RewriteResponse ArithRewriter::preRewriteMult(TNode t){
+ Assert(t.getKind()== kind::MULT);
+
+ // Rewrite multiplications with a 0 argument and to 0
+ Integer intZero;
+
+ for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
+ if((*i).getKind() == kind::CONST_RATIONAL) {
+ if((*i).getConst<Rational>() == d_constants->d_ZERO) {
+ return RewriteComplete(d_constants->d_ZERO_NODE);
+ }
+ } else if((*i).getKind() == kind::CONST_INTEGER) {
+ if((*i).getConst<Integer>() == intZero) {
+ if(t.getType().isInteger()) {
+ return RewriteComplete(NodeManager::currentNM()->mkConst(intZero));
+ } else {
+ return RewriteComplete(d_constants->d_ZERO_NODE);
+ }
+ }
+ }
+ }
+ return RewriteComplete(t);
+}
+RewriteResponse ArithRewriter::preRewritePlus(TNode t){
+ Assert(t.getKind()== kind::PLUS);
+
+ return RewriteComplete(t);
+}
+
+RewriteResponse ArithRewriter::postRewritePlus(TNode t){
+ Assert(t.getKind()== kind::PLUS);
+
+ Polynomial res = Polynomial::mkZero();
+
+ for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){
+ Node curr = *i;
+ Polynomial currPoly = Polynomial::parsePolynomial(curr);
+
+ res = res + currPoly;
+ }
+
+ return RewriteComplete(res.getNode());
+}
+
+RewriteResponse ArithRewriter::postRewriteMult(TNode t){
+ Assert(t.getKind()== kind::MULT);
+
+ Polynomial res = Polynomial::mkOne();
+
+ for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){
+ Node curr = *i;
+ Polynomial currPoly = Polynomial::parsePolynomial(curr);
+
+ res = res * currPoly;
+ }
+
+ return RewriteComplete(res.getNode());
+}
+
+RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
+ TNode left = t[0];
+ TNode right = t[1];
+
+
+ Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
+
+ if(cmp.isBoolean()){
+ return RewriteComplete(cmp.getNode());
+ }
+
+ if(cmp.getLeft().containsConstant()){
+ Monomial constantHead = cmp.getLeft().getHead();
+ Assert(constantHead.isConstant());
+
+ Constant constant = constantHead.getConstant();
+
+ Constant negativeConstantHead = -constant;
+
+ cmp = cmp.addConstant(negativeConstantHead);
+ }
+ Assert(!cmp.getLeft().containsConstant());
+
+ if(!cmp.getLeft().getHead().coefficientIsOne()){
+ Monomial constantHead = cmp.getLeft().getHead();
+ Assert(!constantHead.isConstant());
+ Constant constant = constantHead.getConstant();
+
+ Constant inverse = Constant::mkConstant(constant.getValue().inverse());
+
+ cmp = cmp.multiplyConstant(inverse);
+ }
+ Assert(cmp.getLeft().getHead().coefficientIsOne());
+
+ Assert(cmp.isBoolean() || cmp.isNormalForm());
+ return RewriteComplete(cmp.getNode());
+}
+
+RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
+ // left |><| right
+ TNode left = atom[0];
+ TNode right = atom[1];
+
+ if(right.getMetaKind() == kind::metakind::CONSTANT){
+ return postRewriteAtomConstantRHS(atom);
+ }else{
+ //Transform this to: (left - right) |><| 0
+ Node diff = makeSubtractionNode(left, right);
+ Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE);
+ return FullRewriteNeeded(reduction);
+ }
+}
+
+RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
+ Assert(isAtom(atom));
+ NodeManager* currNM = NodeManager::currentNM();
+
+ if(atom.getKind() == kind::EQUAL) {
+ if(atom[0] == atom[1]) {
+ return RewriteComplete(currNM->mkConst(true));
+ }
+ }
+
+ Node reduction = atom;
+
+ if(atom[1].getMetaKind() != kind::metakind::CONSTANT){
+ // left |><| right
+ TNode left = atom[0];
+ TNode right = atom[1];
+
+ //Transform this to: (left - right) |><| 0
+ Node diff = makeSubtractionNode(left, right);
+ reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE);
+ }
+
+ if(reduction.getKind() == kind::GT){
+ Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
+ reduction = currNM->mkNode(kind::NOT, leq);
+ }else if(reduction.getKind() == kind::LT){
+ Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
+ reduction = currNM->mkNode(kind::NOT, geq);
+ }
+
+ return RewriteComplete(reduction);
+}
+
+RewriteResponse ArithRewriter::postRewrite(TNode t){
+ if(isTerm(t)){
+ RewriteResponse response = postRewriteTerm(t);
+ if(Debug.isOn("arith::rewriter") && response.isDone()) {
+ Polynomial::parsePolynomial(response.getNode());
+ }
+ return response;
+ }else if(isAtom(t)){
+ RewriteResponse response = postRewriteAtom(t);
+ if(Debug.isOn("arith::rewriter") && response.isDone()) {
+ Comparison::parseNormalForm(response.getNode());
+ }
+ return response;
+ }else{
+ Unreachable();
+ return RewriteComplete(Node::null());
+ }
+}
+
+RewriteResponse ArithRewriter::preRewrite(TNode t){
+ if(isTerm(t)){
+ return preRewriteTerm(t);
+ }else if(isAtom(t)){
+ return preRewriteAtom(t);
+ }else{
+ Unreachable();
+ return RewriteComplete(Node::null());
+ }
+}
+
+Node ArithRewriter::makeUnaryMinusNode(TNode n){
+ return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n);
+}
+
+Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
+ Node negR = makeUnaryMinusNode(r);
+ Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR);
+
+ return diff;
+}
+
+RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
+ Assert(t.getKind()== kind::DIVISION);
+
+ Node left = t[0];
+ Node right = t[1];
+ Assert(right.getKind()== kind::CONST_RATIONAL);
+
+
+ const Rational& den = right.getConst<Rational>();
+
+ Assert(den != d_constants->d_ZERO);
+
+ Rational div = den.inverse();
+
+ Node result = mkRationalNode(div);
+
+ Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
+ if(pre){
+ return RewriteComplete(mult);
+ }else{
+ return RewriteAgain(mult);
+ }
+}
--- /dev/null
+/********************* */
+/*! \file arith_rewriter.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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/arith_constants.h"
+#include "theory/theory.h"
+#include "theory/arith/normal_form.h"
+
+#ifndef __CVC4__THEORY__ARITH__REWRITER_H
+#define __CVC4__THEORY__ARITH__REWRITER_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithRewriter{
+private:
+ ArithConstants* d_constants;
+
+ Node makeSubtractionNode(TNode l, TNode r);
+ Node makeUnaryMinusNode(TNode n);
+
+ RewriteResponse preRewriteTerm(TNode t);
+ RewriteResponse postRewriteTerm(TNode t);
+
+ RewriteResponse rewriteVariable(TNode t);
+ RewriteResponse rewriteConstant(TNode t);
+ RewriteResponse rewriteMinus(TNode t, bool pre);
+ RewriteResponse rewriteUMinus(TNode t, bool pre);
+ RewriteResponse rewriteDivByConstant(TNode t, bool pre);
+
+ RewriteResponse preRewritePlus(TNode t);
+ RewriteResponse postRewritePlus(TNode t);
+
+ RewriteResponse preRewriteMult(TNode t);
+ RewriteResponse postRewriteMult(TNode t);
+
+
+ RewriteResponse preRewriteAtom(TNode t);
+ RewriteResponse postRewriteAtom(TNode t);
+ RewriteResponse postRewriteAtomConstantRHS(TNode t);
+
+public:
+ ArithRewriter(ArithConstants* ac) : d_constants(ac) {}
+
+ RewriteResponse preRewrite(TNode n);
+ RewriteResponse postRewrite(TNode n);
+
+private:
+ bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); }
+ bool isTerm(TNode n) const { return !isAtom(n); }
+};
+
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__REWRITER_H */
#include "util/rational.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include <vector>
#include <stdint.h>
#include <limits>
return x.setAttribute(ArithVarAttr(), (uint64_t)a);
}
+typedef std::vector<uint64_t> ActivityMonitor;
+
+
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
--- /dev/null
+/********************* */
+/*! \file arithvar_dense_set.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 <vector>
+#include "theory/arith/arith_utilities.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
+#define __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithVarDenseSet {
+private:
+ std::vector<bool> d_set;
+
+public:
+ ArithVarDenseSet() : d_set() {}
+
+ size_t size() const {
+ return d_set.size();
+ }
+
+ void increaseSize(ArithVar max){
+ Assert(max >= size());
+ d_set.resize(max+1, false);
+ }
+
+ bool isMember(ArithVar x) const{
+ return d_set[x];
+ }
+
+ void init(ArithVar x, bool val) {
+ Assert(x >= size());
+ increaseSize(x);
+ d_set[x] = val;
+ }
+
+ void add(ArithVar x){
+ Assert(!isMember(x));
+ d_set[x] = true;
+ }
+
+ void remove(ArithVar x){
+ Assert(isMember(x));
+ d_set[x] = false;
+ }
+};
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H */
+++ /dev/null
-/********************* */
-/*! \file basic.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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 "expr/node.h"
-#include "expr/attribute.h"
-
-
-#ifndef __CVC4__THEORY__ARITH__BASIC_H
-#define __CVC4__THEORY__ARITH__BASIC_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class IsBasicManager {
-private:
- std::vector<bool> d_basic;
-
-public:
- IsBasicManager() : d_basic() {}
-
- void init(ArithVar var, bool value){
- Assert(var == d_basic.size());
- d_basic.push_back(value);
- }
-
- bool isBasic(ArithVar x) const{
- return d_basic[x];
- }
-
- void makeBasic(ArithVar x){
- Assert(!isBasic(x));
- d_basic[x] = true;
- }
-
- void makeNonbasic(ArithVar x){
- Assert(isBasic(x));
- d_basic[x] = false;
- }
-};
-
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH__BASIC_H */
+++ /dev/null
-/********************* */
-/*! \file next_arith_rewriter.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 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/theory.h"
-#include "theory/arith/normal_form.h"
-#include "theory/arith/next_arith_rewriter.h"
-#include "theory/arith/arith_utilities.h"
-
-#include <vector>
-#include <set>
-#include <stack>
-
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-bool isVariable(TNode t){
- return t.getMetaKind() == kind::metakind::VARIABLE;
-}
-
-RewriteResponse NextArithRewriter::rewriteConstant(TNode t){
- Assert(t.getMetaKind() == kind::metakind::CONSTANT);
- Node val = coerceToRationalNode(t);
-
- return RewriteComplete(val);
-}
-
-RewriteResponse NextArithRewriter::rewriteVariable(TNode t){
- Assert(isVariable(t));
-
- return RewriteComplete(t);
-}
-
-RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){
- Assert(t.getKind()== kind::MINUS);
-
- if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE);
-
- Node noMinus = makeSubtractionNode(t[0],t[1]);
- if(pre){
- return RewriteComplete(noMinus);
- }else{
- return FullRewriteNeeded(noMinus);
- }
-}
-
-RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){
- Assert(t.getKind()== kind::UMINUS);
-
- Node noUminus = makeUnaryMinusNode(t[0]);
- if(pre)
- return RewriteComplete(noUminus);
- else
- return RewriteAgain(noUminus);
-}
-
-RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){
- if(t.getMetaKind() == kind::metakind::CONSTANT){
- return rewriteConstant(t);
- }else if(isVariable(t)){
- return rewriteVariable(t);
- }else if(t.getKind() == kind::MINUS){
- return rewriteMinus(t, true);
- }else if(t.getKind() == kind::UMINUS){
- return rewriteUMinus(t, true);
- }else if(t.getKind() == kind::DIVISION){
- if(t[0].getKind()== kind::CONST_RATIONAL){
- return rewriteDivByConstant(t, true);
- }else{
- return RewriteComplete(t);
- }
- }else if(t.getKind() == kind::PLUS){
- return preRewritePlus(t);
- }else if(t.getKind() == kind::MULT){
- return preRewriteMult(t);
- }else{
- Unreachable();
- }
-}
-RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){
- if(t.getMetaKind() == kind::metakind::CONSTANT){
- return rewriteConstant(t);
- }else if(isVariable(t)){
- return rewriteVariable(t);
- }else if(t.getKind() == kind::MINUS){
- return rewriteMinus(t, false);
- }else if(t.getKind() == kind::UMINUS){
- return rewriteUMinus(t, false);
- }else if(t.getKind() == kind::DIVISION){
- return rewriteDivByConstant(t, false);
- }else if(t.getKind() == kind::PLUS){
- return postRewritePlus(t);
- }else if(t.getKind() == kind::MULT){
- return postRewriteMult(t);
- }else{
- Unreachable();
- }
-}
-
-RewriteResponse NextArithRewriter::preRewriteMult(TNode t){
- Assert(t.getKind()== kind::MULT);
-
- // Rewrite multiplications with a 0 argument and to 0
- Integer intZero;
-
- for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
- if((*i).getKind() == kind::CONST_RATIONAL) {
- if((*i).getConst<Rational>() == d_constants->d_ZERO) {
- return RewriteComplete(d_constants->d_ZERO_NODE);
- }
- } else if((*i).getKind() == kind::CONST_INTEGER) {
- if((*i).getConst<Integer>() == intZero) {
- if(t.getType().isInteger()) {
- return RewriteComplete(NodeManager::currentNM()->mkConst(intZero));
- } else {
- return RewriteComplete(d_constants->d_ZERO_NODE);
- }
- }
- }
- }
- return RewriteComplete(t);
-}
-RewriteResponse NextArithRewriter::preRewritePlus(TNode t){
- Assert(t.getKind()== kind::PLUS);
-
- return RewriteComplete(t);
-}
-
-RewriteResponse NextArithRewriter::postRewritePlus(TNode t){
- Assert(t.getKind()== kind::PLUS);
-
- Polynomial res = Polynomial::mkZero();
-
- for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){
- Node curr = *i;
- Polynomial currPoly = Polynomial::parsePolynomial(curr);
-
- res = res + currPoly;
- }
-
- return RewriteComplete(res.getNode());
-}
-
-RewriteResponse NextArithRewriter::postRewriteMult(TNode t){
- Assert(t.getKind()== kind::MULT);
-
- Polynomial res = Polynomial::mkOne();
-
- for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){
- Node curr = *i;
- Polynomial currPoly = Polynomial::parsePolynomial(curr);
-
- res = res * currPoly;
- }
-
- return RewriteComplete(res.getNode());
-}
-
-RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){
- TNode left = t[0];
- TNode right = t[1];
-
-
- Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
-
- if(cmp.isBoolean()){
- return RewriteComplete(cmp.getNode());
- }
-
- if(cmp.getLeft().containsConstant()){
- Monomial constantHead = cmp.getLeft().getHead();
- Assert(constantHead.isConstant());
-
- Constant constant = constantHead.getConstant();
-
- Constant negativeConstantHead = -constant;
-
- cmp = cmp.addConstant(negativeConstantHead);
- }
- Assert(!cmp.getLeft().containsConstant());
-
- if(!cmp.getLeft().getHead().coefficientIsOne()){
- Monomial constantHead = cmp.getLeft().getHead();
- Assert(!constantHead.isConstant());
- Constant constant = constantHead.getConstant();
-
- Constant inverse = Constant::mkConstant(constant.getValue().inverse());
-
- cmp = cmp.multiplyConstant(inverse);
- }
- Assert(cmp.getLeft().getHead().coefficientIsOne());
-
- Assert(cmp.isBoolean() || cmp.isNormalForm());
- return RewriteComplete(cmp.getNode());
-}
-
-RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){
- // left |><| right
- TNode left = atom[0];
- TNode right = atom[1];
-
- if(right.getMetaKind() == kind::metakind::CONSTANT){
- return postRewriteAtomConstantRHS(atom);
- }else{
- //Transform this to: (left - right) |><| 0
- Node diff = makeSubtractionNode(left, right);
- Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE);
- return FullRewriteNeeded(reduction);
- }
-}
-
-RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){
- Assert(isAtom(atom));
- NodeManager* currNM = NodeManager::currentNM();
-
- if(atom.getKind() == kind::EQUAL) {
- if(atom[0] == atom[1]) {
- return RewriteComplete(currNM->mkConst(true));
- }
- }
-
- Node reduction = atom;
-
- if(atom[1].getMetaKind() != kind::metakind::CONSTANT){
- // left |><| right
- TNode left = atom[0];
- TNode right = atom[1];
-
- //Transform this to: (left - right) |><| 0
- Node diff = makeSubtractionNode(left, right);
- reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE);
- }
-
- if(reduction.getKind() == kind::GT){
- Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
- reduction = currNM->mkNode(kind::NOT, leq);
- }else if(reduction.getKind() == kind::LT){
- Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
- reduction = currNM->mkNode(kind::NOT, geq);
- }
-
- return RewriteComplete(reduction);
-}
-
-RewriteResponse NextArithRewriter::postRewrite(TNode t){
- if(isTerm(t)){
- RewriteResponse response = postRewriteTerm(t);
- if(Debug.isOn("arith::rewriter") && response.isDone()) {
- Polynomial::parsePolynomial(response.getNode());
- }
- return response;
- }else if(isAtom(t)){
- RewriteResponse response = postRewriteAtom(t);
- if(Debug.isOn("arith::rewriter") && response.isDone()) {
- Comparison::parseNormalForm(response.getNode());
- }
- return response;
- }else{
- Unreachable();
- return RewriteComplete(Node::null());
- }
-}
-
-RewriteResponse NextArithRewriter::preRewrite(TNode t){
- if(isTerm(t)){
- return preRewriteTerm(t);
- }else if(isAtom(t)){
- return preRewriteAtom(t);
- }else{
- Unreachable();
- return RewriteComplete(Node::null());
- }
-}
-
-Node NextArithRewriter::makeUnaryMinusNode(TNode n){
- return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n);
-}
-
-Node NextArithRewriter::makeSubtractionNode(TNode l, TNode r){
- Node negR = makeUnaryMinusNode(r);
- Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR);
-
- return diff;
-}
-
-RewriteResponse NextArithRewriter::rewriteDivByConstant(TNode t, bool pre){
- Assert(t.getKind()== kind::DIVISION);
-
- Node left = t[0];
- Node right = t[1];
- Assert(right.getKind()== kind::CONST_RATIONAL);
-
-
- const Rational& den = right.getConst<Rational>();
-
- Assert(den != d_constants->d_ZERO);
-
- Rational div = den.inverse();
-
- Node result = mkRationalNode(div);
-
- Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
- if(pre){
- return RewriteComplete(mult);
- }else{
- return RewriteAgain(mult);
- }
-}
+++ /dev/null
-/********************* */
-/*! \file next_arith_rewriter.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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/arith_constants.h"
-#include "theory/theory.h"
-#include "theory/arith/normal_form.h"
-
-#ifndef __CVC4__THEORY__ARITH__REWRITER_NEXT_H
-#define __CVC4__THEORY__ARITH__REWRITER_NEXT_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class NextArithRewriter{
-private:
- ArithConstants* d_constants;
-
- Node makeSubtractionNode(TNode l, TNode r);
- Node makeUnaryMinusNode(TNode n);
-
- RewriteResponse preRewriteTerm(TNode t);
- RewriteResponse postRewriteTerm(TNode t);
-
- RewriteResponse rewriteVariable(TNode t);
- RewriteResponse rewriteConstant(TNode t);
- RewriteResponse rewriteMinus(TNode t, bool pre);
- RewriteResponse rewriteUMinus(TNode t, bool pre);
- RewriteResponse rewriteDivByConstant(TNode t, bool pre);
-
- RewriteResponse preRewritePlus(TNode t);
- RewriteResponse postRewritePlus(TNode t);
-
- RewriteResponse preRewriteMult(TNode t);
- RewriteResponse postRewriteMult(TNode t);
-
-
- RewriteResponse preRewriteAtom(TNode t);
- RewriteResponse postRewriteAtom(TNode t);
- RewriteResponse postRewriteAtomConstantRHS(TNode t);
-
-public:
- NextArithRewriter(ArithConstants* ac) : d_constants(ac) {}
-
- RewriteResponse preRewrite(TNode n);
- RewriteResponse postRewrite(TNode n);
-
-private:
- bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); }
- bool isTerm(TNode n) const { return !isAtom(n); }
-};
-
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH__REWRITER_NEXT_H */
+++ /dev/null
-/********************* */
-/*! \file slack.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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
- **/
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-struct SlackAttrID;
-
-typedef expr::Attribute<SlackAttrID, Node> Slack;
-
-
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
const std::vector<ArithVar>& variables){
Assert(coeffs.size() == variables.size());
- Assert(d_basicManager.isBasic(basicVar));
+ Assert(d_basicManager.isMember(basicVar));
//The new basic variable cannot already be a basic variable
Assert(!isActiveBasicVariable(basicVar));
for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
ArithVar var = *varsIter;
- if(d_basicManager.isBasic(var)){
+ if(d_basicManager.isMember(var)){
if(!isActiveBasicVariable(var)){
reinjectBasic(var);
}
}
void Tableau::pivot(ArithVar x_r, ArithVar x_s){
- Assert(d_basicManager.isBasic(x_r));
- Assert(!d_basicManager.isBasic(x_s));
+ Assert(d_basicManager.isMember(x_r));
+ Assert(!d_basicManager.isMember(x_s));
Row* row_s = lookup(x_r);
Assert(row_s->has(x_s));
d_rowsTable[x_r] = NULL;
d_activeBasicVars.erase(x_r);
- d_basicManager.makeNonbasic(x_r);
+ d_basicManager.remove(x_r);
d_activeBasicVars.insert(x_s);
- d_basicManager.makeBasic(x_s);
+ d_basicManager.add(x_s);
row_s->pivot(x_s);
ArithVar basic = *basicIter;
Row* row_k = lookup(basic);
if(row_k->has(x_s)){
- d_activityMonitor.increaseActivity(basic, 30);
+ d_activityMonitor[basic] += 30;
row_k->substitute(*row_s);
}
}
for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
ArithVar var = i->first;
++i;
- if(d_basicManager.isBasic(var)){
+ if(d_basicManager.isMember(var)){
Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
Assert(row_var != row);
#include "expr/attribute.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arith_activity.h"
-#include "theory/arith/basic.h"
+#include "theory/arith/arithvar_dense_set.h"
#include "theory/arith/normal_form.h"
#include <ext/hash_map>
ArithVarSet d_activeBasicVars;
RowsTable d_rowsTable;
+
ActivityMonitor& d_activityMonitor;
- IsBasicManager& d_basicManager;
+ ArithVarDenseSet& d_basicManager;
public:
/**
* Constructs an empty tableau.
*/
- Tableau(ActivityMonitor &am, IsBasicManager& bm) :
+ Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) :
d_activeBasicVars(),
d_rowsTable(),
d_activityMonitor(am),
void printTableau();
bool isEjected(ArithVar var){
- return d_basicManager.isBasic(var) && !isActiveBasicVariable(var);
+ return d_basicManager.isMember(var) && !isActiveBasicVariable(var);
}
void ejectBasic(ArithVar basic){
- Assert(d_basicManager.isBasic(basic));
+ Assert(d_basicManager.isMember(basic));
Assert(isActiveBasicVariable(basic));
d_activeBasicVars.erase(basic);
}
void reinjectBasic(ArithVar basic){
- Assert(d_basicManager.isBasic(basic));
+ Assert(d_basicManager.isMember(basic));
Assert(isEjected(basic));
Row* row = lookupEjected(basic);
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
-#include "theory/arith/slack.h"
-#include "theory/arith/basic.h"
-#include "theory/arith/arith_activity.h"
+#include "theory/arith/arithvar_dense_set.h"
-#include "theory/arith/next_arith_rewriter.h"
+#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_propagator.h"
#include "theory/arith/theory_arith.h"
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+struct SlackAttrID;
+typedef expr::Attribute<SlackAttrID, Node> Slack;
+const static uint64_t ACTIVITY_THRESHOLD = 100;
TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
Theory(id, c, out),
d_activityMonitor(),
d_diseq(c),
d_tableau(d_activityMonitor, d_basicManager),
- d_nextRewriter(&d_constants),
+ d_rewriter(&d_constants),
d_propagator(c),
d_statistics()
{}
return false;
}else if(!d_partialModel.hasEverHadABound(var)){
return true;
- }else if(d_activityMonitor.getActivity(var) >= ActivityMonitor::ACTIVITY_THRESHOLD){
+ }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
return true;
}
return false;
//TNode var = *i;
//ArithVar variable = asArithVar(var);
if(shouldEject(variable)){
- if(d_basicManager.isBasic(variable)){
+ if(d_basicManager.isMember(variable)){
Debug("decay") << "ejecting basic " << variable << endl;;
d_tableau.ejectBasic(variable);
}
void TheoryArith::checkBasicVariable(ArithVar basic){
- Assert(d_basicManager.isBasic(basic));
+ Assert(d_basicManager.isMember(basic));
if(!d_partialModel.assignmentIsConsistent(basic)){
d_possiblyInconsistent.push(basic);
}
setArithVar(x,varX);
- d_activityMonitor.initActivity(varX);
- d_basicManager.init(varX, basic);
+ Assert(varX == d_activityMonitor.size());
+ d_activityMonitor.push_back(0);
+
+ d_basicManager.init(varX,basic);
d_tableau.increaseSize();
Debug("arith::arithvar") << x << " |-> " << varX << endl;
*/
void TheoryArith::setupInitialValue(ArithVar x){
- if(!d_basicManager.isBasic(x)){
+ if(!d_basicManager.isMember(x)){
d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
}else{
//If the variable is basic, assertions may have already happened and updates
* Computes the value of a basic variable using the current assignment.
*/
DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
- Assert(d_basicManager.isBasic(x));
+ Assert(d_basicManager.isMember(x));
DeltaRational sum = d_constants.d_ZERO_DELTA;
Row* row = d_tableau.lookup(x);
RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
- return d_nextRewriter.preRewrite(n);
+ return d_rewriter.preRewrite(n);
}
void TheoryArith::registerTerm(TNode tn){
bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
- d_activityMonitor.resetActivity(x_i);
+ d_activityMonitor[x_i] = 0;
- if(!d_basicManager.isBasic(x_i)){
+ if(!d_basicManager.isMember(x_i)){
if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
- if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setLowerConstraint(x_i,original);
d_partialModel.setLowerBound(x_i, c_i);
- d_activityMonitor.resetActivity(x_i);
+ d_activityMonitor[x_i] = 0;
- if(!d_basicManager.isBasic(x_i)){
+ if(!d_basicManager.isMember(x_i)){
if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
- if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
- d_activityMonitor.resetActivity(x_i);
+ d_activityMonitor[x_i] = 0;
- if(!d_basicManager.isBasic(x_i)){
+ if(!d_basicManager.isMember(x_i)){
if(!(d_partialModel.getAssignment(x_i) == c_i)){
update(x_i, c_i);
}
return false;
}
void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
- Assert(!d_basicManager.isBasic(x_i));
+ Assert(!d_basicManager.isMember(x_i));
DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
++(d_statistics.d_statUpdates);
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
- d_activityMonitor.increaseActivity(x_j, 1);
+ d_activityMonitor[x_j] += 1;
checkBasicVariable(x_j);
}
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
- d_activityMonitor.increaseActivity(x_j, 1);
+ d_activityMonitor[x_j] += 1;
checkBasicVariable(x_k);
}
while(!d_possiblyInconsistent.empty()){
ArithVar var = d_possiblyInconsistent.top();
Debug("arith_update") << "possiblyInconsistent var" << var << endl;
- if(d_basicManager.isBasic(var)){
+ if(d_basicManager.isMember(var)){
if(!d_partialModel.assignmentIsConsistent(var)){
return var;
}
for (ArithVar i = 0; i < d_variables.size(); ++ i) {
Debug("arith::print_model") << d_variables[i] << " : " <<
d_partialModel.getAssignment(i);
- if(d_basicManager.isBasic(i))
+ if(d_basicManager.isMember(i))
Debug("arith::print_model") << " (basic)";
Debug("arith::print_model") << endl;
}
#include "expr/node.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/basic.h"
-#include "theory/arith/arith_activity.h"
+#include "theory/arith/arithvar_dense_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
-#include "theory/arith/next_arith_rewriter.h"
+#include "theory/arith/arith_rewriter.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/arith_propagator.h"
*/
ArithPartialModel d_partialModel;
- IsBasicManager d_basicManager;
+ ArithVarDenseSet d_basicManager;
ActivityMonitor d_activityMonitor;
/**
/**
* The rewriter module for arithmetic.
*/
- NextArithRewriter d_nextRewriter;
+ ArithRewriter d_rewriter;
ArithUnatePropagator d_propagator;
* Plug in old rewrite to the new (pre,post)rewrite interface.
*/
RewriteResponse postRewrite(TNode n, bool topLevel) {
- return d_nextRewriter.postRewrite(n);
+ return d_rewriter.postRewrite(n);
}
/**
projects / cvc5.git / commitdiff