From 07504bdc61fe1d18af2fabe56fcee89e531b033c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 10 Sep 2015 18:38:16 +0200 Subject: [PATCH] Models for codatatypes. Fixes bug 662. --- src/theory/arrays/theory_arrays.cpp | 4 +- src/theory/datatypes/datatypes_rewriter.h | 41 +++++---- src/theory/datatypes/theory_datatypes.cpp | 84 +++++++------------ src/theory/datatypes/theory_datatypes.h | 2 +- src/theory/theory_model.cpp | 59 ++++++++++++- src/theory/theory_model.h | 3 + test/regress/regress0/datatypes/Makefile.am | 3 +- .../regress0/datatypes/cdt-model-cade15.smt2 | 17 ++++ 8 files changed, 137 insertions(+), 76 deletions(-) create mode 100755 test/regress/regress0/datatypes/cdt-model-cade15.smt2 diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8bdf38ca3..d872ab42c 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -757,7 +757,7 @@ void TheoryArrays::computeCareGraph() // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check // Also, insert this read in the list at the proper index - + if (!x_shared.isConst()) { x_shared = d_valuation.getModelValue(x_shared); } @@ -1032,7 +1032,7 @@ void TheoryArrays::check(Effort e) { if (done() && !fullEffort(e)) { return; } - + getOutputChannel().spendResource(options::theoryCheckStep()); TimerStat::CodeTimer checkTimer(d_checkTime); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index f33c380d7..c342e488a 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -58,6 +58,13 @@ public: return RewriteResponse(REWRITE_DONE, inr); } } + if( in.isConst() ){ + Node inn = normalizeConstant( in ); + if( inn!=in ){ + Trace("datatypes-rewrite-debug") << "Normalized constant " << in << " -> " << inn << std::endl; + return RewriteResponse(REWRITE_DONE, inn); + } + } } if(in.getKind() == kind::APPLY_TESTER) { @@ -585,23 +592,27 @@ public: } //normalize constant : apply to top-level codatatype constants static Node normalizeConstant( Node n ){ - Assert( n.getType().isDatatype() ); - const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - if( dt.isCodatatype() ){ - return normalizeCodatatypeConstant( n ); - }else{ - std::vector< Node > children; - bool childrenChanged = false; - for( unsigned i = 0; imkNode( n.getKind(), children ); + if( n.getType().isDatatype() ){ + Assert( n.getType().isDatatype() ); + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + if( dt.isCodatatype() ){ + return normalizeCodatatypeConstant( n ); }else{ - return n; + std::vector< Node > children; + bool childrenChanged = false; + for( unsigned i = 0; imkNode( n.getKind(), children ); + }else{ + return n; + } } + }else{ + return n; } } };/* class DatatypesRewriter */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e0a4dc7d8..72717f974 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1277,26 +1277,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Node c = ei->d_constructor.get(); cons.push_back( c ); eqc_cons[ eqc ] = c; - Trace("dt-cmi") << "Datatypes : assert representative " << c << " for " << eqc << std::endl; - m->assertRepresentative( c ); }else{ //if eqc contains a symbol known to datatypes (a selector), then we must assign -#if 0 - bool shouldConsider = false; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl; - if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){ - shouldConsider = true; - break; - } - ++eqc_i; - } -#else //should assign constructors to EQC if they have a selector or a tester bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); -#endif if( shouldConsider ){ nodes.push_back( eqc ); } @@ -1398,68 +1382,56 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-cmi") << "Assign : " << neqc << std::endl; m->assertEquality( eqc, neqc, true ); eqc_cons[ eqc ] = neqc; - Trace("dt-cmi") << "Datatypes : assert representative " << neqc << " for " << eqc << std::endl; - m->assertRepresentative( neqc ); } - //m->assertRepresentative( neqc ); if( addCons ){ cons.push_back( neqc ); } ++index; } - //assign MU for each codatatype eqc - std::map< Node, Node > eqc_mu; for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){ Node eqc = it->first; const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( dt.isCodatatype() ){ //until models are implemented for codatatypes - throw Exception("Models for codatatypes are not supported in this version."); - /* - std::map< Node, Node > vmap; - std::vector< Node > fv; - Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv ); - Trace("dt-cmi-cdt") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; - //m->assertEquality( eqc, v, true ); - */ + //throw Exception("Models for codatatypes are not supported in this version."); + //must proactive expand to avoid looping behavior in model builder + std::map< Node, int > vmap; + Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 ); + Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; + m->assertEquality( eqc, v, true ); + m->assertRepresentative( v ); + }else{ + Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl; + m->assertRepresentative( it->second ); } } } -Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv ){ - std::map< Node, Node >::iterator itv = vmap.find( n ); +Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){ + std::map< Node, int >::iterator itv = vmap.find( n ); if( itv!=vmap.end() ){ - if( std::find( fv.begin(), fv.end(), itv->second )==fv.end() ){ - fv.push_back( itv->second ); - } - return itv->second; + int debruijn = depth - 1 - itv->second; + return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); }else if( DatatypesRewriter::isTermDatatype( n ) ){ - std::stringstream ss; - ss << "$x" << vmap.size(); - Node nv = NodeManager::currentNM()->mkBoundVar( ss.str().c_str(), n.getType() ); - vmap[n] = nv; - Trace("dt-cmi-cdt-debug") << " map " << n << " -> " << nv << std::endl; Node nc = eqc_cons[n]; - Assert( nc.getKind()==APPLY_CONSTRUCTOR ); - std::vector< Node > children; - children.push_back( nc.getOperator() ); - for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ); - //add mu if we found a circular reference - if( std::find( fv.begin(), fv.end(), nv )!=fv.end() ){ - v = NodeManager::currentNM()->mkNode( MU, nv, v ); + if( !nc.isNull() ){ + vmap[n] = depth; + Trace("dt-cmi-cdt-debug") << " map " << n << " -> " << depth << std::endl; + Assert( nc.getKind()==APPLY_CONSTRUCTOR ); + std::vector< Node > children; + children.push_back( nc.getOperator() ); + for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ); } - return v; - }else{ - return n; } + return n; } Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index ab40f07db..a221153a3 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -266,7 +266,7 @@ private: std::map< Node, Node >& cn, std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); /** build model */ - Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv ); + Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ); /** get singleton lemma */ Node getSingletonLemma( TypeNode tn, bool pol ); /** collect terms */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cf0fbcbfe..5766a26c1 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -489,6 +489,46 @@ void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { + Trace("model-builder-cdt") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; + for (set::iterator i = repSet->begin(); i != repSet->end(); ++i ) { + Assert(assertedReps.find(*i) != assertedReps.end()); + Node rep = assertedReps[*i]; + Trace("model-builder-cdt") << " Rep : " << rep << std::endl; + //check matching val to rep with eqc as a free variable + Node eqc_m; + if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){ + Trace("model-builder-cdt") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; + Trace("model-builder-cdt") << "*** " << val << " is excluded datatype for " << eqc << std::endl; + return true; + } + } + return false; +} + +bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ) { + if( r==v ){ + return true; + }else if( r==eqc ){ + if( eqc_m.isNull() ){ + //only if an uninterpreted constant? + eqc_m = v; + return true; + }else{ + return v==eqc_m; + } + }else if( v.getKind()==kind::APPLY_CONSTRUCTOR && r.getKind()==kind::APPLY_CONSTRUCTOR ){ + if( v.getOperator()==r.getOperator() ){ + for( unsigned i=0; igetDatatypeForTupleRecord(t); } + bool isCorecursive = false; + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); + isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() ); + } + set* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { set* repSet = typeRepSet.getSet(tb); @@ -731,7 +777,18 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); Node n; if (t.getCardinality().isInfinite()) { - n = typeConstSet.nextTypeEnum(t, true); + bool success; + do{ + n = typeConstSet.nextTypeEnum(t, true); + success = true; + if( isCorecursive ){ + if (repSet != NULL && !repSet->empty()) { + // in the case of codatatypes, check if it is in the set of values that we cannot assign + // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015 + success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 ); + } + } + }while( !success ); } else { TypeEnumerator te(t); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index a161f02f4..092b5e8c7 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -262,6 +262,9 @@ protected: bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); void assignConstantRep( TheoryModel* tm, std::map& constantReps, Node eqc, Node const_rep, bool fullModel ); + /** is v an excluded codatatype value */ + bool isExcludedCdtValue( Node v, std::set* repSet, std::map< Node, Node >& assertedReps, Node eqc ); + bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 45060dbd3..fc110ed92 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -65,7 +65,8 @@ TESTS = \ stream-singleton.smt2 \ is_test.smt2 \ manos-model.smt2 \ - bug625.smt2 + bug625.smt2 \ + cdt-model-cade15.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 new file mode 100755 index 000000000..5b570a915 --- /dev/null +++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream))))) + +(declare-const z Stream) +(declare-const x Stream) +(declare-const y Stream) +(declare-const u Stream) +(declare-const v Stream) +(declare-const w Stream) + +(assert (= u (C z))) +(assert (= v (D z))) +(assert (= w (E y))) +(assert (= x (C v))) +(assert (distinct x y z u v w)) +(check-sat) \ No newline at end of file -- 2.30.2