From: Clark Barrett Date: Thu, 24 Oct 2013 23:48:30 +0000 (-0700) Subject: Fix for bug515 X-Git-Tag: cvc5-1.0.0~7278^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0274d973ae504fa74fd73aa80c725a778581bb26;p=cvc5.git Fix for bug515 --- diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 840c8bc3a..393f3883c 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -28,17 +28,22 @@ using namespace CVC4::context; using namespace CVC4::theory; TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) : - d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) + d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + d_eeContext = new context::Context(); + d_equalityEngine = new eq::EqualityEngine(d_eeContext, name); + // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::APPLY_UF); - d_equalityEngine.addFunctionKind(kind::SELECT); - // d_equalityEngine.addFunctionKind(kind::STORE); - d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine->addFunctionKind(kind::APPLY_UF); + d_equalityEngine->addFunctionKind(kind::SELECT); + // d_equalityEngine->addFunctionKind(kind::STORE); + d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); + d_eeContext->push(); } void TheoryModel::reset(){ @@ -46,6 +51,8 @@ void TheoryModel::reset(){ d_rep_set.clear(); d_uf_terms.clear(); d_uf_models.clear(); + d_eeContext->pop(); + d_eeContext->push(); } Node TheoryModel::getValue(TNode n) const { @@ -98,7 +105,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) { + if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { return n; } else { n = Rewriter::rewrite(n); @@ -158,13 +165,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const return val; } - if (!d_equalityEngine.hasTerm(n)) { + if (!d_equalityEngine->hasTerm(n)) { // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); return *te; } } - Node val = d_equalityEngine.getRepresentative(n); + Node val = d_equalityEngine->getRepresentative(n); Assert(d_reps.find(val) != d_reps.end()); std::map< Node, Node >::const_iterator it = d_reps.find( val ); if( it!=d_reps.end() ){ @@ -237,7 +244,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ /** add term */ void TheoryModel::addTerm(TNode n ){ - Assert(d_equalityEngine.hasTerm(n)); + Assert(d_equalityEngine->hasTerm(n)); //must collect UF terms if (n.getKind()==APPLY_UF) { Node op = n.getOperator(); @@ -254,8 +261,8 @@ void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ return; } Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl; - d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } /** assert predicate */ @@ -266,11 +273,11 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){ } if (a.getKind() == EQUAL) { Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertEquality( a, polarity, Node::null() ); + d_equalityEngine->assertEquality( a, polarity, Node::null() ); } else { Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertPredicate( a, polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertPredicate( a, polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } } @@ -309,8 +316,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* } else { Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; - d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null()); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); + Assert(d_equalityEngine->consistent()); } } } else { @@ -334,13 +341,13 @@ void TheoryModel::assertRepresentative(TNode n ) bool TheoryModel::hasTerm(TNode a) { - return d_equalityEngine.hasTerm( a ); + return d_equalityEngine->hasTerm( a ); } Node TheoryModel::getRepresentative(TNode a) { - if( d_equalityEngine.hasTerm( a ) ){ - Node r = d_equalityEngine.getRepresentative( a ); + if( d_equalityEngine->hasTerm( a ) ){ + Node r = d_equalityEngine->getRepresentative( a ); if( d_reps.find( r )!=d_reps.end() ){ return d_reps[ r ]; }else{ @@ -355,8 +362,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) { if( a==b ){ return true; - }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areEqual( a, b ); + }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areEqual( a, b ); }else{ return false; } @@ -364,8 +371,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) bool TheoryModel::areDisequal(TNode a, TNode b) { - if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areDisequal( a, b, false ); + if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areDisequal( a, b, false ); }else{ return false; } @@ -422,7 +429,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac return; } if (isAssignable(n)) { - tm->d_equalityEngine.addTerm(n); + tm->d_equalityEngine->addTerm(n); } for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { checkTerms(*child_it, tm, cache); @@ -448,11 +455,11 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) d_te->collectModelInfo(tm, fullModel); // Loop through all terms and make sure that assignable sub-terms are in the equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); { NodeSet cache; for ( ; !eqcs_i.isFinished(); ++eqcs_i) { - eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { checkTerms(*eqc_i, tm, cache); } @@ -465,20 +472,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, Node > assertedReps, constantReps; TypeSet typeConstSet, typeRepSet, typeNoRepSet; std::set< TypeNode > allTypes; - eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); + eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Trace("model-builder") << "Processing EC: " << eqc << endl; - Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc); + Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc); TypeNode eqct = eqc.getType(); Assert(assertedReps.find(eqc) == assertedReps.end()); Assert(constantReps.find(eqc) == constantReps.end()); // Loop through terms in this EC Node rep, const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; Trace("model-builder") << " Processing Term: " << n << endl; @@ -556,7 +563,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) assignable = false; evaluable = false; evaluated = false; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; if (isAssignable(n)) { @@ -653,7 +660,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) for (i = noRepSet.begin(); i != noRepSet.end(); ) { i2 = i; ++i; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); assignable = false; evaluable = false; for ( ; !eqc_i.isFinished(); ++eqc_i) { @@ -744,7 +751,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) #ifdef CVC4_ASSERTIONS if (fullModel) { // Check that every term evaluates to its representative in the model - for (eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { + for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Node rep; @@ -757,7 +764,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(itMap != constantReps.end()); rep = itMap->second; } - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; static int repCheckInstance = 0; @@ -795,18 +802,19 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node bool childrenConst = true; for (size_t i=0; i < r.getNumChildren(); ++i) { Node ri = r[i]; + bool recurse = true; if (!ri.isConst()) { - if (m->d_equalityEngine.hasTerm(ri)) { - ri = m->d_equalityEngine.getRepresentative(ri); - itMap = constantReps.find(ri); + if (m->d_equalityEngine->hasTerm(ri)) { + itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri)); if (itMap != constantReps.end()) { ri = (*itMap).second; + recurse = false; } - else if (evalOnly) { - ri = normalize(m, r[i], constantReps, evalOnly); - } + else if (!evalOnly) { + recurse = false; + } } - else { + if (recurse) { ri = normalize(m, ri, constantReps, evalOnly); } if (!ri.isConst()) { diff --git a/src/theory/model.h b/src/theory/model.h index 03a641df4..a18d66ab0 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -42,8 +42,11 @@ protected: public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} + + /** special local context for our equalityEngine so we can clear it independently of search context */ + context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine d_equalityEngine; + eq::EqualityEngine* d_equalityEngine; /** map of representatives of equality engine to used representatives in representative set */ std::map< Node, Node > d_reps; /** stores set of representatives for each type */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 8c85e4dd2..8aa7d625d 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1382,7 +1382,7 @@ void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( eqc.getType()==d_type ){ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 601d65799..bfbc851ef 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + array_card.smt2 \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ @@ -29,7 +30,7 @@ TESTS = \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 + bug0909.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2 new file mode 100644 index 000000000..9ee00d13a --- /dev/null +++ b/test/regress/regress0/fmf/array_card.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic AUFLIA) +(set-option :produce-models true) +(declare-sort U 0) +(declare-fun f () (Array U U)) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (distinct a b c)) + +(assert (distinct (select f a) (select f b))) + +(assert (forall ((x U)) (or (= (select f x) c) (= (select f x) b)))) + +(check-sat)