// 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);
}
if (done() && !fullEffort(e)) {
return;
}
-
+
getOutputChannel().spendResource(options::theoryCheckStep());
TimerStat::CodeTimer checkTimer(d_checkTime);
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) {
}
//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; i<n.getNumChildren(); i++ ){
- Node nc = normalizeConstant( n[i] );
- children.push_back( nc );
- childrenChanged = childrenChanged || nc!=n[i];
- }
- if( childrenChanged ){
- return NodeManager::currentNM()->mkNode( 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; i<n.getNumChildren(); i++ ){
+ Node nc = normalizeConstant( n[i] );
+ children.push_back( nc );
+ childrenChanged = childrenChanged || nc!=n[i];
+ }
+ if( childrenChanged ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ return n;
+ }
}
+ }else{
+ return n;
}
}
};/* class DatatypesRewriter */
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 );
}
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; i<nc.getNumChildren(); i++ ){
- Node r = getRepresentative( nc[i] );
- Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap, fv );
- children.push_back( rv );
- }
- vmap.erase( n );
- Node v = NodeManager::currentNM()->mkNode( 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; i<nc.getNumChildren(); i++ ){
+ Node r = getRepresentative( nc[i] );
+ Node rv = getCodatatypesValue( r, eqc_cons, vmap, depth+1 );
+ children.push_back( rv );
+ }
+ vmap.erase( n );
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
}
- return v;
- }else{
- return n;
}
+ return n;
}
Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
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 */
}
}
+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;
+ 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;
+ //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; i<v.getNumChildren(); i++ ){
+ if( !isCdtValueMatch( v[i], r[i], eqc, eqc_m ) ){
+ return false;
+ }
+ }
+ return true;
+ }
+ }
+ return false;
+}
void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
{
if(t.isTuple() || t.isRecord()) {
t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
}
+ bool isCorecursive = false;
+ if( t.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
+ isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
+ }
+ set<Node>* repSet = typeRepSet.getSet(t);
TypeNode tb = t.getBaseType();
if (!assignOne) {
set<Node>* repSet = typeRepSet.getSet(tb);
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);
bool isAssignable(TNode n);
void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
+ /** is v an excluded codatatype value */
+ bool isExcludedCdtValue( Node v, std::set<Node>* 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(){}
stream-singleton.smt2 \
is_test.smt2 \
manos-model.smt2 \
- bug625.smt2
+ bug625.smt2 \
+ cdt-model-cade15.smt2
FAILING_TESTS = \
datatype-dump.cvc
--- /dev/null
+(set-logic ALL_SUPPORTED)\r
+(set-info :status sat)\r
+(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))\r
+\r
+(declare-const z Stream)\r
+(declare-const x Stream)\r
+(declare-const y Stream)\r
+(declare-const u Stream)\r
+(declare-const v Stream)\r
+(declare-const w Stream)\r
+\r
+(assert (= u (C z)))\r
+(assert (= v (D z)))\r
+(assert (= w (E y)))\r
+(assert (= x (C v)))\r
+(assert (distinct x y z u v w))\r
+(check-sat)
\ No newline at end of file
projects / cvc5.git / commitdiff