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; i<q[0].getNumChildren(); i++ ){
+ d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "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; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){
+ d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] );
+ }
+ }else if( getTermDatabase()->isQAttrSynthesis( 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; i<conj->d_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; i<conj->d_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; i<conj->d_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; i<v.getNumChildren(); i++ ){
+ children.push_back( getModelValue( v[i] ) );
+ }
+ Node vv = NodeManager::currentNM()->mkNode( 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
namespace theory {
namespace quantifiers {
+
+
class CegInstantiation : public QuantifiersModule
{
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> 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"; }
};
}\r
}\r
\r
-eq::EqualityEngine * ConjectureGenerator::getEqualityEngine() {\r
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();\r
-}\r
-\r
-bool ConjectureGenerator::areEqual( TNode n1, TNode n2 ) {\r
- eq::EqualityEngine * ee = getEqualityEngine();\r
- return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );\r
-}\r
-\r
-bool ConjectureGenerator::areDisequal( TNode n1, TNode n2 ) {\r
- eq::EqualityEngine * ee = getEqualityEngine();\r
- return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );\r
-}\r
-\r
-TNode ConjectureGenerator::getRepresentative( TNode n ) {\r
- eq::EqualityEngine * ee = getEqualityEngine();\r
- if( ee->hasTerm( n ) ){\r
- return ee->getRepresentative( n );\r
- }else{\r
- return n;\r
- }\r
-}\r
-\r
-TermDb * ConjectureGenerator::getTermDatabase() {\r
- return d_quantEngine->getTermDatabase();\r
-}\r
-\r
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {\r
Assert( !tn.isNull() );\r
while( d_free_var[tn].size()<=i ){\r
}\r
}\r
\r
-Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {\r
- std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );\r
- unsigned teIndex;\r
- if( it==d_typ_enum_map.end() ){\r
- teIndex = (int)d_typ_enum.size();\r
- d_typ_enum_map[tn] = teIndex;\r
- d_typ_enum.push_back( TypeEnumerator(tn) );\r
- }else{\r
- teIndex = it->second;\r
- }\r
- while( index>=d_enum_terms[tn].size() ){\r
- if( d_typ_enum[teIndex].isFinished() ){\r
- return Node::null();\r
- }\r
- d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );\r
- ++d_typ_enum[teIndex];\r
- }\r
- return d_enum_terms[tn][index];\r
-}\r
-\r
-\r
Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {\r
std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );\r
if( it==d_typ_pred.end() ){\r
vec.push_back( size_limit );\r
}else{\r
//see if we can iterate current\r
- if( vec_sum<size_limit && !getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){\r
+ if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){\r
vec[index]++;\r
vec_sum++;\r
vec.push_back( size_limit - vec_sum );\r
}\r
if( success ){\r
if( vec.size()==n.getNumChildren() ){\r
- Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );\r
+ Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );\r
if( !lc.isNull() ){\r
for( unsigned i=0; i<vec.size(); i++ ){\r
Trace("sg-gt-enum-debug") << vec[i] << " ";\r
std::vector< Node > children;\r
children.push_back( n.getOperator() );\r
for( unsigned i=0; i<(vec.size()-1); i++ ){\r
- Node nn = getEnumerateTerm( n[i].getType(), vec[i] );\r
+ Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] );\r
Assert( !nn.isNull() );\r
Assert( nn.getType()==n[i].getType() );\r
children.push_back( nn );\r
// get generalization depth\r
int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );\r
private:\r
- //ground term enumeration\r
- std::map< TypeNode, std::vector< Node > > d_enum_terms;\r
- //type enumerators\r
- std::map< TypeNode, unsigned > d_typ_enum_map;\r
- std::vector< TypeEnumerator > d_typ_enum;\r
- //get nth term for type\r
- Node getEnumerateTerm( TypeNode tn, unsigned index );\r
//predicate for type\r
std::map< TypeNode, Node > d_typ_pred;\r
//get predicate for type\r
std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;\r
//number of ground substitutions whose equality is unknown\r
unsigned d_subs_unkCount;\r
-public: //for ground equivalence classes\r
- eq::EqualityEngine * getEqualityEngine();\r
- bool areDisequal( TNode n1, TNode n2 );\r
- bool areEqual( TNode n1, TNode n2 );\r
- TNode getRepresentative( TNode n );\r
- TermDb * getTermDatabase();\r
private: //information about ground equivalence classes\r
TNode d_bool_eqc[2];\r
std::map< TNode, Node > d_ground_eqc_map;\r
}\r
}\r
\r
-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {\r
- //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();\r
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();\r
-}\r
-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {\r
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );\r
-}\r
-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {\r
- return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
-}\r
-Node QuantConflictFind::getRepresentative( Node n ) {\r
- if( getEqualityEngine()->hasTerm( n ) ){\r
- return getEqualityEngine()->getRepresentative( n );\r
- }else{\r
- return n;\r
- }\r
-}\r
-TermDb* QuantConflictFind::getTermDatabase() { \r
- return d_quantEngine->getTermDatabase();\r
-}\r
-\r
Node QuantConflictFind::evaluateTerm( Node n ) {\r
if( MatchGen::isHandledUfTerm( n ) ){\r
Node f = MatchGen::getOperator( this, n );\r
NodeList d_qassert;\r
std::map< Node, QuantInfo > d_qinfo;\r
private: //for equivalence classes\r
- eq::EqualityEngine * getEqualityEngine();\r
- bool areDisequal( Node n1, Node n2 );\r
- bool areEqual( Node n1, Node n2 );\r
- Node getRepresentative( Node n );\r
- TermDb* getTermDatabase();\r
// type -> list(eqc)\r
std::map< TypeNode, std::vector< TNode > > d_eqcs;\r
std::map< TypeNode, Node > d_model_basis;\r
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() ){
void TermDb::computeAttributes( Node q ) {
if( q.getNumChildren()==3 ){
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
if( q[2][i].getKind()==INST_ATTRIBUTE ){
Node avar = q[2][i][0];
if( avar.getAttribute(AxiomAttribute()) ){
d_qattr_conjecture[q] = true;
}
if( avar.getAttribute(SygusAttribute()) ){
+ //should be nested existential
+ Assert( q[1].getKind()==NOT );
+ Assert( q[1][0].getKind()==FORALL );
Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
d_qattr_sygus[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.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()) ){
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() );
}
#include "expr/attribute.h"
#include "theory/theory.h"
+#include "theory/type_enumerator.h"
#include <map>
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 */
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 */
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? */
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 );
}
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){
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;
}
class QuantifiersEngine;
+namespace quantifiers {
+ class TermDb;
+}
+
class QuantifiersModule {
protected:
QuantifiersEngine* d_quantEngine;
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;
projects / cvc5.git / commitdiff