d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
d_labels( c ),
d_selector_apps( c ),
+ d_consEqc( c ),
d_conflict( c, false ),
d_collectTermsCache( c ),
d_consTerms( c ),
d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+ d_true = NodeManager::currentNM()->mkConst( true );
}
TheoryDatatypes::~TheoryDatatypes() {
}
}
+TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
+ EqcInfo * ei = getOrMakeEqcInfo( r, false );
+ if( ei && !ei->d_constructor.get().isNull() ){
+ return ei->d_constructor.get();
+ }else{
+ return r;
+ }
+}
+
void TheoryDatatypes::check(Effort e) {
Trace("datatypes-debug") << "Check effort " << e << std::endl;
while(!done() && !d_conflict) {
if( dt.getNumConstructors()==1 ){
Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
d_pending.push_back( t );
- d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true );
+ d_pending_exp[ t ] = d_true;
Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
d_infer.push_back( t );
}else{
if( mustCommunicateFact( fact, exp ) ){
Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
Node lem = fact;
- if( exp.isNull() || exp==NodeManager::currentNM()->mkConst( true ) ){
+ if( exp.isNull() || exp==d_true ){
lem = fact;
}else{
Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
tst = Rewriter::rewrite( tst );
Node n_ret;
- if( tst==NodeManager::currentNM()->mkConst( true ) ){
+ if( tst==d_true ){
n_ret = sel;
}else{
if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
nn = NodeManager::currentNM()->mkConst(false);
}else{
- nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
+ nn = rew.size()==0 ? d_true :
( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
}
return nn;
return mkAnd( assumptions );
}
+Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
+ std::vector< TNode > assumptions;
+ for( unsigned i=0; i<lits.size(); i++ ){
+ explain( lits[i], assumptions );
+ }
+ return mkAnd( assumptions );
+}
+
/** Conflict when merging two constants */
void TheoryDatatypes::conflict(TNode a, TNode b){
if (a.getKind() == kind::CONST_BOOLEAN) {
void TheoryDatatypes::eqNotifyNewClass(TNode t){
if( t.getKind()==APPLY_CONSTRUCTOR ){
getOrMakeEqcInfo( t, true );
+ //look at all equivalence classes with constructor terms
+/*
+ for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
+ if( (*it).second ){
+ TNode r = (*it).first;
+ if( r.getType()==t.getType() ){
+ EqcInfo * ei = getOrMakeEqcInfo( r, false );
+ if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
+ Node deq = ei->d_constructor.get().eqNode( t ).negate();
+ d_pending.push_back( deq );
+ d_pending_exp[ deq ] = d_true;
+ Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
+ d_infer.push_back( deq );
+ }
+ }
+ }
+ }
+*/
+ d_consEqc[t] = true;
}
}
//if both have constructor, then either clash or unification
if( !cons1.isNull() && !cons2.isNull() ){
Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
- if( cons1.getOperator()!=cons2.getOperator() ){
+ Node unifEq = cons1.eqNode( cons2 );
+ std::vector< Node > exp;
+ if( checkClashModEq( cons1, cons2, exp ) ){
+ exp.push_back( unifEq );
//check for clash
- d_conflictNode = explain( cons1.eqNode( cons2 ) );
+ d_conflictNode = explain( exp );
Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
d_conflict = true;
return;
}else{
//do unification
- Node unifEq = cons1.eqNode( cons2 );
for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
- if( cons1[i]!=cons2[i] ){
+ if( !areEqual( cons1[i], cons2[i] ) ){
Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
d_pending.push_back( eq );
d_pending_exp[ eq ] = unifEq;
d_infer.push_back( eq );
d_infer_exp.push_back( unifEq );
}
+ }
+/*
+ std::vector< Node > rew;
+ if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
+ Assert(false);
+ }else{
+ for( unsigned i=0; i<rew.size(); i++ ){
+ d_pending.push_back( rew[i] );
+ d_pending_exp[ rew[i] ] = unifEq;
+ Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
+ d_infer.push_back( rew[i] );
+ d_infer_exp.push_back( unifEq );
+ }
}
+*/
}
}
if( !eqc1->d_inst && eqc2->d_inst ){
eqc1->d_inst = true;
}
- if( cons1.isNull() && !cons2.isNull() ){
- Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
- checkInst = true;
- addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
- if( d_conflict ){
- return;
+ if( !cons2.isNull() ){
+ if( cons1.isNull() ){
+ Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+ checkInst = true;
+ addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
+ if( d_conflict ){
+ return;
+ }
+ d_consEqc[t1] = true;
}
+ d_consEqc[t2] = false;
}
}else{
Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
//if( r!=rr ){
//Node eq_exp = NodeManager::currentNM()->mkConst(true);
//Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
- if( s!=rr ){
+ if( s!=rr ){::
Node eq_exp = c.eqNode( s[0] );
Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
}else if( !areEqual( x, y ) ){
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
//check if they are definately disequal
-
- if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
- Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
- //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- //if( eqStatus!=EQUALITY_UNKNOWN ){
- currentPairs.push_back(make_pair(x_shared, y_shared));
+ bool defDiseq = false;
+/*
+ TNode rx = getRepresentative( x );
+ EqcInfo* eix = getOrMakeEqcInfo( rx, false );
+ if( eix ){
+ TNode ry = getRepresentative( y );
+ EqcInfo* eiy = getOrMakeEqcInfo( ry, false );
+ if( eiy ){
+ if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){
+ defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator();
+ }else{
+ }
+ }
+ }
+*/
+ if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
+ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
+ if( eqStatus!=EQUALITY_UNKNOWN ){
+ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+ Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
+ currentPairs.push_back(make_pair(x_shared, y_shared));
+ }
}
}
}
if( rn!=n && !areEqual( rn, n ) ){
Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
d_pending.push_back( eq );
- d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
+ d_pending_exp[ eq ] = d_true;
Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
d_infer.push_back( eq );
}
Node exp;
Node tt;
if( !eqc->d_constructor.get().isNull() ){
- exp = NodeManager::currentNM()->mkConst( true );
+ exp = d_true;
tt = eqc->d_constructor;
}else{
exp = getLabel( n );
}
}
-Node TheoryDatatypes::getRepresentative( TNode a ){
+TNode TheoryDatatypes::getRepresentative( TNode a ){
if( hasTerm( a ) ){
return d_equalityEngine.getRepresentative( a );
}else{
Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
if( assumptions.empty() ){
- return NodeManager::currentNM()->mkConst( true );
+ return d_true;
}else if( assumptions.size()==1 ){
return assumptions[0];
}else{
return NodeManager::currentNM()->mkNode( AND, assumptions );
}
}
+
+bool TheoryDatatypes::checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ) {
+ if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
+ (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
+ (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
+ if( n1.getOperator() != n2.getOperator() ) {
+ return true;
+ } else {
+ Assert( n1.getNumChildren() == n2.getNumChildren() );
+ for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
+ TNode nc1 = n1[i];
+ TNode nc2 = n2[i];
+ if( DatatypesRewriter::isTermDatatype( n1[i] ) ){
+ nc1 = getEqcConstructor( n1[i] );
+ nc2 = getEqcConstructor( n2[i] );
+ }
+ if( checkClashModEq( nc1, nc2, exp ) ) {
+ if( nc1!=n1[i] ){
+ exp.push_back( nc1.eqNode( n1[i] ) );
+ }
+ if( nc2!=n2[i] ){
+ exp.push_back( nc2.eqNode( n2[i] ) );
+ }
+ return true;
+ }
+ }
+ }
+ }else if( n1!=n2 ){
+ if( n1.isConst() && n2.isConst() ){
+ return true;
+ }else{
+ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+ if( d_equalityEngine.areDisequal( n1, n2, true ) ){
+ exp.push_back( eq.negate() );
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
/** inferences */
NodeList d_infer;
NodeList d_infer_exp;
-
+ Node d_true;
/** mkAnd */
Node mkAnd( std::vector< TNode >& assumptions );
private:
NodeListMap d_labels;
/** selector apps for eqch equivalence class */
NodeListMap d_selector_apps;
+ /** constructor terms */
+ BoolMap d_consEqc;
/** Are we in conflict */
context::CDO<bool> d_conflict;
/** The conflict node */
EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
/** has eqc info */
bool hasEqcInfo( Node n ) { return d_labels.find( n )!=d_labels.end(); }
+ /** get eqc constructor */
+ TNode getEqcConstructor( TNode r );
protected:
/** compute care graph */
void computeCareGraph();
void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
void explain( TNode literal, std::vector<TNode>& assumptions );
Node explain( TNode literal );
+ Node explain( std::vector< Node >& lits );
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalance class is created */
bool mustSpecifyAssignment();
/** must communicate fact */
bool mustCommunicateFact( Node n, Node exp );
+ /** check clash mod eq */
+ bool checkClashModEq( Node n1, Node n2, std::vector< Node >& exp );
private:
//equality queries
bool hasTerm( TNode a );
bool areEqual( TNode a, TNode b );
bool areDisequal( TNode a, TNode b );
- Node getRepresentative( TNode a );
+ TNode getRepresentative( TNode a );
public:
/** get equality engine */
eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
bool isGroundRange(Node f, Node v);
+
+ /** Identify this module */
+ std::string identify() const { return "BoundedIntegers"; }
};
}
~Statistics();
};
Statistics d_statistics;
+ /** Identify this module */
+ std::string identify() const { return "InstEngine"; }
};/* class InstantiationEngine */
}/* CVC4::theory::quantifiers namespace */
void ModelEngine::check( Theory::Effort e ){
if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
- FirstOrderModel* fm = d_quantEngine->getModel();
- //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
int addedLemmas = 0;
- //quantifiers are initialized, we begin an instantiation round
- double clSet = 0;
- if( Trace.isOn("model-engine") ){
- clSet = double(clock())/double(CLOCKS_PER_SEC);
- }
- ++(d_statistics.d_inst_rounds);
- bool buildAtFullModel = d_builder->optBuildAtFullModel();
- //two effort levels: first try exhaustive instantiation without axioms, then with.
- int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
- for( int effort=startEffort; effort<2; effort++ ){
- // for effort = 0, we only instantiate non-axioms
- // for effort = 1, we instantiate everything
- if( addedLemmas==0 ){
- Trace("model-engine") << "---Model Engine Round---" << std::endl;
- //initialize the model
- Trace("model-engine-debug") << "Build model..." << std::endl;
- d_builder->d_considerAxioms = effort>=1;
- d_builder->d_addedLemmas = 0;
- d_builder->buildModel( fm, buildAtFullModel );
- addedLemmas += (int)d_builder->d_addedLemmas;
- //if builder has lemmas, add and return
+ bool needsBuild = true;
+ FirstOrderModel* fm = d_quantEngine->getModel();
+ if( fm->getNumAssertedQuantifiers()>0 ){
+ //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
+ //quantifiers are initialized, we begin an instantiation round
+ double clSet = 0;
+ if( Trace.isOn("model-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ }
+ ++(d_statistics.d_inst_rounds);
+ bool buildAtFullModel = d_builder->optBuildAtFullModel();
+ needsBuild = !buildAtFullModel;
+ //two effort levels: first try exhaustive instantiation without axioms, then with.
+ int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
+ for( int effort=startEffort; effort<2; effort++ ){
+ // for effort = 0, we only instantiate non-axioms
+ // for effort = 1, we instantiate everything
if( addedLemmas==0 ){
- Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
- //let the strong solver verify that the model is minimal
- //for debugging, this will if there are terms in the model that the strong solver was not notified of
- if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
- Trace("model-engine-debug") << "Check model..." << std::endl;
- d_incomplete_check = false;
- //print debug
- Debug("fmf-model-complete") << std::endl;
- debugPrint("fmf-model-complete");
- //successfully built an acceptable model, now check it
- addedLemmas += checkModel();
- }else{
- addedLemmas++;
+ Trace("model-engine") << "---Model Engine Round---" << std::endl;
+ //initialize the model
+ Trace("model-engine-debug") << "Build model..." << std::endl;
+ d_builder->d_considerAxioms = effort>=1;
+ d_builder->d_addedLemmas = 0;
+ d_builder->buildModel( fm, buildAtFullModel );
+ addedLemmas += (int)d_builder->d_addedLemmas;
+ //if builder has lemmas, add and return
+ if( addedLemmas==0 ){
+ Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
+ //let the strong solver verify that the model is minimal
+ //for debugging, this will if there are terms in the model that the strong solver was not notified of
+ if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
+ Trace("model-engine-debug") << "Check model..." << std::endl;
+ d_incomplete_check = false;
+ //print debug
+ Debug("fmf-model-complete") << std::endl;
+ debugPrint("fmf-model-complete");
+ //successfully built an acceptable model, now check it
+ addedLemmas += checkModel();
+ }else{
+ addedLemmas++;
+ }
}
}
- }
- if( addedLemmas==0 ){
- //if we have not added lemmas yet and axiomInstMode=trust, then we are done
- if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
- //we must return unknown if an axiom is asserted
- if( effort==0 ){
- d_incomplete_check = true;
+ if( addedLemmas==0 ){
+ //if we have not added lemmas yet and axiomInstMode=trust, then we are done
+ if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
+ //we must return unknown if an axiom is asserted
+ if( effort==0 ){
+ d_incomplete_check = true;
+ }
+ break;
}
- break;
}
}
- }
- if( Trace.isOn("model-engine") ){
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+ if( Trace.isOn("model-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+ }
+ }else{
+ Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl;
}
if( addedLemmas==0 ){
Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
//CVC4 will answer SAT or unknown
Trace("fmf-consistent") << std::endl;
debugPrint("fmf-consistent");
- if( options::produceModels() && !buildAtFullModel ){
+ if( options::produceModels() && needsBuild ){
// finish building the model
d_builder->buildModel( fm, true );
}
~Statistics();
};
Statistics d_statistics;
+ /** Identify this module */
+ std::string identify() const { return "ModelEngine"; }
};/* class ModelEngine */
}/* CVC4::theory::quantifiers namespace */
class QuantInfo {\r
private:\r
void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );\r
- void flatten( Node n, bool beneathQuant );
+ void flatten( Node n, bool beneathQuant );\r
private: //for completing match\r
std::vector< int > d_unassigned;\r
std::vector< TypeNode > d_unassigned_tn;\r
bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );\r
void revertMatch( std::vector< int >& assigned );\r
void debugPrintMatch( const char * c );\r
- bool isConstrainedVar( int v );
-public:
+ bool isConstrainedVar( int v );\r
+public:\r
void getMatch( std::vector< Node >& terms );\r
};\r
\r
~Statistics();\r
};\r
Statistics d_statistics;\r
+ /** Identify this module */\r
+ std::string identify() const { return "QcfEngine"; }\r
};\r
\r
}\r
void check( Theory::Effort e );
void registerQuantifier( Node f );
- void assertNode( Node n );
+ void assertNode( Node n );
+ /** Identify this module */
+ std::string identify() const { return "RewriteEngine"; }
};
}
Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
return;
}
+ Trace("quant-engine-debug") << "Resetting modules..." << std::endl;
//reset relevant information
d_hasAddedLemma = false;
d_term_db->reset( e );
for( int i=0; i<(int)d_modules.size(); i++ ){
d_modules[i]->reset_round( e );
}
+ Trace("quant-engine-debug") << "Done resetting modules." << std::endl;
+
if( e==Theory::EFFORT_LAST_CALL ){
//if effort is last call, try to minimize model first
if( options::finiteModelFind() ){
}else if( e==Theory::EFFORT_FULL ){
++(d_statistics.d_instantiation_rounds);
}
+ Trace("quant-engine-debug") << "Check with modules..." << std::endl;
for( int i=0; i<(int)d_modules.size(); i++ ){
+ Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
d_modules[i]->check( e );
}
+ Trace("quant-engine-debug") << "Done check with modules." << std::endl;
//build the model if not done so already
// this happens if no quantifiers are currently asserted and no model-building module is enabled
if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
if( options::produceModels() && !d_model->isModelSet() ){
+ Trace("quant-engine-debug") << "Build the model..." << std::endl;
d_te->getModelBuilder()->buildModel( d_model, true );
+ Trace("quant-engine-debug") << "Done building the model." << std::endl;
}
if( Trace.isOn("inst-per-quant") ){
for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
virtual void propagate( Theory::Effort level ){}
virtual Node getNextDecisionRequest() { return TNode::null(); }
virtual Node explain(TNode n) { return TNode::null(); }
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const = 0;
};/* class QuantifiersModule */
namespace quantifiers {
projects / cvc5.git / commitdiff