return;
}
}while( d_addedFact );
-
+
//check for splits
Trace("datatypes-debug") << "Check for splits " << e << endl;
do {
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
Node n = (*eqcs_i);
+ //TODO : avoid irrelevant (pre-registered but not asserted) terms here?
TypeNode tn = n.getType();
if( tn.isDatatype() ){
Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
Trace("dt-model") << std::endl;
+
+ set<Node> termSet;
+
+ // Compute terms appearing in assertions and shared terms, and in inferred equalities
+ getRelevantTerms(termSet);
//combine the equality engine
- m->assertEqualityEngine( &d_equalityEngine );
+ m->assertEqualityEngine( &d_equalityEngine, &termSet );
+
//get all constructors
eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqccs_i.isFinished() ){
Node eqc = (*eqccs_i);
//for all equivalence classes that are datatypes
- if( eqc.getType().isDatatype() ){
- EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( ei && !ei->d_constructor.get().isNull() ){
- Node c = ei->d_constructor.get();
- cons.push_back( c );
- eqc_cons[ eqc ] = c;
- }else{
- //if eqc contains a symbol known to datatypes (a selector), then we must assign
- //should assign constructors to EQC if they have a selector or a tester
- bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
- if( shouldConsider ){
- nodes.push_back( eqc );
+ if( termSet.find( eqc )==termSet.end() ){
+ Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
+ }else{
+ if( eqc.getType().isDatatype() ){
+ EqcInfo* ei = getOrMakeEqcInfo( eqc );
+ if( ei && !ei->d_constructor.get().isNull() ){
+ Node c = ei->d_constructor.get();
+ cons.push_back( c );
+ eqc_cons[ eqc ] = c;
+ }else{
+ //if eqc contains a symbol known to datatypes (a selector), then we must assign
+ //should assign constructors to EQC if they have a selector or a tester
+ bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
+ if( shouldConsider ){
+ nodes.push_back( eqc );
+ }
}
}
}
const Datatype& dt = ((DatatypeType)tt).getDatatype();
if( !d_equalityEngine.hasTerm( eqc ) ){
Assert( false );
- /*
- if( !dt.isCodatatype() ){
- Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
- Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
- TypeNode tn = eqc.getType();
- //if it is infinite, make sure it is fresh
- // this ensures that the term that this is an argument of is distinct.
- if( eqc.getType().getCardinality().isInfinite() ){
- std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
- int teIndex;
- if( it==typ_enum_map.end() ){
- teIndex = (int)typ_enum.size();
- typ_enum_map[tn] = teIndex;
- typ_enum.push_back( TypeEnumerator(tn) );
- }else{
- teIndex = it->second;
- }
- bool success;
- do{
- success = true;
- Assert( !typ_enum[teIndex].isFinished() );
- neqc = *typ_enum[teIndex];
- Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
- ++typ_enum[teIndex];
- for( unsigned i=0; i<cons.size(); i++ ){
- //check if it is modulo equality the same
- if( cons[i].getOperator()==neqc.getOperator() ){
- bool diff = false;
- for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
- if( !m->areEqual( cons[i][j], neqc[j] ) ){
- diff = true;
- break;
- }
- }
- if( !diff ){
- Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
- success = false;
- break;
- }
- }
- }
- }while( !success );
- }else{
- TypeEnumerator te(tn);
- neqc = *te;
- }
- }
- */
}else{
Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
return false;
}
+void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
+ // Compute terms appearing in assertions and shared terms
+ computeRelevantTerms(termSet);
+
+ //also include non-singleton equivalence classes
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ TNode r = (*eqcs_i);
+ bool addedFirst = false;
+ Node first;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ TNode n = (*eqc_i);
+ if( first.isNull() ){
+ first = n;
+ }else{
+ if( !addedFirst ){
+ addedFirst = true;
+ termSet.insert( first );
+ }
+ termSet.insert( n );
+ }
+ ++eqc_i;
+ }
+ ++eqcs_i;
+ }
+}
+
std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {
Trace("dt-entail") << "Check entailed : " << lit << std::endl;
Node atom = lit.getKind()==NOT ? lit[0] : lit;
bool mustCommunicateFact( Node n, Node exp );
/** check clash mod eq */
bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
+ /** get relevant terms */
+ void getRelevantTerms( std::set<Node>& termSet );
private:
//equality queries
bool hasTerm( TNode a );
void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){
+ set<Node> termSet;
+
+ // Compute terms appearing in assertions and shared terms
+ computeRelevantTerms(termSet);
+
// Send the equality engine information to the model
- m->assertEqualityEngine( &d_equalityEngine );
+ m->assertEqualityEngine( &d_equalityEngine, &termSet );
}
void TheorySep::postProcessModel( TheoryModel* m ){
d_sentLemma = false;
d_addedFact = false;
d_set_eqc.clear();
- d_set_eqc_relevant.clear();
d_set_eqc_list.clear();
d_eqc_emptyset.clear();
d_eqc_singleton.clear();
if( tn.isSet() ){
isSet = true;
d_set_eqc.push_back( eqc );
- if( d_equalityEngine.isTriggerTerm(eqc, THEORY_SETS) ){
- d_set_eqc_relevant[eqc] = true;
- }
}
Trace("sets-eqc") << "[" << eqc << "] : ";
eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
if( pindex!=-1 ){
if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
d_pol_mems[pindex][s][x] = n;
- d_set_eqc_relevant[s] = true;
Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
}
if( d_members_index[s].find( x )==d_members_index[s].end() ){
}else{
Node r1 = d_equalityEngine.getRepresentative( n[0] );
Node r2 = d_equalityEngine.getRepresentative( n[1] );
- d_set_eqc_relevant[r1] = true;
- d_set_eqc_relevant[r2] = true;
if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
d_bop_index[n.getKind()][r1][r2] = n;
d_op_list[n.getKind()].push_back( n );
//TODO: extend approach for this case
}
Node r = d_equalityEngine.getRepresentative( n[0] );
- d_set_eqc_relevant[r] = true;
if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
d_eqc_to_card_term[ r ] = n;
registerCardinalityTerm( n[0], lemmas );
void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) {
- Trace("sets") << "Set collect model info" << std::endl;
+ Trace("sets-model") << "Set collect model info" << std::endl;
+ set<Node> termSet;
+ // Compute terms appearing in assertions and shared terms
+ d_external.computeRelevantTerms(termSet);
+
// Assert equalities and disequalities to the model
- m->assertEqualityEngine(&d_equalityEngine);
+ m->assertEqualityEngine(&d_equalityEngine,&termSet);
std::map< Node, Node > mvals;
for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
Node eqc = d_set_eqc[i];
- if( d_set_eqc_relevant.find( eqc )==d_set_eqc_relevant.end() ){
+ if( termSet.find( eqc )==termSet.end() ){
Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
}else{
std::vector< Node > els;
void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
+
+ //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings.
+ // change this if we generalize to sequences.
+ //set<Node> termSet;
+ // Compute terms appearing in assertions and shared terms
+ //computeRelevantTerms(termSet);
+ //m->assertEqualityEngine( &d_equalityEngine, &termSet );
+
m->assertEqualityEngine( &d_equalityEngine );
+
// Generate model
std::vector< Node > nodes;
getEquivalenceClasses( nodes );
}
void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
- m->assertEqualityEngine( &d_equalityEngine );
+ set<Node> termSet;
+
+ // Compute terms appearing in assertions and shared terms
+ computeRelevantTerms(termSet);
+
+ m->assertEqualityEngine( &d_equalityEngine, &termSet );
// if( fullModel ){
// std::map< TypeNode, TypeEnumerator* > type_enums;
// //must choose proper representatives
card-6.smt2 \
card-7.smt2 \
abt-min.smt2 \
- abt-te-exh.smt2
-
+ abt-te-exh.smt2 \
+ abt-te-exh2.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun p ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun j ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun k ((Set Atom) (Set Atom)) (Set Atom))
+(declare-fun d ((Set Atom) (Set Atom)) (Set Atom))
+
+(declare-fun a () (Set Atom))
+(declare-fun n () Atom)
+(declare-fun v () Atom)
+
+(assert (forall ((b Atom) (c Atom))
+(or
+(member v (k (singleton n) (j (singleton b) a)))
+(= (as emptyset (Set Atom)) (d (j (singleton b) a) (singleton n)))
+)
+)
+)
+
+(check-sat)
+
projects / cvc5.git / commitdiff