From: Tim King Date: Wed, 16 Jun 2010 20:26:14 +0000 (+0000) Subject: This commit just contains miscellaneous arithmetic cleanup. X-Git-Tag: cvc5-1.0.0~8985 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c237443e1fad0ab948f2acb97651dec4f0c34dae;p=cvc5.git This commit just contains miscellaneous arithmetic cleanup. --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2d96ac57a..7e0cfd0cf 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -313,6 +313,8 @@ public: Node mkVar(const TypeNode& type); Node* mkVarPtr(const TypeNode& type); + /** Create a skolem constant with the given type. */ + Node mkSkolem(const TypeNode& type); /** * Create a constant of type T. It will have the appropriate @@ -864,6 +866,12 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) { return n; } +inline Node NodeManager::mkSkolem(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::SKOLEM); + n.setAttribute(TypeAttr(), type); + return n; +} + template Node NodeManager::mkConst(const T& val) { return mkConstInternal(val); diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 60db60c1a..78d5fb665 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -60,7 +60,7 @@ public: return DeltaRational(tmpC, tmpK); } - DeltaRational operator*(CVC4::Rational& a) const{ + DeltaRational operator*(const Rational& a) const{ CVC4::Rational tmpC = a*c; CVC4::Rational tmpK = a*k; return DeltaRational(tmpC, tmpK); @@ -95,7 +95,7 @@ public: return *(this); } - DeltaRational& operator*=(CVC4::Rational& a){ + DeltaRational& operator*=(const CVC4::Rational& a){ c = c * a; k = k * a; diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index bb2864cf9..e7e3f8bc2 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -175,7 +175,7 @@ bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool st return false; } - DeltaRational l = (*i).second; + const DeltaRational& l = (*i).second; if(strict){ return c < l; @@ -191,7 +191,7 @@ bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool st // ? u < -\infty |- _|_ return false; } - DeltaRational u = (*i).second; + const DeltaRational& u = (*i).second; if(strict){ return c > u; @@ -208,9 +208,9 @@ bool ArithPartialModel::strictlyBelowUpperBound(TNode x){ if(i == d_UpperBoundMap.end()){// u = \infty return true; } - DeltaRational u = (*i).second; - return *assign < u; + const DeltaRational& u = (*i).second; + return (*assign) < u; } bool ArithPartialModel::strictlyAboveLowerBound(TNode x){ @@ -221,7 +221,8 @@ bool ArithPartialModel::strictlyAboveLowerBound(TNode x){ if(i == d_LowerBoundMap.end()){// l = \infty return true; } - DeltaRational l = (*i).second; + + const DeltaRational& l = (*i).second; return l < *assign; } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 26f9a135b..0351abf9d 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -104,13 +104,11 @@ typedef expr::CDAttribute LowerConstraint; struct UpperConstraintAttrID {}; typedef expr::CDAttribute UpperConstraint; - -}; /*namespace partial_model*/ - - struct TheoryArithPropagatedID {}; typedef expr::CDAttribute TheoryArithPropagated; +}; /*namespace partial_model*/ + class ArithPartialModel { diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index a5499db08..0cadc8d10 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -44,27 +44,29 @@ class Row { public: + typedef std::set::iterator iterator; + /** * Construct a row equal to: * basic = \sum_{x_i} c_i * x_i */ - Row(TNode basic, TNode sum): d_x_i(basic),d_nonbasic(), d_coeffs(){ - using namespace CVC4::kind; - - Assert(d_x_i.getMetaKind() == CVC4::kind::metakind::VARIABLE); + Row(TNode basic, TNode sum): + d_x_i(basic), + d_nonbasic(), + d_coeffs(){ - //TODO Assert(d_x_i.getType() == REAL); - Assert(sum.getKind() == PLUS); + Assert(d_x_i.getMetaKind() == kind::metakind::VARIABLE); + Assert(sum.getKind() == kind::PLUS); for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){ TNode pair = *iter; - Assert(pair.getKind() == MULT); + Assert(pair.getKind() == kind::MULT); Assert(pair.getNumChildren() == 2); TNode coeff = pair[0]; TNode var_i = pair[1]; - Assert(coeff.getKind() == CONST_RATIONAL); - Assert(var_i.getKind() == VARIABLE); - //TODO Assert(var_i.getKind() == REAL); + Assert(coeff.getKind() == kind::CONST_RATIONAL); + Assert(var_i.getKind() == kind::VARIABLE); + Assert(!has(var_i)); d_nonbasic.insert(var_i); d_coeffs[var_i] = coeff.getConst(); @@ -73,11 +75,11 @@ public: } } - std::set::iterator begin(){ + iterator begin(){ return d_nonbasic.begin(); } - std::set::iterator end(){ + iterator end(){ return d_nonbasic.end(); } @@ -90,7 +92,7 @@ public: return x_jPos != d_coeffs.end(); } - Rational& lookup(TNode x_j){ + const Rational& lookup(TNode x_j){ CoefficientTable::iterator x_jPos = d_coeffs.find(x_j); Assert(x_jPos != d_coeffs.end()); return (*x_jPos).second; @@ -105,11 +107,11 @@ public: d_nonbasic.insert(d_x_i); d_x_i = x_j; - for(std::set::iterator nonbasicIter = d_nonbasic.begin(); + for(iterator nonbasicIter = d_nonbasic.begin(); nonbasicIter != d_nonbasic.end(); ++nonbasicIter){ TNode nb = *nonbasicIter; - d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs; + d_coeffs[nb] *= negInverseA_rs; } } @@ -128,7 +130,7 @@ public: d_coeffs.erase(x_s); d_nonbasic.erase(x_s); - for(std::set::iterator iter = row_s.d_nonbasic.begin(); + for(iterator iter = row_s.d_nonbasic.begin(); iter != row_s.d_nonbasic.end(); ++iter){ TNode x_j = *iter; @@ -146,24 +148,12 @@ public: d_nonbasic.insert(x_j); d_coeffs.insert(make_pair(x_j,a_sj)); } - /* - if(has(x_j)){ - d_coeffs[x_j] = d_coeffs[x_j] + a_sj; - if(d_coeffs[x_j] == zero){ - d_coeffs.erase(x_j); - d_nonbasic.erase(x_j); - } - }else{ - d_nonbasic.insert(x_j); - d_coeffs[x_j] = a_sj; - } - */ } } void printRow(){ Debug("tableau") << d_x_i << " "; - for(std::set::iterator nonbasicIter = d_nonbasic.begin(); + for(iterator nonbasicIter = d_nonbasic.begin(); nonbasicIter != d_nonbasic.end(); ++nonbasicIter){ TNode nb = *nonbasicIter; @@ -183,9 +173,6 @@ private: VarSet d_basicVars; RowsTable d_rows; - inline bool contains(TNode var){ - return d_basicVars.find(var) != d_basicVars.end(); - } public: /** @@ -206,43 +193,6 @@ public: return d_rows[var]; } - /** - * Iterator for the tableau. Iterates over rows. - */ - /* TODO add back in =( - class iterator { - private: - const Tableau* table_ref; - VarSet::iterator variableIter; - - iterator(const Tableau* tr, VarSet::iterator& i) : - table_ref(tr), variableIter(i){} - - public: - void operator++(){ - ++variableIter; - } - - bool operator==(iterator& other){ - return variableIter == other.variableIter; - } - bool operator!=(iterator& other){ - return variableIter != other.variableIter; - } - - Row& operator*() const{ - TNode var = *variableIter; - RowsTable::iterator iter = table_ref->d_rows.find(var); - return *iter; - } - }; - iterator begin(){ - return iterator(this, d_basicVars.begin()); - } - iterator end(){ - return iterator(this, d_basicVars.end()); - }*/ - void addRow(TNode eq){ Assert(eq.getKind() == kind::EQUAL); Assert(eq.getNumChildren() == 2); @@ -250,7 +200,6 @@ public: TNode var = eq[0]; TNode sum = eq[1]; - //Assert(isAdmissableVariable(var)); Assert(var.getAttribute(IsBasic())); //The new basic variable cannot already be a basic variable @@ -260,9 +209,9 @@ public: d_rows[var] = row_var; //A variable in the row may have been made non-basic already. - //fake the pivot of this variable + //If this is the case we fake pivoting this variable for(TNode::iterator sumIter = sum.begin(); sumIter!=sum.end(); ++sumIter){ - TNode child = *sumIter; //(MULT (CONST_RATIONAL 1998/1001) x_5) + TNode child = *sumIter; Assert(child.getKind() == kind::MULT); Assert(child.getNumChildren() == 2); Assert(child[0].getKind() == kind::CONST_RATIONAL); @@ -315,6 +264,10 @@ public: row_k->printRow(); } } +private: + inline bool contains(TNode var){ + return d_basicVars.find(var) != d_basicVars.end(); + } }; }; /* namespace arith */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 5d5313b76..2f62c8bc1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -162,7 +162,6 @@ void TheoryArith::setupSlack(TNode left){ makeBasic(slack); Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); - slackEqLeft.setAttribute(TheoryArithPropagated(), true); Debug("slack") << "slack " << slackEqLeft << endl; @@ -223,7 +222,7 @@ DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){ Row* row = d_tableau.lookup(x); for(std::set::iterator i = row->begin(); i != row->end();++i){ TNode nonbasic = *i; - Rational& coeff = row->lookup(nonbasic); + const Rational& coeff = row->lookup(nonbasic); DeltaRational assignment = d_partialModel.getAssignment(nonbasic); sum = sum + (assignment * coeff); } @@ -240,7 +239,7 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ Row* row = d_tableau.lookup(x); for(std::set::iterator i = row->begin(); i != row->end();++i){ TNode nonbasic = *i; - Rational& coeff = row->lookup(nonbasic); + const Rational& coeff = row->lookup(nonbasic); DeltaRational assignment = d_partialModel.getSafeAssignment(nonbasic); sum = sum + (assignment * coeff); } @@ -350,7 +349,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ Row* row_j = d_tableau.lookup(x_j); if(row_j->has(x_i)){ - Rational& a_ji = row_j->lookup(x_i); + const Rational& a_ji = row_j->lookup(x_i); DeltaRational assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); @@ -370,7 +369,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ Assert(x_i != x_j); Row* row_i = d_tableau.lookup(x_i); - Rational& a_ij = row_i->lookup(x_j); + const Rational& a_ij = row_i->lookup(x_j); DeltaRational betaX_i = d_partialModel.getAssignment(x_i); @@ -527,7 +526,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ TNode nonbasic = *nbi; - Rational& a_ij = row_i->lookup(nonbasic); + const Rational& a_ij = row_i->lookup(nonbasic); Assert(a_ij != d_constants.d_ZERO); @@ -565,7 +564,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ for(NonBasicIter nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ TNode nonbasic = *nbi; - Rational& a_ij = row_i->lookup(nonbasic); + const Rational& a_ij = row_i->lookup(nonbasic); Assert(a_ij != d_constants.d_ZERO); @@ -765,7 +764,7 @@ void TheoryArith::checkTableau(){ nonbasicIter != row_k->end(); ++nonbasicIter){ TNode nonbasic = *nonbasicIter; - Rational& coeff = row_k->lookup(nonbasic); + const Rational& coeff = row_k->lookup(nonbasic); DeltaRational beta = d_partialModel.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff<