options::fmfInstGen.set( false );
}
}
+ if ( options::fmfBoundInt() ){
+ //if bounded integers are set, must use full model check for MBQI
+ options::fmfFullModelCheck.set( true );
+ }
if( options::ufssSymBreak() ){
options::sortInference.set( true );
}
public:
static RewriteResponse postRewrite(TNode in) {
- Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl;
+ Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
Type t = in.getType().toType();
// to ensure a normal form, all parameteric datatype constructors must have a type ascription
if( dt.isParametric() ){
if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
- Trace("datatypes-rewrite") << "Ascribing type to parametric datatype constructor " << in << std::endl;
+ Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
Node op = in.getOperator();
//get the constructor object
const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
children.push_back( op_new );
children.insert( children.end(), in.begin(), in.end() );
Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
- Trace("datatypes-rewrite") << "Created " << inr << std::endl;
+ Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
return RewriteResponse(REWRITE_DONE, inr);
}
}
}
static RewriteResponse preRewrite(TNode in) {
- Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
+ Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
return RewriteResponse(REWRITE_DONE, in);
}
#include "smt/options.h"
#include "smt/boolean_terms.h"
#include "theory/quantifiers/options.h"
+#include "theory/datatypes/options.h"
+#include "theory/type_enumerator.h"
#include <map>
}
}
if( !needSplit && mustSpecifyAssignment() ){
+ // &&
//for the sake of termination, we must choose the constructor of a ground term
//NEED GUARENTEE: groundTerm should not contain any subterms of the same type
//** TODO: this is probably not good enough, actually need fair enumeration strategy
+ /*
Node groundTerm = n.getType().mkGroundTerm();
int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
if( pcons[index] ){
consIndex = index;
}
needSplit = true;
+ */
}
if( needSplit && consIndex!=-1 ) {
Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
d_out->requirePhase( test, true );
return;
}else{
- Trace("dt-split") << "Do not split constructor for " << n << std::endl;
+ Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl;
}
}
}else{
trep2 = eqc2->d_constructor.get();
}
EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
+
+
+
if( eqc1 ){
if( !eqc1->d_constructor.get().isNull() ){
trep1 = eqc1->d_constructor.get();
eqc1->d_inst = true;
}
if( cons1.isNull() && !cons2.isNull() ){
+ Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+ NodeListMap::iterator lbl_i = d_labels.find( t1 );
+ if( lbl_i != d_labels.end() ){
+ size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr());
+ NodeList* lbl = (*lbl_i).second;
+ for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+ if( (*i).getKind()==NOT ){
+ if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){
+ Node n = *i;
+ std::vector< TNode > assumptions;
+ explain( *i, assumptions );
+ explain( cons2.eqNode( (*i)[0][0] ), assumptions );
+ d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
+ Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+ Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+ d_out->conflict( d_conflictNode );
+ d_conflict = true;
+ return;
+ }
+ }
+ }
+ }
+
checkInst = true;
eqc1->d_constructor.set( eqc2->d_constructor );
}
eqc1->d_inst.set( eqc2->d_inst );
eqc1->d_constructor.set( eqc2->d_constructor );
}
+
+
+
//merge labels
- Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
NodeListMap::iterator lbl_i = d_labels.find( t2 );
if( lbl_i != d_labels.end() ){
+ Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
NodeList* lbl = (*lbl_i).second;
for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
addTester( *j, eqc1, t1 );
if( d_conflict ){
+ Debug("datatypes-debug") << "Conflict!" << std::endl;
return;
}
}
void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
if( !d_conflict ){
- Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl;
+ Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
bool tpolarity = t.getKind()!=NOT;
Node tt = ( t.getKind() == NOT ) ? t[0] : t;
int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
m->assertEqualityEngine( &d_equalityEngine );
+
+ std::vector< TypeEnumerator > vec;
+ std::map< TypeNode, int > tes;
+ Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl;
+
+ //get all constructors
+ eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
+ std::vector< Node > cons;
+ while( !eqccs_i.isFinished() ){
+ Node eqc = (*eqccs_i);
+ //for all equivalence classes that are datatypes
+ if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ EqcInfo* ei = getOrMakeEqcInfo( eqc );
+ if( ei ){
+ if( !ei->d_constructor.get().isNull() ){
+ cons.push_back( ei->d_constructor.get() );
+ }
+ }
+ }
+ ++eqccs_i;
+ }
+
//must choose proper representatives
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
if( ei ){
if( !ei->d_constructor.get().isNull() ){
//specify that we should use the constructor as the representative
- m->assertRepresentative( ei->d_constructor.get() );
+ //m->assertRepresentative( ei->d_constructor.get() );
}else{
- Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl;
- Trace("model-warn") << " Type : " << eqc.getType() << std::endl;
+ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
+ Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
+
+ std::vector< bool > pcons;
+ getPossibleCons( ei, eqc, pcons );
+ Trace("dt-cmi") << "Possible constructors : ";
+ for( unsigned i=0; i<pcons.size(); i++ ){
+ Trace("dt-cmi") << pcons[i] << " ";
+ }
+ Trace("dt-cmi") << std::endl;
+
+ if( tes.find( eqc.getType() )==tes.end() ){
+ tes[eqc.getType()]=vec.size();
+ vec.push_back( TypeEnumerator( eqc.getType() ) );
+ }
+ bool success;
+ Node n;
+ do {
+ success = true;
+ Assert( !vec[tes[eqc.getType()]].isFinished() );
+ n = *vec[tes[eqc.getType()]];
+ ++vec[tes[eqc.getType()]];
+
+ //applyTypeAscriptions( n, eqc.getType() );
+
+ Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl;
+ //check if it is consistent with labels
+ size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+ if( constructorIndex<pcons.size() && pcons[constructorIndex] ){
+ for( unsigned i=0; i<cons.size(); i++ ){
+ //check if it is modulo equality the same
+ if( cons[i].getOperator()==n.getOperator() ){
+ bool diff = false;
+ for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+ if( !m->areEqual( cons[i][j], n[j] ) ){
+ diff = true;
+ break;
+ }
+ }
+ if( !diff ){
+ Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
+ success = false;
+ break;
+ }
+ }
+ }
+ }else{
+ Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
+ success = false;
+ }
+ }while( !success );
+ Trace("dt-cmi") << "Assign : " << n << std::endl;
+ //m->assertRepresentative( n );
+ m->assertEquality( eqc, n, true );
+
}
}else{
Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl;
return n_ic;
//}
}
-
+/*
+Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){
+ Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl;
+ if( n.getKind()==APPLY_CONSTRUCTOR ){
+ //add type ascription for ambiguous constructor types
+ if(!n.getType().isComparableTo(tn)) {
+ size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( dt.isParametric() );
+ Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl;
+ Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl;
+ Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType());
+ Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl;
+ Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() );
+ std::vector< Node > children;
+ children.push_back( op );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ children.push_back( applyTypeAscriptions( n[i], TypeNode::fromType( tspec )[i] ) );
+ }
+ n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ) );
+ Assert( n.getType()==tn );
+ return n;
+ }
+ }else{
+ if( n.getType()!=tn ){
+ Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl;
+ }
+ }
+ return n;
+}
+*/
void TheoryDatatypes::collapseSelectors(){
//must check incorrect applications of selectors
for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){
int index = getLabelIndex( eqc, n );
const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
//must be finite or have a selector
- if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
+ //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
//instantiate this equivalence class
eqc->d_inst = true;
Node tt_cons = getInstantiateCons( tt, dt, index );
d_infer.push_back( eq );
d_infer_exp.push_back( exp );
}
- }
+ //}
+ //else{
+ // Debug("datatypes-inst") << "Do not instantiate" << std::endl;
+ //}
}
}
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
- Trace( c ) << "DATATYPE : ";
- }
- Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
- Trace( c ) << " { ";
- //add terms to model
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
- while( !eqc_i.isFinished() ){
- Trace( c ) << (*eqc_i) << " ";
- ++eqc_i;
- }
- Trace( c ) << "}" << std::endl;
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
- EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( ei ){
- Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl;
- if( ei->d_constructor.get().isNull() ){
- Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
- Trace("model-warn") << " Type : " << eqc.getType() << std::endl;
- Trace( c ) << " Constructor : " << std::endl;
- Trace( c ) << " Labels : ";
- if( hasLabel( ei, eqc ) ){
- Trace( c ) << getLabel( eqc );
- }else{
- NodeListMap::iterator lbl_i = d_labels.find( eqc );
- if( lbl_i != d_labels.end() ){
- NodeList* lbl = (*lbl_i).second;
- for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
- Trace( c ) << *j << " ";
+ if( !eqc.getType().isBoolean() ){
+ if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ Trace( c ) << "DATATYPE : ";
+ }
+ Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
+ Trace( c ) << " { ";
+ //add terms to model
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ Trace( c ) << (*eqc_i) << " ";
+ ++eqc_i;
+ }
+ Trace( c ) << "}" << std::endl;
+ if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ EqcInfo* ei = getOrMakeEqcInfo( eqc );
+ if( ei ){
+ Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl;
+ if( ei->d_constructor.get().isNull() ){
+ Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
+ Trace("debug-model-warn") << " Type : " << eqc.getType() << std::endl;
+ Trace( c ) << " Constructor : " << std::endl;
+ Trace( c ) << " Labels : ";
+ if( hasLabel( ei, eqc ) ){
+ Trace( c ) << getLabel( eqc );
+ }else{
+ NodeListMap::iterator lbl_i = d_labels.find( eqc );
+ if( lbl_i != d_labels.end() ){
+ NodeList* lbl = (*lbl_i).second;
+ for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
+ Trace( c ) << *j << " ";
+ }
}
}
+ Trace( c ) << std::endl;
+ }else{
+ Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl;
}
- Trace( c ) << std::endl;
- }else{
- Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl;
+ Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
}
- Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
}
}
++eqcs_i;
void collectTerms( Node n );
/** get instantiate cons */
Node getInstantiateCons( Node n, const Datatype& dt, int index );
+ /** apply type ascriptions */
+ //Node applyTypeAscriptions( Node n, TypeNode tn );
/** process new term that was created internally */
void processNewTerm( Node n );
/** check instantiate */
size_t d_zeroCtor;
/** Delegate enumerators for the arguments of the current constructor */
TypeEnumerator** d_argEnumerators;
+ /** type */
+ TypeNode d_type;
/** Allocate and initialize the delegate enumerators */
void newEnumerators() {
d_datatype(DatatypeType(type.toType()).getDatatype()),
d_ctor(0),
d_zeroCtor(0),
- d_argEnumerators(NULL) {
+ d_argEnumerators(NULL),
+ d_type(type) {
//Assert(type.isDatatype());
Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
/* FIXME: this isn't sufficient for mutually-recursive datatypes! */
while(d_zeroCtor < d_datatype.getNumConstructors()) {
bool recursive = false;
- for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
- recursive = (Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type);
+ if( d_datatype.isParametric() ){
+ TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) );
+ for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
+ if( tn[i]==type ){
+ recursive = true;
+ break;
+ }
+ }
+ }else{
+ for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
+ if(Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type) {
+ recursive = true;
+ break;
+ }
+ }
}
if(!recursive) {
break;
d_datatype(de.d_datatype),
d_ctor(de.d_ctor),
d_zeroCtor(de.d_zeroCtor),
- d_argEnumerators(NULL) {
+ d_argEnumerators(NULL),
+ d_type(de.d_type) {
if(de.d_argEnumerators != NULL) {
newEnumerators();
if(d_ctor < d_datatype.getNumConstructors()) {
DatatypeConstructor ctor = d_datatype[d_ctor];
NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
- b << ctor.getConstructor();
+ Type typ;
+ if( d_datatype.isParametric() ){
+ typ = d_datatype[d_ctor].getSpecializedConstructorType(d_type.toType());
+ b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
+ }else{
+ b << ctor.getConstructor();
+ }
try {
for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) {
if(d_argEnumerators[a] == NULL) {
- d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+ if( d_datatype.isParametric() ){
+ d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType( typ )[a]);
+ }else{
+ d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+ }
}
b << **d_argEnumerators[a];
}
} catch(NoMoreValuesException&) {
InternalError();
}
- return Node(b);
+ Node nnn = Node(b);
+ //if( nnn.getType()!=d_type || !nnn.getType().isComparableTo(d_type) ){
+ // Debug("dt-warn") << "WARNING : Enum : " << nnn << " bad type : " << nnn.getType() << " " << d_type << std::endl;
+ //}
+ return nnn;
} else {
throw NoMoreValuesException(getType());
}
int ModelEngine::checkModel(){
FirstOrderModel* fm = d_quantEngine->getModel();
+
+ //flatten the representatives
+ //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
+ //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
+
//for debugging
if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
for( size_t i=0; i<it->second.size(); i++ ){
//Trace("model-engine-debug") << it->second[i] << " ";
- Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
+ Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
disable model-based quantifier instantiation for finite model finding
-option fmfFullModelCheck --fmf-fmc bool :default false
+option fmfFullModelCheck --fmf-fmc bool :default false :read-write
enable full model check for finite model finding
option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
disable simple models in full model check for finite model finding
delete d_eq_query;
}
-EqualityQuery* QuantifiersEngine::getEqualityQuery() {
+EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
return d_eq_query;
}
eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) ){
return ee->getRepresentative( a );
+ }else{
+ return a;
}
- return a;
}
bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
if( !options::internalReps() ){
return r;
}else{
- int sortId = 0;
- if( optInternalRepSortInference() && !f.isNull() ){
- sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
- }
- if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
+ if( d_int_rep.find( r )==d_int_rep.end() ){
//find best selection for representative
Node r_best;
- if( options::fmfRelevantDomain() ){
+ if( options::fmfRelevantDomain() && !f.isNull() ){
Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r );
Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
//if cbqi is active, do not choose instantiation constant terms
if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
int score = getRepScore( eqc[i], f, index );
- //base it on sort information as well
- if( sortId!=0 ){
- int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] );
- if( score>=0 && e_sortId!=sortId ){
- score += 100;
- }
- }
//score prefers earliest use of this term as a representative
if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
r_best = eqc[i];
}
}
if( r_best.isNull() ){
- Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
- r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+ if( !f.isNull() ){
+ Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+ r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+ }else{
+ r_best = a;
+ }
}
//now, make sure that no other member of the class is an instance
- if( !optInternalRepSortInference() ){
- r_best = getInstance( r_best, eqc );
- }
+ r_best = getInstance( r_best, eqc );
//store that this representative was chosen at this point
if( d_rep_score.find( r_best )==d_rep_score.end() ){
d_rep_score[ r_best ] = d_reset_count;
}
Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
}
- d_int_rep[sortId][r] = r_best;
+ d_int_rep[r] = r_best;
if( r_best!=a ){
Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
}
- if( optInternalRepSortInference() ){
- int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best );
- if( sortId!=sortIdBest ){
- Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl;
- }
- }
return r_best;
}else{
- return d_int_rep[sortId][r];
+ return d_int_rep[r];
}
}
}
+void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
+ //make sure internal representatives currently exist
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
+ if( it->first.isSort() ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
+ }
+ }
+ }
+ Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
+ for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+ Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ }
+ //store representatives for newly created terms
+ std::map< Node, Node > temp_rep_map;
+
+ bool success;
+ do {
+ success = false;
+ for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+ if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
+ Node ni = it->second;
+ std::vector< Node > cc;
+ cc.push_back( it->second.getOperator() );
+ bool changed = false;
+ for( unsigned j=0; j<ni.getNumChildren(); j++ ){
+ if( ni[j].getType().isSort() ){
+ Node r = getRepresentative( ni[j] );
+ if( d_int_rep.find( r )==d_int_rep.end() ){
+ Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
+ r = temp_rep_map[r];
+ }
+ if( r==ni ){
+ //found sub-term as instance
+ Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
+ d_int_rep[it->first] = ni[j];
+ changed = false;
+ success = true;
+ break;
+ }else{
+ Node ir = d_int_rep[r];
+ cc.push_back( ir );
+ if( ni[j]!=ir ){
+ changed = true;
+ }
+ }
+ }else{
+ changed = false;
+ break;
+ }
+ }
+ if( changed ){
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+ Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+ success = true;
+ d_int_rep[it->first] = n;
+ temp_rep_map[n] = it->first;
+ }
+ }
+ }
+ }while( success );
+ Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
+ for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+ Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ }
+}
+
eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
return d_qe->getMasterEqualityEngine();
}
//return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
}
-bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
- return false; //shown to be not effective
-}
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
generic one */
- EqualityQuery* getEqualityQuery();
+ EqualityQueryQuantifiersEngine* getEqualityQuery();
/** get instantiation engine */
quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
/** get model engine */
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** internal representatives */
- std::map< int, std::map< Node, Node > > d_int_rep;
+ std::map< Node, Node > d_int_rep;
/** rep score */
std::map< Node, int > d_rep_score;
/** reset count */
Node getInstance( Node n, std::vector< Node >& eqc );
/** get score */
int getRepScore( Node n, Node f, int index );
- /** choose rep based on sort inference */
- bool optInternalRepSortInference();
public:
EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
~EqualityQueryQuantifiersEngine(){}
not contain instantiation constants, if such a term exists.
*/
Node getInternalRepresentative( Node a, Node f, int index );
+ /** flatten representatives */
+ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
void setLiberal( bool l ) { d_liberal = l; }
}; /* EqualityQueryQuantifiersEngine */
projects / cvc5.git / commitdiff