summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt/Smt.g7
-rw-r--r--src/theory/arith/arith_rewriter.cpp24
-rw-r--r--src/theory/arith/arith_rewriter.h3
-rw-r--r--src/theory/arith/kinds1
-rw-r--r--src/theory/arith/partial_model.cpp4
-rw-r--r--src/theory/arith/theory_arith.cpp18
-rw-r--r--src/theory/arith/theory_arith.h27
-rw-r--r--src/theory/theory_engine.h11
-rw-r--r--test/regress/regress0/ite.smt27
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<Rational>() == 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>();
+ Rational den = reRight.getConst<Rational>();
+
+ 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<Node>::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 <vector>
+
namespace CVC4 {
namespace theory {
namespace arith {
class TheoryArith : public Theory {
private:
- ArithConstants d_constants;
- ArithPartialModel d_partialModel;
+ /* Chopping block begins */
- context::CDList<Node> d_diseq;
context::CDList<Node> 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<Node> 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<Node> 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("<<x<<")"<<std::endl;
+ };
};
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b559da562..c8b93e8b4 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -221,8 +221,15 @@ public:
if(lhs.getKind() == kind::VARIABLE) {
// FIXME: we don't yet have a Type-to-Theory map. When we do,
// look up the type of the LHS and return that Theory (?)
- return &d_uf;
- //Unimplemented();
+
+ //The following JUST hacks around this lack of a table
+ TypeNode type_of_n = lhs.getType();
+ if(type_of_n.isReal()){
+ return &d_arith;
+ }else{
+ return &d_uf;
+ //Unimplemented();
+ }
} else {
return theoryOf(lhs);
}
diff --git a/test/regress/regress0/ite.smt2 b/test/regress/regress0/ite.smt2
index 0e171666f..99f170ff4 100644
--- a/test/regress/regress0/ite.smt2
+++ b/test/regress/regress0/ite.smt2
@@ -1,6 +1,7 @@
-(set-logic QF_LRA)
+(set-logic QF_UF)
(set-info :status unsat)
-(declare-fun x () Real)
-(declare-fun y () Real)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
(assert (not (= x (ite true x y))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback