From 5321d62fce6c747fa9d11e9df5b2ef8c4e25de21 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 20 May 2010 22:51:48 +0000 Subject: [PATCH] Added the division symbol to the parser, and minimal support for it in TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real. --- src/parser/smt/Smt.g | 7 ++++--- src/theory/arith/arith_rewriter.cpp | 24 +++++++++++++++++++++++- src/theory/arith/arith_rewriter.h | 3 +++ src/theory/arith/kinds | 1 + src/theory/arith/partial_model.cpp | 4 +++- src/theory/arith/theory_arith.cpp | 18 +++++++++++++----- src/theory/arith/theory_arith.h | 27 ++++++++++++++++++++++++--- src/theory/theory_engine.h | 11 +++++++++-- test/regress/regress0/ite.smt2 | 7 ++++--- 9 files changed, 84 insertions(+), 18 deletions(-) diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index dde5d26eb..07dd3de5b 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -284,10 +284,11 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + | DIV_TOK { $kind = CVC4::kind::DIVISION; } // Bit-vectors | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } - | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } - | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } + | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } + | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } @@ -300,7 +301,7 @@ builtinOp[CVC4::Kind& kind] | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } - | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } + | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a20d187bd..13ee9183f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -253,7 +253,7 @@ Node ArithRewriter::rewritePlus(TNode t){ if(pnfs.size() == 1){ Node p_1 = *(pnfs.begin()); if(p_1[0].getConst() == d_constants->d_ONE){ - if(accumulator == 0){ // 0 + (* 1 var) |-> var + if(accumulator == d_constants->d_ZERO){ // 0 + (* 1 var) |-> var Node var = p_1[1]; return var; } @@ -386,6 +386,26 @@ Node ArithRewriter::rewriteMult(TNode t){ } } +Node ArithRewriter::rewriteConstantDiv(TNode t){ + Assert(t.getKind()== kind::DIVISION); + + Node reLeft = rewrite(t[0]); + Node reRight = rewrite(t[1]); + Assert(reLeft.getKind()== kind::CONST_RATIONAL); + Assert(reRight.getKind()== kind::CONST_RATIONAL); + + Rational num = reLeft.getConst(); + Rational den = reRight.getConst(); + + Assert(den != d_constants->d_ZERO); + + Rational div = num / den; + + Node result = mkRationalNode(div); + + return result; +} + Node ArithRewriter::rewriteTerm(TNode t){ if(t.getMetaKind() == kind::metakind::CONSTANT){ return coerceToRationalNode(t); @@ -395,6 +415,8 @@ Node ArithRewriter::rewriteTerm(TNode t){ return rewriteMult(t); }else if(t.getKind() == kind::PLUS){ return rewritePlus(t); + }else if(t.getKind() == kind::DIVISION){ + return rewriteConstantDiv(t); }else{ Unreachable(); return Node::null(); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index a2a8b1b4b..5d94d20a9 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -82,6 +82,9 @@ private: Node multPnfByNonZero(TNode pnf, Rational& q); + Node rewriteConstantDiv(TNode t); + + public: ArithRewriter(ArithConstants* ac) : d_constants(ac) diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index fafa33a68..99f7258da 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -10,6 +10,7 @@ operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" +operator DIVISION 2 "arithmetic division" constant CONST_RATIONAL \ ::CVC4::Rational \ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index e3347df64..4ac03c904 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -12,12 +12,14 @@ using namespace CVC4::theory::arith::partial_model; void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; + d_UpperBoundMap[x] = r; } void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - + Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl; d_LowerBoundMap[x] = r; } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 390cb60aa..66883161e 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,15 +31,20 @@ using namespace CVC4::theory::arith; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : Theory(c, out), + d_preprocessed(c), d_constants(NodeManager::currentNM()), d_partialModel(c), d_diseq(c), - d_preprocessed(c), d_rewriter(&d_constants) { uint64_t ass_id = partial_model::Assignment::getId(); - Debug("arithsetup") << "Assignment: " << ass_id - << std::endl; + Debug("arithsetup") << "Assignment: " << ass_id << std::endl; +} +TheoryArith::~TheoryArith(){ + for(vector::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ + Node var = *i; + Debug("arithgc") << var << endl; + } } @@ -87,13 +92,14 @@ Node TheoryArith::rewrite(TNode n){ return result; } + void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; if(tn.getKind() == kind::BUILTIN) return; if(tn.getMetaKind() == metakind::VARIABLE){ - d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA); + setupVariable(tn); } //TODO is an atom @@ -115,7 +121,9 @@ void TheoryArith::registerTerm(TNode tn){ //TODO TypeNode real_type = NodeManager::currentNM()->realType(); slack = NodeManager::currentNM()->mkVar(real_type); - d_partialModel.setAssignment(slack,d_constants.d_ZERO_DELTA); + + setupVariable(slack); + left.setAttribute(Slack(), slack); makeBasic(slack); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ecdebd720..7bfa535a8 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -28,26 +28,40 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" +#include + namespace CVC4 { namespace theory { namespace arith { class TheoryArith : public Theory { private: - ArithConstants d_constants; - ArithPartialModel d_partialModel; + /* Chopping block begins */ - context::CDList d_diseq; context::CDList d_preprocessed; //TODO This is currently needed to save preprocessed nodes that may not //currently have an outisde reference. Get rid of when preprocessing is occuring //correctly. + std::vector d_variables; + //TODO get rid of this. Currently forces every variable and skolem constant that + // can hit the tableau to stay alive forever! + //This needs to come before d_partialModel and d_tableau in the file + + + /* Chopping block ends */ + ArithConstants d_constants; + ArithPartialModel d_partialModel; + + context::CDList d_diseq; Tableau d_tableau; ArithRewriter d_rewriter; + + public: TheoryArith(context::Context* c, OutputChannel& out); + ~TheoryArith(); Node rewrite(TNode n); @@ -74,6 +88,13 @@ private: //TODO get rid of this! Node simulatePreprocessing(TNode n); + void setupVariable(TNode x){ + Assert(x.getMetaKind() == kind::metakind::VARIABLE); + d_partialModel.setAssignment(x,d_constants.d_ZERO_DELTA); + d_variables.push_back(Node(x)); + + Debug("arithgc") << "setupVariable("<