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;
//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 );
}
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;
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++ ){
if(t.isTuple() || t.isRecord()) {
t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
}
+
//get properties of this type
bool isCorecursive = false;
bool isUSortFiniteRestricted = false;
if( options::finiteModelFind() ){
isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
}
+
set<Node>* repSet = typeRepSet.getSet(t);
TypeNode tb = t.getBaseType();
if (!assignOne) {
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);
//--- 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)
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
// 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;
}
}
}
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
--- /dev/null
+(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
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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff