From: Tim King Date: Thu, 20 May 2010 22:51:48 +0000 (+0000) Subject: Added the division symbol to the parser, and minimal support for it in TheoryArith... X-Git-Tag: cvc5-1.0.0~9055 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5321d62fce6c747fa9d11e9df5b2ef8c4e25de21;p=cvc5.git 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. --- 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("<