theory/quantifiers/ce_guided_single_inv.cpp \
theory/quantifiers/ce_guided_single_inv_sol.h \
theory/quantifiers/ce_guided_single_inv_sol.cpp \
+ theory/quantifiers/ce_guided_single_inv_ei.h \
+ theory/quantifiers/ce_guided_single_inv_ei.cpp \
theory/quantifiers/local_theory_ext.h \
theory/quantifiers/local_theory_ext.cpp \
theory/quantifiers/fun_def_process.h \
}
void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
- if( isAssigned() && d_guard.isNull() ){
- d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
- //specify guard behavior
- d_guard = qe->getValuation().ensureLiteral( d_guard );
- AlwaysAssert( !d_guard.isNull() );
- qe->getOutputChannel().requirePhase( d_guard, true );
+ if( isAssigned() ){
if( !d_syntax_guided ){
- //add immediate lemma
- Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
- Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl;
- qe->getOutputChannel().lemma( lem );
- }else if( d_ceg_si ){
+ if( d_nsg_guard.isNull() ){
+ d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+ d_nsg_guard = qe->getValuation().ensureLiteral( d_nsg_guard );
+ AlwaysAssert( !d_nsg_guard.isNull() );
+ qe->getOutputChannel().requirePhase( d_nsg_guard, true );
+ //add immediate lemma
+ Node lem = NodeManager::currentNM()->mkNode( OR, d_nsg_guard.negate(), d_base_inst.negate() );
+ Trace("cegqi-lemma") << "Cegqi::Lemma : non-syntax-guided : " << lem << std::endl;
+ qe->getOutputChannel().lemma( lem );
+ }
+ }else if( d_ceg_si->d_si_guard.isNull() ){
std::vector< Node > lems;
- d_ceg_si->getInitialSingleInvLemma( d_guard, lems );
+ d_ceg_si->getInitialSingleInvLemma( lems );
for( unsigned i=0; i<lems.size(); i++ ){
- Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
qe->getOutputChannel().lemma( lems[i] );
if( Trace.isOn("cegqi-debug") ){
Node rlem = Rewriter::rewrite( lems[i] );
}
}
}
+ Assert( !getGuard().isNull() );
}
}
d_lits[i] = lit;
Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
- Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl;
qe->getOutputChannel().lemma( lem );
qe->getOutputChannel().requirePhase( lit, true );
lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
}
Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
- Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl;
qe->getOutputChannel().lemma( hlem );
}
return lit;
}
}
+Node CegConjecture::getGuard() {
+ return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard;
+}
+
CegqiFairMode CegConjecture::getCegqiFairMode() {
return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair();
}
return d_ceg_si->isFullySingleInvocation();
}
-bool CegConjecture::needsCheck() {
- return !isSingleInvocation() || d_ceg_si->needsCheck();
+bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
+ if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
+ return false;
+ }else{
+ bool value;
+ if( !isSingleInvocation() || isFullySingleInvocation() ){
+ Assert( !getGuard().isNull() );
+ // non or fully single invocation : look at guard only
+ if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
+ if( !value ){
+ Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+ return false;
+ }
+ }else{
+ Assert( false );
+ }
+ }else{
+ // not fully single invocation : infeasible if overall specification is infeasible
+ Assert( !d_ceg_si->d_full_guard.isNull() );
+ if( d_qe->getValuation().hasSatValue( d_ceg_si->d_full_guard, value ) ) {
+ if( !value ){
+ Trace("cegqi-nsi") << "NSI : found full specification is infeasible." << std::endl;
+ return false;
+ }else{
+ Assert( !d_ceg_si->d_si_guard.isNull() );
+ if( d_qe->getValuation().hasSatValue( d_ceg_si->d_si_guard, value ) ) {
+ if( !value ){
+ if( !d_ceg_si->d_single_inv_exp.isNull() ){
+ //this should happen infrequently : only if cegqi determines infeasibility of a false candidate before E-matching does
+ Trace("cegqi-nsi") << "NSI : current single invocation lemma was infeasible, block assignment upon which conjecture was based." << std::endl;
+ Node l = NodeManager::currentNM()->mkNode( OR, d_ceg_si->d_full_guard.negate(), d_ceg_si->d_single_inv_exp );
+ lem.push_back( l );
+ d_ceg_si->initializeNextSiConjecture();
+ }
+ return false;
+ }
+ }else{
+ Assert( false );
+ }
+ }
+ }else{
+ Assert( false );
+ }
+ }
+ return true;
+ }
}
void CegConjecture::preregisterConjecture( Node q ) {
}
unsigned CegInstantiation::needsModel( Theory::Effort e ) {
- return QuantifiersEngine::QEFFORT_MODEL;
+ return d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
}
void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
- if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+ unsigned echeck = d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+ if( quant_e==echeck ){
Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
Trace("cegqi-engine-debug") << std::endl;
bool active = false;
- bool feasible = false;
bool value;
if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) {
active = value;
}else{
Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl;
}
- if( d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
- feasible = value;
- }else{
- Trace("cegqi-engine-debug") << "...no value for guard." << std::endl;
- }
- Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << " feasible : " << feasible << std::endl;
- if( active && feasible && d_conj->needsCheck() ){
+ Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << std::endl;
+ std::vector< Node > lem;
+ if( active && d_conj->needsCheck( lem ) ){
checkCegConjecture( d_conj );
+ }else{
+ for( unsigned i=0; i<lem.size(); i++ ){
+ Trace("cegqi-lemma") << "Cegqi::Lemma : check lemma : " << lem[i] << std::endl;
+ d_quantEngine->getOutputChannel().lemma( lem[i] );
+ }
}
Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
}
if( d_conj->isAssigned() ){
d_conj->initializeGuard( d_quantEngine );
std::vector< Node > req_dec;
- req_dec.push_back( d_conj->d_guard );
- if( d_conj->d_ceg_si && !d_conj->d_ceg_si->d_ns_guard.isNull() ){
- req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+ req_dec.push_back( d_conj->getGuard() );
+ if( d_conj->d_ceg_si ){
+ if( !d_conj->d_ceg_si->d_full_guard.isNull() ){
+ req_dec.push_back( d_conj->d_ceg_si->d_full_guard );
+ }
+ if( !d_conj->d_ceg_si->d_ns_guard.isNull() ){
+ req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+ }
}
for( unsigned i=0; i<req_dec.size(); i++ ){
bool value;
if( !lems.empty() ){
d_last_inst_si = true;
for( unsigned j=0; j<lems.size(); j++ ){
- Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << lems[j] << std::endl;
d_quantEngine->addLemma( lems[j] );
}
d_statistics.d_cegqi_si_lemmas += lems.size();
}
if( !lems.empty() ){
for( unsigned j=0; j<lems.size(); j++ ){
- Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : measure : " << lems[j] << std::endl;
d_quantEngine->addLemma( lems[j] );
}
Trace("cegqi-engine") << " ...refine size." << std::endl;
Node lem = NodeManager::currentNM()->mkNode( OR, ic );
lem = Rewriter::rewrite( lem );
d_last_inst_si = false;
- Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
d_quantEngine->addLemma( lem );
++(d_statistics.d_cegqi_lemmas_ce);
Trace("cegqi-engine") << " ...find counterexample." << std::endl;
}
if( success ){
Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
- lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), lem );
+ lem = NodeManager::currentNM()->mkNode( OR, conj->getGuard().negate(), lem );
lem = Rewriter::rewrite( lem );
- Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+ Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
Trace("cegqi-engine") << " ...refine candidate." << std::endl;
d_quantEngine->addLemma( lem );
++(d_statistics.d_cegqi_lemmas_refine);
Node d_assert_quant;
/** quantified formula (after processing) */
Node d_quant;
- /** guard */
- Node d_guard;
/** base instantiation */
Node d_base_inst;
/** expand base inst to disjuncts */
std::vector< Node > d_base_disj;
- /** guard split */
- Node d_guard_split;
- /** is syntax-guided */
- bool d_syntax_guided;
/** list of constants for quantified formula */
std::vector< Node > d_candidates;
/** list of variables on inner quantification */
std::vector< std::vector< Node > > d_inner_vars_disj;
/** list of terms we have instantiated candidates with */
std::map< int, std::vector< Node > > d_candidate_inst;
- /** initialize guard */
- void initializeGuard( QuantifiersEngine * qe );
/** measure term */
Node d_measure_term;
/** measure sum size */
int d_measure_term_size;
/** refine count */
unsigned d_refine_count;
- /** assign */
- void assign( Node q );
- /** is assigned */
- bool isAssigned() { return !d_quant.isNull(); }
/** current extential quantifeirs whose couterexamples we must refine */
std::vector< std::vector< Node > > d_ce_sk;
/** single invocation utility */
CegConjectureSingleInv * d_ceg_si;
+public: //non-syntax guided (deprecated)
+ /** guard */
+ bool d_syntax_guided;
+ Node d_nsg_guard;
public: //for fairness
/** the cardinality literals */
std::map< int, Node > d_lits;
context::CDO< int > d_curr_lit;
/** allocate literal */
Node getLiteral( QuantifiersEngine * qe, int i );
+ /** get guard */
+ Node getGuard();
/** is ground */
bool isGround() { return d_inner_vars.empty(); }
/** fairness */
/** is single invocation */
bool isFullySingleInvocation();
/** needs check */
- bool needsCheck();
+ bool needsCheck( std::vector< Node >& lem );
/** preregister conjecture */
void preregisterConjecture( Node q );
+ /** initialize guard */
+ void initializeGuard( QuantifiersEngine * qe );
+ /** assign */
+ void assign( Node q );
+ /** is assigned */
+ bool isAssigned() { return !d_quant.isNull(); }
};
#include "theory/quantifiers/ce_guided_single_inv.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/ce_guided_single_inv_ei.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
}else{
d_c_inst_match_trie = NULL;
}
- CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+ d_cosi = new CegqiOutputSingleInv( this );
// third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
- d_cinst = new CegInstantiator( qe, cosi, false, false );
+ d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
d_sol = new CegConjectureSingleInvSol( qe );
d_sip = new SingleInvocationPartition;
+
+ if( options::cegqiSingleInvPartial() ){
+ d_ei = new CegEntailmentInfer( qe, d_sip );
+ }else{
+ d_ei = NULL;
+ }
}
-void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ) {
+void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
+ Assert( d_si_guard.isNull() );
+ //single invocation guard
+ d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+ d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard );
+ AlwaysAssert( !d_si_guard.isNull() );
+ d_qe->getOutputChannel().requirePhase( d_si_guard, true );
+
if( !d_single_inv.isNull() ) {
+ //make for new var/sk
d_single_inv_var.clear();
d_single_inv_sk.clear();
Node inst;
Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
//register with the instantiator
- Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+ Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst );
lems.push_back( ginst );
+ //make and register the instantiator
+ if( d_cinst ){
+ delete d_cinst;
+ }
+ d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
}
}
if( !d_sip->d_conjuncts[1].empty() ){
singleInvocation = false;
if( options::cegqiSingleInvPartial() ){
- /* TODO : this enables partially single invocation techniques
+ //this enables partially single invocation techniques
d_nsingle_inv = d_sip->getNonSingleInvocation();
d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv );
d_full_inv = d_sip->getFullSpecification();
d_full_inv = TermDb::simpleNegate( d_full_inv );
singleInvocation = true;
- */
}else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
//if we are doing invariant templates, then construct the template
std::map< Node, bool > has_inv;
//just invoke the presolve now
d_cinst->presolve( d_single_inv );
}
- if( !d_nsingle_inv.isNull() ){
+ if( !isFullySingleInvocation() ){
//initialize information as next single invocation conjecture
initializeNextSiConjecture();
Trace("cegqi-si") << "Non-single invocation formula is : " << d_nsingle_inv << std::endl;
Trace("cegqi-si") << "Full specification is : " << d_full_inv << std::endl;
+ //add full specification lemma : will use for testing infeasibility/deriving entailments
+ d_full_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GF", NodeManager::currentNM()->booleanType() ) );
+ d_full_guard = d_qe->getValuation().ensureLiteral( d_full_guard );
+ AlwaysAssert( !d_full_guard.isNull() );
+ d_qe->getOutputChannel().requirePhase( d_full_guard, true );
+ Node fbvl;
+ if( !d_sip->d_all_vars.empty() ){
+ fbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_all_vars );
+ }
+ std::vector< Node > flem_c;
+ for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){
+ Node flemi = d_sip->d_conjuncts[2][i];
+ if( !fbvl.isNull() ){
+ flemi = NodeManager::currentNM()->mkNode( FORALL, fbvl, flemi );
+ }
+ flem_c.push_back( flemi );
+ }
+ Node flem = flem_c.empty() ? d_qe->getTermDatabase()->d_true : ( flem_c.size()==1 ? flem_c[0] : NodeManager::currentNM()->mkNode( AND, flem_c ) );
+ flem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), flem );
+ flem = Rewriter::rewrite( flem );
+ Trace("cegqi-lemma") << "Cegqi::Lemma : full specification " << flem << std::endl;
+ d_qe->getOutputChannel().lemma( flem );
}
}else{
Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
}
void CegConjectureSingleInv::initializeNextSiConjecture() {
+ Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture..." << std::endl;
+ if( d_single_inv.isNull() ){
+ if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){
+ Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl;
+ Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl;
+ }else{
+ Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl;
+ Notice() << "Incomplete due to --cegqi-si-partial." << std::endl;
+ exit( 10 );
+ }
+ }else{
+ //initial call
+ Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl;
+ Assert( d_single_inv_exp.isNull() );
+ }
+
+ d_si_guard = Node::null();
d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) );
d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard );
AlwaysAssert( !d_ns_guard.isNull() );
Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem );
}
- //add guard if not fully single invocation
- if( !isFullySingleInvocation() ){
- lem = NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), lem );
- }
Trace("cegqi-engine-debug") << "Rewrite..." << std::endl;
lem = Rewriter::rewrite( lem );
Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
}
}else if( !isFullySingleInvocation() ){
//create next candidate conjecture
- Trace("cegqi-nsi") << "NSI : create next candidate conjecture..." << std::endl;
- exit( 10 );
+ Assert( d_ei!=NULL );
+ //construct d_single_inv
+ d_single_inv = Node::null();
+ initializeNextSiConjecture();
+ return;
}
d_curr_lemmas.clear();
//call check for instantiator
d_cinst->check();
//add lemmas
- lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+ //add guard if not fully single invocation
+ if( !isFullySingleInvocation() ){
+ Assert( !d_ns_guard.isNull() );
+ for( unsigned i=0; i<d_curr_lemmas.size(); i++ ){
+ lems.push_back( NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), d_curr_lemmas[i] ) );
+ }
+ }else{
+ lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+ }
}
}
class CegConjecture;
class CegConjectureSingleInv;
+class CegEntailmentInfer;
class CegqiOutputSingleInv : public CegqiOutput
{
QuantifiersEngine * d_qe;
CegConjecture * d_parent;
CegConjectureSingleInvSol * d_sol;
+ CegEntailmentInfer * d_ei;
//the instantiator
+ CegqiOutputSingleInv * d_cosi;
CegInstantiator * d_cinst;
//for recognizing templates for invariant synthesis
Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
// partially single invocation
Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited );
Node addDeepEmbedding( Node n, std::map< Node, Node >& visited );
- //initialize next candidate si conjecture
- void initializeNextSiConjecture();
//presolve
void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
Node d_quant;
// single invocation portion of quantified formula
Node d_single_inv;
+ Node d_si_guard;
// non-single invocation portion of quantified formula
Node d_nsingle_inv;
+ Node d_ns_guard;
// full version quantified formula
Node d_full_inv;
- // current guard
- Node d_ns_guard;
+ Node d_full_guard;
+ //explanation for current single invocation conjecture
+ Node d_single_inv_exp;
// transition relation version per program
std::map< Node, Node > d_trans_pre;
std::map< Node, Node > d_trans_post;
std::map< Node, Node > d_prog_to_eval_op;
public:
//get the single invocation lemma(s)
- void getInitialSingleInvLemma( Node guard, std::vector< Node >& lems );
+ void getInitialSingleInvLemma( std::vector< Node >& lems );
//initialize
void initialize( Node q );
//check
// is single invocation
bool isSingleInvocation() { return !d_single_inv.isNull(); }
// is single invocation
- bool isFullySingleInvocation() { return d_nsingle_inv.isNull(); }
+ bool isFullySingleInvocation() { return !d_single_inv.isNull() && d_nsingle_inv.isNull(); }
//needs check
bool needsCheck();
/** preregister conjecture */
void preregisterConjecture( Node q );
+ //initialize next candidate si conjecture (if not fully single invocation)
+ void initializeNextSiConjecture();
};
// partitions any formulas given to it into single invocation/non-single invocation
--- /dev/null
+/********************* */
+/*! \file ce_guided_single_inv_ei.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for inferring entailments for cegqi
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_single_inv_ei.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quant_util.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegEntailmentInfer::CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ) : d_qe( qe ), d_sip( sip ) {
+
+}
+
+bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) {
+ if( Trace.isOn("cegqi-ei") ){
+ Trace("cegqi-ei") << "Infer new conjecture from : " << std::endl;
+ d_sip->debugPrint( "cegqi-ei" );
+ Trace("cegqi-ei") << "Current assertions : " << std::endl;
+ d_qe->getTheoryEngine()->printAssertions("cegqi-ei");
+ }
+
+
+ return false;
+}
+
+}
\ No newline at end of file
--- /dev/null
+/********************* */
+/*! \file ce_guided_single_inv_ei.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for inferring entailments for cegqi
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H
+
+
+#include "theory/quantifiers/ce_guided_single_inv.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegEntailmentInfer {
+private:
+ QuantifiersEngine * d_qe;
+ SingleInvocationPartition * d_sip;
+public:
+ CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip );
+ virtual ~CegEntailmentInfer(){}
+
+ bool getEntailedConjecture( Node& conj, Node& exp );
+};
+
+
+}
+}
+}
+
+#endif
projects / cvc5.git / commitdiff