diff options
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 13 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 27 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/coda_simp_model.smt2 | 12 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/jasmin-cdt-crash.smt2 | 100 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/loopy_coda.smt2 | 38 |
7 files changed, 179 insertions, 18 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 35d82b2ae..d49974df2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -190,6 +190,7 @@ void TheoryDatatypes::check(Effort e) { if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton() ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; @@ -1410,11 +1411,13 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //until models are implemented for codatatypes //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 ); + if( !it->second.isNull() ){ + 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 ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 2a8e21059..18ed6714d 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -467,17 +467,19 @@ void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node } bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { - Trace("model-builder-cdt") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; + Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; for (set<Node>::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; + Trace("model-builder-debug") << " 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; + Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; + if( eqc_m.getKind()==kind::UNINTERPRETED_CONSTANT ){ + Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc << std::endl; + return true; + } } } return false; @@ -528,11 +530,11 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne visited[v] = true; TypeNode tn = v.getType(); if( tn.isSort() ){ - Trace("exc-value-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; + Trace("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; unsigned card = eqc_usort_count[tn]; - Trace("exc-value-debug") << " Cardinality is " << card << std::endl; + Trace("model-builder-debug") << " Cardinality is " << card << std::endl; unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); - Trace("exc-value-debug") << " Index is " << index << std::endl; + Trace("model-builder-debug") << " Index is " << index << std::endl; return index>0 && index>=card; } for( unsigned i=0; i<v.getNumChildren(); i++ ){ @@ -772,6 +774,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if(t.isTuple() || t.isRecord()) { t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); } + //get properties of this type bool isCorecursive = false; bool isUSortFiniteRestricted = false; @@ -782,6 +785,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if( options::finiteModelFind() ){ isUSortFiniteRestricted = !t.isSort() && involvesUSort( t ); } + set<Node>* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { @@ -810,6 +814,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) evaluable = true; } } + Trace("model-builder-debug") << " eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl; if (assignable) { Assert(!evaluable || assignOne); Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); @@ -821,7 +826,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) //--- AJR: this code checks whether n is a legal value Assert( !n.isNull() ); success = true; - Trace("exc-value-debug") << "Check if excluded : " << n << std::endl; + Trace("model-builder-debug") << "Check if excluded : " << n << std::endl; if( isUSortFiniteRestricted ){ #ifdef CVC4_ASSERTIONS //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc) @@ -829,7 +834,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, bool > visited; success = !isExcludedUSortValue( eqc_usort_count, n, visited ); if( !success ){ - Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl; + Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl; } Assert( success ); #endif @@ -840,7 +845,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015 success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 ); if( !success ){ - Trace("exc-value") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; + Trace("model-builder") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; } } } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index d06fb1b9b..1759d2924 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -68,7 +68,8 @@ TESTS = \ bug625.smt2 \ cdt-model-cade15.smt2 \ sc-cdt1.smt2 \ - conqueue-dt-enum-iloop.smt2 + conqueue-dt-enum-iloop.smt2 \ + coda_simp_model.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/coda_simp_model.smt2 b/test/regress/regress0/datatypes/coda_simp_model.smt2 new file mode 100644 index 000000000..1e000cecd --- /dev/null +++ b/test/regress/regress0/datatypes/coda_simp_model.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort a_ 0) +(declare-fun __nun_card_witness_0 () a_) +(declare-codatatypes () + ((llist_ (LCons_ (_select_LCons__0 a_) (_select_LCons__1 llist_)) + (LNil_ )))) +(declare-fun s () llist_) +(declare-fun a () a_) +(declare-fun b () a_) +(assert (= s (LCons_ a (LCons_ b s)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index ff2591a5b..d262d624f 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -45,7 +45,9 @@ TESTS = \ sc_bad_model_1221.smt2 \ dt-proper-model.smt2 \ fd-false.smt2 \ - tail_rec.smt2 + tail_rec.smt2 \ + jasmin-cdt-crash.smt2 \ + loopy_coda.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 new file mode 100644 index 000000000..1f7214232 --- /dev/null +++ b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 @@ -0,0 +1,100 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort a_ 0) +(declare-fun __nun_card_witness_0 () a_) +(declare-codatatypes () + ((llist_ (LCons_ (_select_LCons__0 a_) (_select_LCons__1 llist_)) + (LNil_ )))) +(declare-fun xs_ () llist_) +(declare-fun y_ () a_) +(declare-fun ys_ () llist_) +(declare-datatypes () ((_nat (_succ (_select__succ_0 _nat)) (_zero )))) +(declare-fun decr_lprefix_ () _nat) +(declare-sort G_lprefix__neg 0) +(declare-fun __nun_card_witness_1 () G_lprefix__neg) +(declare-fun lprefix__- (_nat llist_ llist_) Bool) +(declare-fun proj_G_lprefix__neg_0 (G_lprefix__neg) _nat) +(declare-fun proj_G_lprefix__neg_1 (G_lprefix__neg) llist_) +(declare-fun proj_G_lprefix__neg_2 (G_lprefix__neg) llist_) +(assert + (forall ((a/60 G_lprefix__neg)) + (=> + (or (= (proj_G_lprefix__neg_0 a/60) _zero) + (and (is-_succ (proj_G_lprefix__neg_0 a/60)) + (= (proj_G_lprefix__neg_1 a/60) LNil_)) + (and + (=> + (exists ((a/68 G_lprefix__neg)) + (and + (= (_select_LCons__1 (proj_G_lprefix__neg_2 a/60)) + (proj_G_lprefix__neg_2 a/68)) + (= (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) + (proj_G_lprefix__neg_1 a/68)) + (= (_select__succ_0 (proj_G_lprefix__neg_0 a/60)) + (proj_G_lprefix__neg_0 a/68)))) + (lprefix__- (_select__succ_0 (proj_G_lprefix__neg_0 a/60)) + (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) + (_select_LCons__1 (proj_G_lprefix__neg_2 a/60)))) + (is-_succ (proj_G_lprefix__neg_0 a/60)) + (is-LCons_ (proj_G_lprefix__neg_1 a/60)) + (is-LCons_ (proj_G_lprefix__neg_2 a/60)) + (= (_select_LCons__0 (proj_G_lprefix__neg_2 a/60)) + (_select_LCons__0 (proj_G_lprefix__neg_1 a/60))))) + (lprefix__- (proj_G_lprefix__neg_0 a/60) (proj_G_lprefix__neg_1 a/60) + (proj_G_lprefix__neg_2 a/60))))) +(declare-sort G_lprefix__pos 0) +(declare-fun __nun_card_witness_2 () G_lprefix__pos) +(declare-fun lprefix__+ (llist_ llist_) Bool) +(declare-fun proj_G_lprefix__pos_0 (G_lprefix__pos) llist_) +(declare-fun proj_G_lprefix__pos_1 (G_lprefix__pos) llist_) +(assert + (forall ((a/69 G_lprefix__pos)) + (=> + (lprefix__+ (proj_G_lprefix__pos_0 a/69) (proj_G_lprefix__pos_1 a/69)) + (or (= (proj_G_lprefix__pos_0 a/69) LNil_) + (and + (lprefix__+ (_select_LCons__1 (proj_G_lprefix__pos_0 a/69)) + (_select_LCons__1 (proj_G_lprefix__pos_1 a/69))) + (exists ((a/77 G_lprefix__pos)) + (and + (= (_select_LCons__1 (proj_G_lprefix__pos_1 a/69)) + (proj_G_lprefix__pos_1 a/77)) + (= (_select_LCons__1 (proj_G_lprefix__pos_0 a/69)) + (proj_G_lprefix__pos_0 a/77)))) + (is-LCons_ (proj_G_lprefix__pos_0 a/69)) + (is-LCons_ (proj_G_lprefix__pos_1 a/69)) + (= (_select_LCons__0 (proj_G_lprefix__pos_1 a/69)) + (_select_LCons__0 (proj_G_lprefix__pos_0 a/69)))))))) +(declare-fun nun_sk_0 () llist_) +(assert + (or + (and + (not + (=> + (exists ((a/109 G_lprefix__neg)) + (and (= (LCons_ y_ ys_) (proj_G_lprefix__neg_2 a/109)) + (= xs_ (proj_G_lprefix__neg_1 a/109)) + (= decr_lprefix_ (proj_G_lprefix__neg_0 a/109)))) + (lprefix__- decr_lprefix_ xs_ (LCons_ y_ ys_)))) + (or (= xs_ LNil_) + (and (= xs_ (LCons_ y_ nun_sk_0)) (lprefix__+ xs_ ys_) + (exists ((a/113 G_lprefix__pos)) + (and (= ys_ (proj_G_lprefix__pos_1 a/113)) + (= xs_ (proj_G_lprefix__pos_0 a/113))))))) + (and (not (= xs_ LNil_)) + (forall ((xs_H_/120 llist_)) + (or (not (= xs_ (LCons_ y_ xs_H_/120))) + (not + (=> + (exists ((a/124 G_lprefix__neg)) + (and (= ys_ (proj_G_lprefix__neg_2 a/124)) + (= xs_ (proj_G_lprefix__neg_1 a/124)) + (= decr_lprefix_ (proj_G_lprefix__neg_0 a/124)))) + (lprefix__- decr_lprefix_ xs_ ys_))))) + (lprefix__+ xs_ (LCons_ y_ ys_)) + (exists ((a/125 G_lprefix__pos)) + (and (= (LCons_ y_ ys_) (proj_G_lprefix__pos_1 a/125)) + (= xs_ (proj_G_lprefix__pos_0 a/125))))))) +(check-sat) diff --git a/test/regress/regress0/fmf/loopy_coda.smt2 b/test/regress/regress0/fmf/loopy_coda.smt2 new file mode 100644 index 000000000..7c1d30886 --- /dev/null +++ b/test/regress/regress0/fmf/loopy_coda.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort a 0) +(declare-fun __nun_card_witness_0 () a) +(declare-codatatypes () + ((llist (LCons (_select_LCons_0 a) (_select_LCons_1 llist)) (LNil )))) +(declare-fun xs () llist) +(declare-fun y () a) +(declare-fun ys () llist) +(declare-sort G_lappend 0) +(declare-fun __nun_card_witness_1 () G_lappend) +(declare-fun lappend (llist llist) llist) +(declare-fun proj_G_lappend_0 (G_lappend) llist) +(declare-fun proj_G_lappend_1 (G_lappend) llist) +(assert + (forall ((a/33 G_lappend)) + (and + (= (lappend (proj_G_lappend_0 a/33) (proj_G_lappend_1 a/33)) + (ite (is-LCons (proj_G_lappend_0 a/33)) + (LCons (_select_LCons_0 (proj_G_lappend_0 a/33)) + (lappend (_select_LCons_1 (proj_G_lappend_0 a/33)) + (proj_G_lappend_1 a/33))) + (proj_G_lappend_1 a/33))) + (=> (is-LCons (proj_G_lappend_0 a/33)) + (exists ((a/35 G_lappend)) + (and (= (proj_G_lappend_1 a/33) (proj_G_lappend_1 a/35)) + (= (_select_LCons_1 (proj_G_lappend_0 a/33)) + (proj_G_lappend_0 a/35)))))))) +(assert + (not + (=> + (exists ((a/37 G_lappend)) + (and (= (LCons y ys) (proj_G_lappend_1 a/37)) + (= xs (proj_G_lappend_0 a/37)))) + (= (lappend xs (LCons y ys)) xs)))) +(check-sat) |