diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/delta_rational.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 4 | ||||
-rw-r--r-- | src/theory/arith/tableau.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 76 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 |
6 files changed, 89 insertions, 11 deletions
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index f6a460fee..d0e4ed1f4 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -24,12 +24,12 @@ using namespace std; using namespace CVC4; std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){ - return os << "(" << dq.getNoninfintestimalPart() - << "," << dq.getInfintestimalPart() << ")"; + return os << "(" << dq.getNoninfinitesimalPart() + << "," << dq.getInfinitesimalPart() << ")"; } std::string DeltaRational::toString() const { - return "(" + getNoninfintestimalPart().toString() + "," + - getInfintestimalPart().toString() + ")"; + return "(" + getNoninfinitesimalPart().toString() + "," + + getInfinitesimalPart().toString() + ")"; } diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 26212ec66..b75f5334c 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -46,11 +46,11 @@ public: DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) : c(base), k(coeff) {} - const CVC4::Rational& getInfintestimalPart() const { + const CVC4::Rational& getInfinitesimalPart() const { return k; } - const CVC4::Rational& getNoninfintestimalPart() const { + const CVC4::Rational& getNoninfinitesimalPart() const { return c; } diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index aaeadb629..d6a30ac91 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -48,7 +48,7 @@ Row::Row(ArithVar basic, Assert(d_coeffs[var_i] != Rational(0,1)); } } -void Row::subsitute(Row& row_s){ +void Row::substitute(Row& row_s){ ArithVar x_s = row_s.basicVar(); Assert(has(x_s)); @@ -133,7 +133,7 @@ void Tableau::addRow(ArithVar basicVar, Assert(isActiveBasicVariable(var)); Row* row_var = lookup(var); - row_current->subsitute(*row_var); + row_current->substitute(*row_var); } } } @@ -163,7 +163,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Row* row_k = lookup(basic); if(row_k->has(x_s)){ d_activityMonitor.increaseActivity(basic, 30); - row_k->subsitute(*row_s); + row_k->substitute(*row_s); } } } @@ -189,7 +189,7 @@ void Tableau::updateRow(Row* row){ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); - row->subsitute(*row_var); + row->substitute(*row_var); i = row->begin(); endIter = row->end(); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index a69493ee0..88a5c2317 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -83,7 +83,7 @@ public: void pivot(ArithVar x_j); - void subsitute(Row& row_s); + void substitute(Row& row_s); void printRow(); }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26bb58e90..ac3dc3d40 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -22,6 +22,8 @@ #include "expr/metakind.h" #include "expr/node_builder.h" +#include "theory/theory_engine.h" + #include "util/rational.h" #include "util/integer.h" @@ -927,3 +929,77 @@ void TheoryArith::propagate(Effort e) { } } } + +Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + case kind::VARIABLE: { + DeltaRational drat = d_partialModel.getAssignment(asArithVar(n)); + // FIXME our infinitesimal is fixed here at 1e-06 + return nodeManager-> + mkConst( drat.getNoninfinitesimalPart() + + drat.getInfinitesimalPart() * Rational(1, 1000000) ); + } + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + case kind::PLUS: { // 2+ args + Rational value = d_constants.d_ZERO; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value += engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MULT: { // 2+ args + Rational value = d_constants.d_ONE; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value *= engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MINUS: // 2 args + // should have been rewritten + Unreachable(); + + case kind::UMINUS: // 1 arg + // should have been rewritten + Unreachable(); + + case kind::DIVISION: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() / + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::IDENTITY: // 1 arg + return engine->getValue(n[0]); + + case kind::LT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() < + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::LEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <= + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() > + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >= + engine->getValue(n[1]).getConst<Rational>() ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index cbfdf27f3..26dcc9825 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -128,6 +128,8 @@ public: void propagate(Effort e); void explain(TNode n, Effort e); + Node getValue(TNode n, TheoryEngine* engine); + void shutdown(){ } std::string identify() const { return std::string("TheoryArith"); } |