diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/model.cpp | 45 | ||||
-rw-r--r-- | src/theory/model.h | 16 |
2 files changed, 40 insertions, 21 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 826e729fc..3880aaad9 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -210,7 +210,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ } /** add term */ -void TheoryModel::addTerm( Node n ){ +void TheoryModel::addTerm(TNode n ){ Assert(d_equalityEngine.hasTerm(n)); //must collect UF terms if (n.getKind()==APPLY_UF) { @@ -223,7 +223,7 @@ void TheoryModel::addTerm( Node n ){ } /** assert equality */ -void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ +void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ if (a == b && polarity) { return; } @@ -233,7 +233,7 @@ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ } /** assert predicate */ -void TheoryModel::assertPredicate( Node a, bool polarity ){ +void TheoryModel::assertPredicate(TNode a, bool polarity ){ if ((a == d_true && polarity) || (a == d_false && (!polarity))) { return; @@ -263,6 +263,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* predFalse = ee->areEqual(eqc, d_false); } eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + bool first = true; + Node rep; for (; !eqc_i.isFinished(); ++eqc_i) { if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { continue; @@ -274,28 +276,43 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* else if (predFalse) { assertPredicate(*eqc_i, false); } - else if (eqc != (*eqc_i)) { - Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << eqc << "));" << endl; - d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null()); - Assert(d_equalityEngine.consistent()); + else { + if (first) { + rep = (*eqc_i); + first = false; + } + else { + Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; + d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null()); + Assert(d_equalityEngine.consistent()); + } } } else { - assertEquality(*eqc_i, eqc, true); + if (first) { + rep = (*eqc_i); + first = false; + } + else { + assertEquality(*eqc_i, rep, true); + } } } } } -void TheoryModel::assertRepresentative( Node n ){ +void TheoryModel::assertRepresentative(TNode n ) +{ Trace("model-builder-reps") << "Assert rep : " << n << std::endl; d_reps[ n ] = n; } -bool TheoryModel::hasTerm( Node a ){ +bool TheoryModel::hasTerm(TNode a) +{ return d_equalityEngine.hasTerm( a ); } -Node TheoryModel::getRepresentative( Node a ){ +Node TheoryModel::getRepresentative(TNode a) +{ if( d_equalityEngine.hasTerm( a ) ){ Node r = d_equalityEngine.getRepresentative( a ); if( d_reps.find( r )!=d_reps.end() ){ @@ -308,7 +325,8 @@ Node TheoryModel::getRepresentative( Node a ){ } } -bool TheoryModel::areEqual( Node a, Node b ){ +bool TheoryModel::areEqual(TNode a, TNode b) +{ if( a==b ){ return true; }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ @@ -318,7 +336,8 @@ bool TheoryModel::areEqual( Node a, Node b ){ } } -bool TheoryModel::areDisequal( Node a, Node b ){ +bool TheoryModel::areDisequal(TNode a, TNode b) +{ if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ return d_equalityEngine.areDisequal( a, b, false ); }else{ diff --git a/src/theory/model.h b/src/theory/model.h index 7ccbe2fc3..e283ee183 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -90,11 +90,11 @@ public: * such as contraining the interpretation of uninterpretted functions, * and adding n to the equality engine of this model */ - virtual void addTerm( Node n ); + virtual void addTerm(TNode n); /** assert equality holds in the model */ - void assertEquality( Node a, Node b, bool polarity ); + void assertEquality(TNode a, TNode b, bool polarity); /** assert predicate holds in the model */ - void assertPredicate( Node a, bool polarity ); + void assertPredicate(TNode a, bool polarity); /** assert all equalities/predicates in equality engine hold in the model */ void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL); /** assert representative @@ -103,13 +103,13 @@ public: * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) * functions where fullModel = true. */ - void assertRepresentative( Node n ); + void assertRepresentative(TNode n); public: /** general queries */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); + bool hasTerm(TNode a); + Node getRepresentative(TNode a); + bool areEqual(TNode a, TNode b); + bool areDisequal(TNode a, TNode b); public: /** get value function for Exprs. */ Expr getValue( Expr expr ) const; |