summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/Makefile.am4
-rw-r--r--src/theory/arrays/theory_arrays.cpp79
-rw-r--r--src/theory/arrays/theory_arrays_model.cpp65
-rw-r--r--src/theory/arrays/theory_arrays_model.h58
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h14
5 files changed, 58 insertions, 162 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index ec834522f..77f102cf8 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -16,9 +16,7 @@ libarrays_la_SOURCES = \
array_info.h \
array_info.cpp \
static_fact_manager.h \
- static_fact_manager.cpp \
- theory_arrays_model.h \
- theory_arrays_model.cpp
+ static_fact_manager.cpp
EXTRA_DIST = \
kinds
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 801893107..98346d0e3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,7 +21,6 @@
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/arrays/theory_arrays_model.h"
#include "theory/model.h"
#include "theory/arrays/options.h"
#include "smt/logic_exception.h"
@@ -464,7 +463,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
}
case kind::STORE: {
// Invariant: array terms should be preregistered before being added to the equality engine
- Assert(!d_equalityEngine.hasTerm(node));
+ if (d_equalityEngine.hasTerm(node)) {
+ break;
+ }
d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
TNode a = d_equalityEngine.getRepresentative(node[0]);
@@ -493,7 +494,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
}
case kind::STORE_ALL: {
throw LogicException("Array theory solver does not yet support assertions using constant array value");
- }
+ }
default:
// Variables etc
if (node.getType().isArray()) {
@@ -588,7 +589,10 @@ void TheoryArrays::computeCareGraph()
}
}
}
- if (options::arraysModelBased()) return;
+ if (options::arraysModelBased()) {
+ checkModel(EFFORT_COMBINATION);
+ return;
+ }
if (d_sharedTerms) {
vector< pair<TNode, TNode> > currentPairs;
@@ -1009,7 +1013,7 @@ void TheoryArrays::checkModel(Effort e)
Assert(d_skolemAssertions.empty());
Assert(d_lemmas.empty());
- if (fullEffort(e)) {
+ if (combination(e)) {
// Add constraints for shared terms
context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2;
Node modelVal, modelVal2, d;
@@ -1061,9 +1065,10 @@ void TheoryArrays::checkModel(Effort e)
unsigned constraintIdx;
Node assertion, assertionToCheck;
vector<TNode> assumptions;
- // int numrestarts = 0;
- while (true) {
- // ++numrestarts;
+ int numrestarts = 0;
+ while (true || numrestarts < 1 || fullEffort(e) || combination(e)) {
+ ++numrestarts;
+ d_out->safePoint();
int level = getSatContext()->getLevel();
d_getModelValCache.clear();
for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
@@ -1076,7 +1081,7 @@ void TheoryArrays::checkModel(Effort e)
if (constraintIdx == d_modelConstraints.size()) {
break;
}
-
+
if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
if (assertionToCheck.getKind() == kind::AND &&
@@ -1202,20 +1207,20 @@ void TheoryArrays::checkModel(Effort e)
}
{
// generate lemma
- // if (all.size() == 0) {
- // d_lemmas.push_back(decision.negate());
- // }
- // else {
- // NodeBuilder<> disjunction(kind::OR);
- // std::set<TNode>::const_iterator it = all.begin();
- // std::set<TNode>::const_iterator it_end = all.end();
- // while (it != it_end) {
- // disjunction << (*it).negate();
- // ++it;
- // }
- // disjunction << decision.negate();
- // d_lemmas.push_back(disjunction);
- // }
+ if (all.size() == 0) {
+ d_lemmas.push_back(decision.negate());
+ }
+ else {
+ NodeBuilder<> disjunction(kind::OR);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ disjunction << (*it).negate();
+ ++it;
+ }
+ disjunction << decision.negate();
+ d_lemmas.push_back(disjunction);
+ }
}
d_equalityEngine.assertEquality(decision, eq, explanation);
if (!eq) decision = decision.notNode();
@@ -1268,6 +1273,13 @@ void TheoryArrays::checkModel(Effort e)
}
d_skolemIndex = d_skolemIndex + 1;
}
+ // Reregister stores
+ if (assertionToCheck != assertion &&
+ assertionToCheck.getKind() == kind::AND &&
+ assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) {
+ TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0];
+ preRegisterStores(s);
+ }
}
if (d_conflict) {
break;
@@ -1294,10 +1306,10 @@ void TheoryArrays::checkModel(Effort e)
d_skolemIndex = 0;
while (!d_lemmas.empty()) {
Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl;
- d_out->lemma(d_lemmas.back());
+ d_out->splitLemma(d_lemmas.back());
#ifdef CVC4_ASSERTIONS
- Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end());
- d_lemmasSaved.insert(d_lemmas.back());
+ // Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end());
+ // d_lemmasSaved.insert(d_lemmas.back());
#endif
d_lemmas.pop_back();
}
@@ -1416,7 +1428,7 @@ Node TheoryArrays::getModelValRec(TNode node)
}
++d_numGetModelValConflicts;
getSatContext()->pop();
- }
+ }
++te;
if (te.isFinished()) {
Assert(false);
@@ -1453,7 +1465,7 @@ bool TheoryArrays::hasLoop(TNode node, TNode target)
return true;
}
}
-
+
return false;
}
@@ -1633,9 +1645,14 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain,
return true;
}
}
- getSatContext()->push();
Node d = node.eqNode(val);
- d_decisions.push_back(invert ? d.notNode() : d);
+ Node r = Rewriter::rewrite(d);
+ if (r.isConst()) {
+ d_equalityEngine.assertEquality(d, r == d_true, d_true);
+ return ((r == d_true) == (!invert));
+ }
+ getSatContext()->push();
+ d_decisions.push_back(invert ? d.negate() : d);
d_equalityEngine.assertEquality(d, !invert, d_decisions.back());
Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl;
++d_numSetModelValSplits;
@@ -1667,7 +1684,7 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain,
d_decisions.pop_back();
d_permRef.push_back(explanation);
d = d.negate();
- Debug("arrays-model-based") << "Asserting learned literal " << d << " with explanation " << explanation << endl;
+ Debug("arrays-model-based") << "Asserting learned literal2 " << d << " with explanation " << explanation << endl;
bool eq = true;
if (d.getKind() == kind::NOT) {
d = d[0];
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
deleted file mode 100644
index b5c81ef69..000000000
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/********************* */
-/*! \file theory_arrays_model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_model class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_model.h"
-#include "theory/model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-ArrayModel::ArrayModel( Node arr, TheoryModel* m ) : d_arr( arr ){
- d_base_arr = arr;
- while( d_base_arr.getKind()==STORE ){
- Node ri = m->getRepresentative( d_base_arr[1] );
- if( d_values.find( ri )==d_values.end() ){
- d_values[ ri ] = m->getRepresentative( d_base_arr[2] );
- }
- d_base_arr = d_base_arr[0];
- }
-}
-
-Node ArrayModel::getValue( TheoryModel* m, Node i ){
- i = m->getRepresentative( i );
- std::map< Node, Node >::iterator it = d_values.find( i );
- if( it!=d_values.end() ){
- return it->second;
- }else{
- return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
- //return d_default_value; //TODO: guarantee I can return this here
- }
-}
-
-void ArrayModel::setValue( TheoryModel* m, Node i, Node e ){
- Node ri = m->getRepresentative( i );
- if( d_values.find( ri )==d_values.end() ){
- d_values[ ri ] = m->getRepresentative( e );
- }
-}
-
-void ArrayModel::setDefaultArray( Node arr ){
- d_base_arr = arr;
-}
-
-Node ArrayModel::getArrayValue(){
- Node curr = d_base_arr;
- for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
- curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
- }
- return curr;
-}
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
deleted file mode 100644
index 66dc80568..000000000
--- a/src/theory/arrays/theory_arrays_model.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/********************* */
-/*! \file theory_arrays_model.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief MODEL for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
-#define __CVC4__THEORY_ARRAYS_MODEL_H
-
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class TheoryModel;
-
-namespace arrays {
-
-class ArrayModel{
-protected:
- /** the array this model is for */
- Node d_arr;
-public:
- ArrayModel(){}
- ArrayModel( Node arr, TheoryModel* m );
- ~ArrayModel() {}
-public:
- /** pre-defined values */
- std::map< Node, Node > d_values;
- /** base array */
- Node d_base_arr;
- /** get value, return arguments that the value depends on */
- Node getValue( TheoryModel* m, Node i );
- /** set value */
- void setValue( TheoryModel* m, Node i, Node e );
- /** set default */
- void setDefaultArray( Node arr );
-public:
- /** get array value */
- Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
-#endif \ No newline at end of file
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 18bbef8cf..5df06bda8 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -36,6 +36,10 @@ namespace attr {
typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+static inline Node mkEqNode(Node a, Node b) {
+ return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
+}
+
class TheoryArraysRewriter {
static Node normalizeConstant(TNode node) {
return normalizeConstant(node, node[1].getType().getCardinality());
@@ -244,7 +248,7 @@ public:
val = false;
}
else {
- n = Rewriter::rewrite(store[1].eqNode(index));
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
if (n.getKind() != kind::CONST_BOOLEAN) {
break;
}
@@ -301,7 +305,7 @@ public:
val = false;
}
else {
- Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index));
+ Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
return RewriteResponse(REWRITE_DONE, node);
@@ -340,7 +344,7 @@ public:
val = false;
}
else {
- n = Rewriter::rewrite(store[1].eqNode(index));
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
if (n.getKind() != kind::CONST_BOOLEAN) {
break;
}
@@ -416,7 +420,7 @@ public:
val = false;
}
else {
- n = Rewriter::rewrite(store[1].eqNode(index));
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
if (n.getKind() != kind::CONST_BOOLEAN) {
break;
}
@@ -466,7 +470,7 @@ public:
val = false;
}
else {
- Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index));
+ Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
break;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback