From 089d232454e89dc44a6ca2136f9b408c9335d8f1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 10 Oct 2014 23:27:39 +0200 Subject: [PATCH] Initial draft of CEGQI. --- .../quantifiers/ce_guided_instantiation.cpp | 181 +++++++++++++++++- .../quantifiers/ce_guided_instantiation.h | 43 +++++ .../quantifiers/conjecture_generator.cpp | 54 +----- src/theory/quantifiers/conjecture_generator.h | 13 -- .../quantifiers/quant_conflict_find.cpp | 21 -- src/theory/quantifiers/quant_conflict_find.h | 5 - src/theory/quantifiers/term_database.cpp | 35 ++++ src/theory/quantifiers/term_database.h | 24 ++- src/theory/quantifiers/theory_quantifiers.cpp | 2 + src/theory/quantifiers_engine.cpp | 30 ++- src/theory/quantifiers_engine.h | 11 +- 11 files changed, 315 insertions(+), 104 deletions(-) diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index fec4255b2..f4cdd1a60 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -27,21 +27,190 @@ using namespace std; namespace CVC4 { -CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { +CegInstantiation::CegConjecture::CegConjecture() { +} + +void CegInstantiation::CegConjecture::assign( Node q ) { + Assert( d_quant.isNull() ); + Assert( q.getKind()==FORALL ); + d_quant = q; + for( unsigned i=0; imkSkolem( "e", q[0][i].getType() ) ); + } +} +void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ + if( d_guard.isNull() ){ + d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + //specify guard behavior + qe->getValuation().ensureLiteral( d_guard ); + qe->getOutputChannel().requirePhase( d_guard, true ); + } +} + +CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) { - +} + +bool CegInstantiation::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { - //TODO + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl; + Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl; + if( d_conj_active && !d_conj_infeasible ){ + checkCegConjecture( &d_conj ); + } + Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl; + } } void CegInstantiation::registerQuantifier( Node q ) { - //TODO + if( d_quantEngine->getOwner( q )==this ){ + if( !d_conj.isAssigned() ){ + Trace("cegqi") << "Register conjecture : " << q << std::endl; + d_conj.assign( q ); + //construct base instantiation + d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) ); + Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl; + if( getTermDatabase()->isQAttrSygus( q ) ){ + Assert( d_conj.d_base_inst.getKind()==NOT ); + Assert( d_conj.d_base_inst[0].getKind()==FORALL ); + for( unsigned j=0; jisQAttrSynthesis( q ) ){ + //add immediate lemma + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst ); + } + }else{ + Assert( d_conj.d_quant==q ); + } + } } void CegInstantiation::assertNode( Node n ) { - + Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl; + bool pol = n.getKind()!=NOT; + Node lit = n.getKind()==NOT ? n[0] : n; + if( lit==d_conj.d_guard ){ + d_guard_assertions[lit] = pol; + d_conj_infeasible = !pol; + } + if( lit==d_conj.d_quant ){ + d_conj_active = true; + } +} + +Node CegInstantiation::getNextDecisionRequest() { + d_conj.initializeGuard( d_quantEngine ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) { + if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){ + if( d_conj.d_guard_split.isNull() ){ + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard ); + d_quantEngine->getOutputChannel().lemma( lem ); + } + Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl; + return d_conj.d_guard; + } + } + return Node::null(); +} + +void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { + Node q = conj->d_quant; + Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; + Trace("cegqi-engine-debug") << " * Candidate program/output : "; + for( unsigned i=0; id_candidates.size(); i++ ){ + Trace("cegqi-engine-debug") << conj->d_candidates[i] << " "; + } + Trace("cegqi-engine-debug") << std::endl; + + if( getTermDatabase()->isQAttrSygus( q ) ){ + Trace("cegqi-engine-debug") << " * Values are : "; + bool success = true; + std::vector< Node > model_values; + for( unsigned i=0; id_candidates.size(); i++ ){ + Node v = getModelValue( conj->d_candidates[i] ); + model_values.push_back( v ); + Trace("cegqi-engine-debug") << v << " "; + if( v.isNull() ){ + success = false; + } + } + Trace("cegqi-engine-debug") << std::endl; + + if( success ){ + //must get a counterexample to the value of the current candidate + Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); + inst = Rewriter::rewrite( inst ); + //body should be an existential + Assert( inst.getKind()==NOT ); + Assert( inst[0].getKind()==FORALL ); + //immediately skolemize + Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ); + Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; + d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) ); + + //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate + Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() ); + Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(), + getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() ); + Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() ); + Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem ); + } + + }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + std::vector< Node > model_terms; + for( unsigned i=0; id_candidates.size(); i++ ){ + Node t = getModelTerm( conj->d_candidates[i] ); + model_terms.push_back( t ); + } + d_quantEngine->addInstantiation( q, model_terms, false ); + } } - + +Node CegInstantiation::getModelValue( Node n ) { + Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; + //return d_quantEngine->getTheoryEngine()->getModelValue( n ); + TypeNode tn = n.getType(); + if( getEqualityEngine()->hasTerm( n ) ){ + Node r = getRepresentative( n ); + Node v; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + TNode nn = (*eqc_i); + if( nn.isConst() ){ + Trace("cegqi-mv") << "..constant : " << nn << std::endl; + return nn; + }else if( nn.getKind()==APPLY_CONSTRUCTOR ){ + v = nn; + } + ++eqc_i; + } + if( !v.isNull() ){ + std::vector< Node > children; + if( v.hasOperator() ){ + children.push_back( v.getOperator() ); + } + for( unsigned i=0; imkNode( v.getKind(), children ); + Trace("cegqi-mv") << "...value : " << vv << std::endl; + return vv; + } + } + Node e = getTermDatabase()->getEnumerateTerm( tn, 0 ); + Trace("cegqi-mv") << "...enumerate : " << e << std::endl; + return e; +} + +Node CegInstantiation::getModelTerm( Node n ){ + return getModelValue( n ); +} + } \ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 7861deffa..6139f8f59 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -25,16 +25,59 @@ namespace CVC4 { namespace theory { namespace quantifiers { + + class CegInstantiation : public QuantifiersModule { + typedef context::CDHashMap NodeBoolMap; +private: + class CegConjecture { + public: + CegConjecture(); + /** quantified formula */ + Node d_quant; + /** guard */ + Node d_guard; + /** base instantiation */ + Node d_base_inst; + /** guard split */ + Node d_guard_split; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + /** is assigned */ + bool isAssigned() { return !d_quant.isNull(); } + /** assign */ + void assign( Node q ); + /** initialize guard */ + void initializeGuard( QuantifiersEngine * qe ); + }; + /** the quantified formula stating the synthesis conjecture */ + CegConjecture d_conj; + /** is conjecture active */ + context::CDO< bool > d_conj_active; + /** is conjecture infeasible */ + context::CDO< bool > d_conj_infeasible; + /** assertions for guards */ + NodeBoolMap d_guard_assertions; +private: + /** check conjecture */ + void checkCegConjecture( CegConjecture * conj ); + /** get model value */ + Node getModelValue( Node n ); + /** get model term */ + Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: + bool needsCheck( Theory::Effort e ); /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ void registerQuantifier( Node q ); void assertNode( Node n ); + Node getNextDecisionRequest(); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } }; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fe3c92323..f491adc7c 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -280,33 +280,6 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { } } -eq::EqualityEngine * ConjectureGenerator::getEqualityEngine() { - return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); -} - -bool ConjectureGenerator::areEqual( TNode n1, TNode n2 ) { - eq::EqualityEngine * ee = getEqualityEngine(); - return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) ); -} - -bool ConjectureGenerator::areDisequal( TNode n1, TNode n2 ) { - eq::EqualityEngine * ee = getEqualityEngine(); - return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false ); -} - -TNode ConjectureGenerator::getRepresentative( TNode n ) { - eq::EqualityEngine * ee = getEqualityEngine(); - if( ee->hasTerm( n ) ){ - return ee->getRepresentative( n ); - }else{ - return n; - } -} - -TermDb * ConjectureGenerator::getTermDatabase() { - return d_quantEngine->getTermDatabase(); -} - Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { Assert( !tn.isNull() ); while( d_free_var[tn].size()<=i ){ @@ -1098,27 +1071,6 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo } } -Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) { - std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); - unsigned teIndex; - if( it==d_typ_enum_map.end() ){ - teIndex = (int)d_typ_enum.size(); - d_typ_enum_map[tn] = teIndex; - d_typ_enum.push_back( TypeEnumerator(tn) ); - }else{ - teIndex = it->second; - } - while( index>=d_enum_terms[tn].size() ){ - if( d_typ_enum[teIndex].isFinished() ){ - return Node::null(); - } - d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); - ++d_typ_enum[teIndex]; - } - return d_enum_terms[tn][index]; -} - - Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn ); if( it==d_typ_pred.end() ){ @@ -1149,7 +1101,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec.push_back( size_limit ); }else{ //see if we can iterate current - if( vec_sumgetEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){ vec[index]++; vec_sum++; vec.push_back( size_limit - vec_sum ); @@ -1164,7 +1116,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } if( success ){ if( vec.size()==n.getNumChildren() ){ - Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] ); + Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] ); if( !lc.isNull() ){ for( unsigned i=0; i children; children.push_back( n.getOperator() ); for( unsigned i=0; i<(vec.size()-1); i++ ){ - Node nn = getEnumerateTerm( n[i].getType(), vec[i] ); + Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] ); Assert( !nn.isNull() ); Assert( nn.getType()==n[i].getType() ); children.push_back( nn ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 23e2b88ba..59d908fec 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -357,13 +357,6 @@ public: //for generalization // get generalization depth int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ); private: - //ground term enumeration - std::map< TypeNode, std::vector< Node > > d_enum_terms; - //type enumerators - std::map< TypeNode, unsigned > d_typ_enum_map; - std::vector< TypeEnumerator > d_typ_enum; - //get nth term for type - Node getEnumerateTerm( TypeNode tn, unsigned index ); //predicate for type std::map< TypeNode, Node > d_typ_pred; //get predicate for type @@ -389,12 +382,6 @@ public: //for property enumeration std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain; //number of ground substitutions whose equality is unknown unsigned d_subs_unkCount; -public: //for ground equivalence classes - eq::EqualityEngine * getEqualityEngine(); - bool areDisequal( TNode n1, TNode n2 ); - bool areEqual( TNode n1, TNode n2 ); - TNode getRepresentative( TNode n ); - TermDb * getTermDatabase(); private: //information about ground equivalence classes TNode d_bool_eqc[2]; std::map< TNode, Node > d_ground_eqc_map; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 060994379..8136bf11e 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1851,27 +1851,6 @@ void QuantConflictFind::assertNode( Node q ) { } } -eq::EqualityEngine * QuantConflictFind::getEqualityEngine() { - //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine(); - return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); -} -bool QuantConflictFind::areEqual( Node n1, Node n2 ) { - return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 ); -} -bool QuantConflictFind::areDisequal( Node n1, Node n2 ) { - return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false ); -} -Node QuantConflictFind::getRepresentative( Node n ) { - if( getEqualityEngine()->hasTerm( n ) ){ - return getEqualityEngine()->getRepresentative( n ); - }else{ - return n; - } -} -TermDb* QuantConflictFind::getTermDatabase() { - return d_quantEngine->getTermDatabase(); -} - Node QuantConflictFind::evaluateTerm( Node n ) { if( MatchGen::isHandledUfTerm( n ) ){ Node f = MatchGen::getOperator( this, n ); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d8f1c8e6f..81f31fa90 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -187,11 +187,6 @@ private: NodeList d_qassert; std::map< Node, QuantInfo > d_qinfo; private: //for equivalence classes - eq::EqualityEngine * getEqualityEngine(); - bool areDisequal( Node n1, Node n2 ); - bool areEqual( Node n1, Node n2 ); - Node getRepresentative( Node n ); - TermDb* getTermDatabase(); // type -> list(eqc) std::map< TypeNode, std::vector< TNode > > d_eqcs; std::map< TypeNode, Node > d_model_basis; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 405b3749d..9c1eeb9b4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -751,6 +751,27 @@ Node TermDb::getSkolemizedBody( Node f ){ return d_skolem_body[ f ]; } +Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); + unsigned teIndex; + if( it==d_typ_enum_map.end() ){ + teIndex = (int)d_typ_enum.size(); + d_typ_enum_map[tn] = teIndex; + d_typ_enum.push_back( TypeEnumerator(tn) ); + }else{ + teIndex = it->second; + } + while( index>=d_enum_terms[tn].size() ){ + if( d_typ_enum[teIndex].isFinished() ){ + return Node::null(); + } + d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); + ++d_typ_enum[teIndex]; + } + return d_enum_terms[tn][index]; +} + + Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ @@ -983,6 +1004,7 @@ Node TermDb::getRewriteRule( Node q ) { void TermDb::computeAttributes( Node q ) { if( q.getNumChildren()==3 ){ for( unsigned i=0; igetCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); } if( avar.getAttribute(SynthesisAttribute()) ){ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; d_qattr_synthesis[q] = true; + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ @@ -1012,7 +1043,11 @@ void TermDb::computeAttributes( Node q ) { Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl; } if( avar.getKind()==REWRITE_RULE ){ + Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; Assert( i==0 ); + if( d_quantEngine->getRewriteEngine()==NULL ){ + Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; + } //set rewrite engine as owner d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3bd0563b6..25ef9c81c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -19,6 +19,7 @@ #include "expr/attribute.h" #include "theory/theory.h" +#include "theory/type_enumerator.h" #include @@ -241,6 +242,8 @@ public: public: //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); + + //for skolem private: /** map from universal quantifiers to their skolemized body */ @@ -253,7 +256,20 @@ public: std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ); /** get the skolemized body */ Node getSkolemizedBody( Node f); - + /** is induction variable */ + static bool isInductionTerm( Node n ); + +//for ground term enumeration +private: + /** ground terms enumerated for types */ + std::map< TypeNode, std::vector< Node > > d_enum_terms; + //type enumerators + std::map< TypeNode, unsigned > d_typ_enum_map; + std::vector< TypeEnumerator > d_typ_enum; +public: + //get nth term for type + Node getEnumerateTerm( TypeNode tn, unsigned index ); + //miscellaneous public: /** map from universal quantifiers to the list of variables */ @@ -289,11 +305,7 @@ public: int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); - -public: //for induction - /** is induction variable */ - static bool isInductionTerm( Node n ); - + public: //general queries concerning quantified formulas wrt modules /** is quantifier treated as a rewrite rule? */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e71489fc5..f7c4c745f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -42,6 +42,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); + out.handleUserAttribute( "sygus", this ); + out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dfa17558d..d17899cf2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -43,6 +43,34 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; + +eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { + return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); +} + +bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) ); +} + +bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false ); +} + +TNode QuantifiersModule::getRepresentative( TNode n ) { + eq::EqualityEngine * ee = getEqualityEngine(); + if( ee->hasTerm( n ) ){ + return ee->getRepresentative( n ); + }else{ + return n; + } +} + +quantifiers::TermDb * QuantifiersModule::getTermDatabase() { + return d_quantEngine->getTermDatabase(); +} + QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), d_lemmas_produced_c(u){ @@ -184,7 +212,7 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { QuantifiersModule * mo = getOwner( q ); if( mo!=m ){ if( mo!=NULL ){ - Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << m->identify() << ", but already has owner " << mo->identify() << "!" << std::endl; + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl; } d_owner[q] = m; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d40277112..b5a02df60 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -37,6 +37,10 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { + class TermDb; +} + class QuantifiersModule { protected: QuantifiersEngine* d_quantEngine; @@ -61,10 +65,15 @@ public: virtual Node explain(TNode n) { return TNode::null(); } /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; +public: + eq::EqualityEngine * getEqualityEngine(); + bool areDisequal( TNode n1, TNode n2 ); + bool areEqual( TNode n1, TNode n2 ); + TNode getRepresentative( TNode n ); + quantifiers::TermDb * getTermDatabase(); };/* class QuantifiersModule */ namespace quantifiers { - class TermDb; class FirstOrderModel; //modules class InstantiationEngine; -- 2.30.2