diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 79 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 65 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.h | 58 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 14 |
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; } |