summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/cnf_stream.cpp7
-rw-r--r--src/theory/arith/tableau.h20
-rw-r--r--src/theory/arith/theory_arith.cpp56
-rw-r--r--src/theory/arith/theory_arith.h6
-rw-r--r--src/theory/booleans/theory_bool.h11
-rw-r--r--src/theory/output_channel.h20
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--src/theory/theory_engine.h17
8 files changed, 114 insertions, 26 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51ae695cf..a245eb469 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -359,6 +359,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
}
if(somethingChanged) {
+
rewrite = nodeManager->mkNode(node.getKind(), newChildren);
nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
return rewrite;
@@ -399,7 +400,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
case AND:
return handleAnd(node);
default:
- return handleAtom(handleNonAtomicNode(node));
+ {
+ Node atomic = handleNonAtomicNode(node);
+ AlwaysAssert(isCached(atomic) || atomic.isAtomic());
+ return toCNF(atomic);
+ }
}
}
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 7237c3a54..fa0712e7e 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -36,6 +36,7 @@ public:
//TODO Assert(d_x_i.getType() == REAL);
Assert(sum.getKind() == PLUS);
+ Rational zero(0,1);
for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
TNode pair = *iter;
@@ -48,7 +49,10 @@ public:
//TODO Assert(var_i.getKind() == REAL);
Assert(!has(var_i));
d_nonbasic.insert(var_i);
- d_coeffs[var_i] = coeff.getConst<Rational>();
+ Rational q = coeff.getConst<Rational>();
+ d_coeffs[var_i] = q;
+ Assert(q != zero);
+ Assert(d_coeffs[var_i] != zero);
}
}
@@ -66,12 +70,13 @@ public:
bool has(TNode x_j){
CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-
return x_jPos != d_coeffs.end();
}
Rational& lookup(TNode x_j){
- return d_coeffs[x_j];
+ CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
+ Assert(x_jPos != d_coeffs.end());
+ return (*x_jPos).second;
}
void pivot(TNode x_j){
@@ -89,17 +94,22 @@ public:
TNode nb = *nonbasicIter;
d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs;
}
+
}
void subsitute(Row& row_s){
TNode x_s = row_s.basicVar();
Assert(has(x_s));
+ Assert(d_nonbasic.find(x_s) != d_nonbasic.end());
Assert(x_s != d_x_i);
+ Rational zero(0,1);
Rational a_rs = lookup(x_s);
+ Assert(a_rs != zero);
d_coeffs.erase(x_s);
+ d_nonbasic.erase(x_s);
for(std::set<TNode>::iterator iter = row_s.d_nonbasic.begin();
iter != row_s.d_nonbasic.end();
@@ -108,6 +118,10 @@ public:
Rational a_sj = a_rs * row_s.lookup(x_j);
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;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ff74f0f9..08b609ba4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -29,6 +29,10 @@ using namespace CVC4::kind;
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+struct EagerSplittingTag {};
+typedef expr::Attribute<EagerSplittingTag, bool> EagerlySplitUpon;
+
+
TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
Theory(c, out),
d_preprocessed(c),
@@ -47,6 +51,29 @@ TheoryArith::~TheoryArith(){
}
}
+void TheoryArith::preRegisterTerm(TNode n) {
+ Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
+ << n << ")" << endl;
+
+ if(n.getKind() == EQUAL){
+ if(!n.getAttribute(EagerlySplitUpon())){
+ TNode left = n[0];
+ TNode right = n[1];
+
+ Node lt = NodeManager::currentNM()->mkNode(LT, left,right);
+ Node gt = NodeManager::currentNM()->mkNode(GT, left,right);
+ Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt);
+
+ d_splits.push_back(eagerSplit);
+
+ n.setAttribute(EagerlySplitUpon(), true);
+ d_out->augmentingLemma(eagerSplit);
+ }
+ }
+
+ Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+ << n << ")" << endl;
+}
bool isBasicSum(TNode n){
if(n.getKind() != kind::PLUS) return false;
@@ -220,11 +247,13 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
TNode x_j = *basicIter;
Row* row_j = d_tableau.lookup(x_j);
- Rational& a_ji = row_j->lookup(x_i);
+ if(row_j->has(x_i)){
+ Rational& a_ji = row_j->lookup(x_i);
- DeltaRational assignment = d_partialModel.getAssignment(x_j);
- DeltaRational nAssignment = assignment+(diff * a_ji);
- d_partialModel.setAssignment(x_j, nAssignment);
+ DeltaRational assignment = d_partialModel.getAssignment(x_j);
+ DeltaRational nAssignment = assignment+(diff * a_ji);
+ d_partialModel.setAssignment(x_j, nAssignment);
+ }
}
d_partialModel.setAssignment(x_i, v);
@@ -252,7 +281,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
TNode x_k = *basicIter;
Row* row_k = d_tableau.lookup(x_k);
- if(x_k != x_i){
+ if(x_k != x_i && row_k->has(x_j)){
DeltaRational a_kj = row_k->lookup(x_j);
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta;
d_partialModel.setAssignment(x_k, nextAssignment);
@@ -321,7 +350,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
d_partialModel.beginRecordingAssignments();
while(true){
TNode x_i = selectSmallestInconsistentVar();
+ Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
if(x_i == Node::null()){
+ Debug("arith_update") << "No inconsistent variables" << endl;
d_partialModel.stopRecordingAssignments(false);
return Node::null(); //sat
}
@@ -509,6 +540,8 @@ void TheoryArith::check(Effort level){
if(possibleConflict != Node::null()){
Debug("arith") << "Found a conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
+ }else{
+ Debug("arith") << "No conflict found" << endl;
}
}
@@ -516,22 +549,33 @@ void TheoryArith::check(Effort level){
bool enqueuedCaseSplit = false;
typedef context::CDList<Node>::const_iterator diseq_iterator;
for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
+
Node assertion = *i;
+ Debug("arith") << "splitting" << assertion << endl;
TNode eq = assertion[0];
TNode x_i = eq[0];
TNode c_i = eq[1];
DeltaRational constant = c_i.getConst<Rational>();
+ Debug("arith") << "broken apart" << endl;
if(d_partialModel.getAssignment(x_i) == constant){
+ Debug("arith") << "here" << endl;
enqueuedCaseSplit = true;
Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
//d_out->enqueueCaseSplits(caseSplit);
+ Debug("arith") << "finished" << caseSplit << endl;
}
+ Debug("arith") << "end of for loop" << endl;
+
}
+ Debug("arith") << "finished" << endl;
+
if(enqueuedCaseSplit){
//d_out->caseSplit();
- Warning() << "Outstanding case split in theory arith" << endl;
+ //Warning() << "Outstanding case split in theory arith" << endl;
}
}
+ Debug("arith") << "TheoryArith::check end" << std::endl;
+
}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7bfa535a8..1d6cca5cc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,6 +38,10 @@ class TheoryArith : public Theory {
private:
/* Chopping block begins */
+ std::vector<Node> d_splits;
+ //This stores the eager splits sent out of the theory.
+ //TODO get rid of this.
+
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
@@ -65,7 +69,7 @@ public:
Node rewrite(TNode n);
- void preRegisterTerm(TNode n) { Unimplemented(); }
+ void preRegisterTerm(TNode n);
void registerTerm(TNode n);
void check(Effort e);
void propagate(Effort e) { Unimplemented(); }
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index eb6e84c39..b39663449 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -31,11 +31,18 @@ public:
Theory(c, out) {
}
- void preRegisterTerm(TNode n) { Unimplemented(); }
- void registerTerm(TNode n) { Unimplemented(); }
+ void preRegisterTerm(TNode n) {
+ Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+ Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+ }
+ void registerTerm(TNode n) {
+ Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+ Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+ }
void check(Effort e) { Unimplemented(); }
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
+
};
}/* CVC4::theory::booleans namespace */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 54fa71808..08a3353e6 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -18,6 +18,7 @@
#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
#define __CVC4__THEORY__OUTPUT_CHANNEL_H
+#include "util/Assert.h"
#include "theory/interrupted.h"
namespace CVC4 {
@@ -53,7 +54,7 @@ public:
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
*/
- virtual void safePoint() throw(Interrupted) {
+ virtual void safePoint() throw(Interrupted, AssertionException) {
}
/**
@@ -66,7 +67,7 @@ public:
*
* @param safe - whether it is safe to be interrupted
*/
- virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0;
+ virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
/**
* Propagate a theory literal.
@@ -75,7 +76,7 @@ public:
*
* @param safe - whether it is safe to be interrupted
*/
- virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0;
+ virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
/**
* Tell the core that a valid theory lemma at decision level 0 has
@@ -84,7 +85,16 @@ public:
* @param n - a theory lemma valid at decision level 0
* @param safe - whether it is safe to be interrupted
*/
- virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0;
+ virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+
+ /**
+ * Tell the core to add the following valid lemma as if it were a user assertion.
+ * This should NOT be called during solving, only preprocessing.
+ *
+ * @param n - a theory lemma valid to be asserted
+ * @param safe - whether it is safe to be interrupted
+ */
+ virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
/**
* Provide an explanation in response to an explanation request.
@@ -92,7 +102,7 @@ public:
* @param n - an explanation
* @param safe - whether it is safe to be interrupted
*/
- virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0;
+ virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
};/* class OutputChannel */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d29195011..5af64c5dd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -32,8 +32,7 @@ typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
Node TheoryEngine::preprocess(TNode t) {
Node top = rewrite(t);
- Debug("rewrite") << "rewrote: " << t << "\nto : " << top << "\n";
- return top;
+ Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl;
list<TNode> toReg;
toReg.push_back(top);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e85e66e99..00336a1e3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -68,7 +68,7 @@ class TheoryEngine {
d_conflictNode(context) {
}
- void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted) {
+ void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
d_conflictNode = conflictNode;
if(safe) {
@@ -76,14 +76,16 @@ class TheoryEngine {
}
}
- void propagate(TNode, bool) throw(theory::Interrupted) {
+ void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) {
}
- void lemma(TNode node, bool) throw(theory::Interrupted) {
+ void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
d_engine->newLemma(node);
}
-
- void explanation(TNode, bool) throw(theory::Interrupted) {
+ void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+ d_engine->newAugmentingLemma(node);
+ }
+ void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) {
}
};
@@ -289,7 +291,10 @@ public:
inline void newLemma(TNode node) {
d_propEngine->assertLemma(node);
}
-
+ inline void newAugmentingLemma(TNode node) {
+ Node preprocessed = preprocess(node);
+ d_propEngine->assertFormula(preprocessed);
+ }
/**
* Returns the last conflict (if any).
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback