diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 30 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.cpp | 31 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.h | 8 |
4 files changed, 51 insertions, 26 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 460289439..5add52d1f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -24,6 +24,7 @@ #include "theory/rewriter.h" #include "expr/command.h" #include "theory/arrays/theory_arrays_instantiator.h" +#include "theory/model.h" using namespace std; @@ -57,7 +58,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_checkTimer("theory::arrays::checkTime"), d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"), d_ppFacts(u), - // d_ppCache(u), + // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), @@ -211,7 +212,7 @@ Node TheoryArrays::ppRewrite(TNode term) { for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; if (!ppDisequal(index_i, index_j)) { - Node hyp2(index_i.getType() == nm->booleanType()? + Node hyp2(index_i.getType() == nm->booleanType()? index_i.iffNode(index_j) : index_i.eqNode(index_j)); hyp << hyp2.notNode(); } @@ -623,27 +624,10 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - -Node TheoryArrays::getValue(TNode n) -{ - // TODO: Implement this - NodeManager* nodeManager = NodeManager::currentNM(); - - switch(n.getKind()) { - - case kind::VARIABLE: - Unhandled(kind::VARIABLE); - - case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - - default: - Unhandled(n.getKind()); - } +void TheoryArrays::collectModelInfo( TheoryModel* m ){ + m->assertEqualityEngine( &d_equalityEngine ); } - ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// @@ -663,7 +647,7 @@ void TheoryArrays::presolve() void TheoryArrays::check(Effort e) { TimerStat::CodeTimer codeTimer(d_checkTimer); - while (!done() && !d_conflict) + while (!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); @@ -1306,7 +1290,7 @@ void TheoryArrays::dischargeLemmas() d_equalityEngine.assertEquality(eq2, true, d_true); continue; } - + Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r); Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 25797dda3..6787f8ad8 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -219,7 +219,7 @@ class TheoryArrays : public Theory { private: public: - Node getValue(TNode n); + void collectModelInfo( TheoryModel* m ); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -346,6 +346,12 @@ class TheoryArrays : public Theory { void queueRowLemma(RowLemmaType lem); void dischargeLemmas(); + public: + + eq::EqualityEngine* getEqualityEngine() { + return &d_equalityEngine; + } + };/* class TheoryArrays */ }/* CVC4::theory::arrays namespace */ diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index 334d70eea..2e446c57f 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -51,6 +51,35 @@ void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort ef } -int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){ +int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){ return InstStrategy::STATUS_SAT; } + +bool InstantiatorTheoryArrays::hasTerm( Node a ){ + return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a ); +} + +bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b ); + }else{ + return a==b; + } +} + +bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false ); + }else{ + return false; + } +} + +Node InstantiatorTheoryArrays::getRepresentative( Node a ){ + if( hasTerm( a ) ){ + return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a ); + }else{ + return a; + } +} + diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h index 6a7c9c3ed..ade43fdb0 100644 --- a/src/theory/arrays/theory_arrays_instantiator.h +++ b/src/theory/arrays/theory_arrays_instantiator.h @@ -32,7 +32,7 @@ protected: /** reset instantiation round */ void processResetInstantiationRound( Theory::Effort effort ); /** process quantifier */ - int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ); + int process( Node f, Theory::Effort effort, int e ); public: InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th); ~InstantiatorTheoryArrays() {} @@ -42,6 +42,12 @@ public: void assertNode( Node assertion ); /** identify */ std::string identify() const { return std::string("InstantiatorTheoryArrays"); } +public: + /** general queries about equality */ + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + Node getRepresentative( Node a ); };/* class Instantiatior */ } |