* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
theory/quantifiers/ceg_t_instantiator.h \
theory/quantifiers/conjecture_generator.cpp \
theory/quantifiers/conjecture_generator.h \
+ theory/quantifiers/equality_query.cpp \
+ theory/quantifiers/equality_query.h \
theory/quantifiers/equality_infer.cpp \
theory/quantifiers/equality_infer.h \
theory/quantifiers/first_order_model.cpp \
theory/quantifiers/term_database.h \
theory/quantifiers/term_database_sygus.cpp \
theory/quantifiers/term_database_sygus.h \
+ theory/quantifiers/term_util.cpp \
+ theory/quantifiers/term_util.h \
theory/quantifiers/theory_quantifiers.cpp \
theory/quantifiers/theory_quantifiers.h \
theory/quantifiers/theory_quantifiers_type_rules.h \
#include "base/output.h"
#include "expr/attribute.h"
-#include "theory/quantifiers/term_database.h"
-
-
using namespace std;
namespace CVC4 {
for(iterator i = begin(); i != end() && !hasBv; ++i) {
hasBv = (*i).hasBoundVar();
}
- if( !hasBv ){
- //FIXME : this is a hack to handle synthesis conjectures
- // the issue is that we represent second-order quantification in synthesis conjectures via a Node:
- // exists x forall y P[f,y], where x is a dummy variable that maps to f through attribute SygusSynthFunVarListAttributeId
- // when asked whether a node has a bound variable, we want to treat f as if it were a bound (second-order) variable. -AJR
- if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
- hasBv = true;
- }
- }
}
setAttribute(HasBoundVarAttr(), hasBv);
setAttribute(HasBoundVarComputedAttr(), true);
}else{
synth_fun_type = range;
}
- // allow overloading for synth fun
- synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true);
+ // we do not allow overloading for synth fun
+ synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
// we add a declare function command here
// this is the single unmuted command in the sequence generated by this smt2 command
seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
}
const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
+ //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute
Expr sym = mkBoundVar("sfproxy", t);
d_sygusFunSymbols.push_back(sym);
#include "smt_util/boolean_simplification.h"
#include "smt_util/node_visitor.h"
#include "theory/arrays/theory_arrays_rewriter.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/substitutions.h"
#include "theory/theory_model.h"
#include "util/smt2_quote_string.h"
#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/macros.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/sort_inference.h"
#include "theory/strings/theory_strings.h"
#include "theory/substitutions.h"
quantifiers::SingleInvocationPartition sip;
std::vector< Node > funcs;
for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){
+ // TODO : revisit this when addressing #1205
Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute());
Assert( !sf.isNull() );
funcs.push_back( sf );
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/datatypes_sygus.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/theory_model.h"
if( depth==1 ){
if( nk!=UNDEFINED_KIND ){
// commutative operators
- if( quantifiers::TermDb::isComm( nk ) ){
+ if( quantifiers::TermUtil::isComm( nk ) ){
if( children.size()==2 ){
if( children[0].getType()==children[1].getType() ){
#if 0
std::vector< unsigned > deq_child[2];
if( children.size()==2 && children[0].getType()==tn ){
bool argDeq = false;
- if( quantifiers::TermDb::isNonAdditive( nk ) ){
+ if( quantifiers::TermUtil::isNonAdditive( nk ) ){
argDeq = true;
}else{
//other cases of rewriting x k x -> x'
}else if( depth==2 ){
if( nk!=UNDEFINED_KIND ){
// commutative operators
- if( quantifiers::TermDb::isComm( nk ) ){
+ if( quantifiers::TermUtil::isComm( nk ) ){
if( children.size()==2 ){
if( children[0].getType()==children[1].getType() ){
//chainable
**/
#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
using namespace CVC4;
using namespace std;
using namespace CVC4::kind;
struct sortTypeOrder {
- TermDb* d_tdb;
+ TermUtil* d_tu;
bool operator() (TypeNode i, TypeNode j) {
- return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+ return d_tu->getIdForType( i )<d_tu->getIdForType( j );
}
};
Assert( q.getKind()==FORALL );
Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
//construct canonical quantified formula
- Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true );
+ Node t = d_qe->getTermUtil()->getCanonicalTerm( q[1], true );
Trace("aeq") << " canonical form: " << t << std::endl;
//compute variable type counts
std::map< TypeNode, int > typ_count;
}
}
sortTypeOrder sto;
- sto.d_tdb = d_qe->getTermDatabase();
+ sto.d_tu = d_qe->getTermUtil();
std::sort( typs.begin(), typs.end(), sto );
Trace("aeq-debug") << " ";
Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
using namespace std;
namespace quantifiers {
struct sortTypeOrder {
- TermDb* d_tdb;
+ TermUtil* d_tu;
bool operator() (TypeNode i, TypeNode j) {
- return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+ return d_tu->getIdForType( i )<d_tu->getIdForType( j );
}
};
indices[d_ask_types[q][j]].push_back( j );
}
sortTypeOrder sto;
- sto.d_tdb = d_quantEngine->getTermDatabase();
+ sto.d_tu = d_quantEngine->getTermUtil();
std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto );
//increment j on inner loop
for( unsigned j=0; j<d_ask_types[q].size(); ){
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
using namespace CVC4;
//if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn }
Node conj = n;
if( !pol ){
- conj = TermDb::simpleNegate( conj );
+ conj = TermUtil::simpleNegate( conj );
}
Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
Assert( conj.getKind()==AND );
for( unsigned i=0; i<f[0].getNumChildren(); i++) {
if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
TypeNode tn = f[0][i].getType();
- if( tn.isSort() || getTermDatabase()->mayComplete( tn ) ){
+ if( tn.isSort() || getTermUtil()->mayComplete( tn ) ){
success = true;
setBoundedVar( f, f[0][i], BOUND_FINITE );
break;
Node tu = u;
getBounds( q, v, rsi, tl, tu );
Assert( !tl.isNull() && !tu.isNull() );
- if( ra==d_quantEngine->getTermDatabase()->d_true ){
+ if( ra==d_quantEngine->getTermUtil()->d_true ){
long rr = range.getConst<Rational>().getNumerator().getLong()+1;
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
for( unsigned k=0; k<rr; k++ ){
#include <algorithm>
#include <stack>
-#include "theory/quantifiers/term_database.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/bv/theory_bv_utils.h"
+
using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::theory;
#include "theory/quantifiers/candidate_generator.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
using namespace CVC4::theory::inst;
bool CandidateGenerator::isLegalCandidate( Node n ){
- return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) );
+ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
}
void CandidateGeneratorQueue::addCandidate( Node n ) {
CandidateGenerator( qe ), d_match_pattern( mpat ){
Assert( mpat.getKind()==EQUAL );
for( unsigned i=0; i<2; i++ ){
- if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){
d_match_gterm = mpat[i];
}
}
CandidateGenerator( qe ), d_match_pattern( mpat ){
d_match_pattern_type = mpat.getType();
Assert( mpat.getKind()==INST_CONSTANT );
- d_f = quantifiers::TermDb::getInstConstAttr( mpat );
+ d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
d_index = mpat.getAttribute(InstVarNumAttribute());
d_firstTime = false;
}
#include "prop/prop_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
using namespace CVC4::kind;
std::map< Node, Node > templates;
std::map< Node, Node > templates_arg;
//register with single invocation if applicable
- if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+ if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
d_ceg_si->initialize( d_quant );
q = d_ceg_si->getSimplifiedConjecture();
// carry the templates
Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl;
// we now finalize the single invocation module, based on the syntax restrictions
- if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+ if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() );
}
}
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
- if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+ if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
collectDisjuncts( d_base_inst, d_base_disj );
Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
//store the inner variables for each disjunct
}
}
d_syntax_guided = true;
- }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_quant ) ){
+ }else if( d_qe->getQuantAttributes()->isSynthesis( d_quant ) ){
d_syntax_guided = false;
}else{
Assert( false );
Node dr = Rewriter::rewrite( d[i] );
if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
if( constructed_cand ){
- ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+ ic.push_back( d_qe->getTermUtil()->getSkolemizedBody( dr[0] ).negate() );
}
if( sk_refine ){
Assert( !isGround() );
Node ce_q = d_ce_sk[0][k];
if( !ce_q.isNull() ){
Assert( !d_inner_vars_disj[k].empty() );
- Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() );
+ Assert( d_inner_vars_disj[k].size()==d_qe->getTermUtil()->d_skolem_constants[ce_q].size() );
std::vector< Node > model_values;
- getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values );
+ getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values );
sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
}else{
if( !options::sygusTemplEmbedGrammar() ){
TNode templa = d_ceg_si->getTemplateArg( sf );
// make the builtin version of the full solution
- TermDbSygus* sygusDb = d_qe->getTermDatabase()->getTermDatabaseSygus();
+ TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
Trace("cegqi-inv") << "Builtin version of solution is : "
<< sol << ", type : " << sol.getType()
#include "options/quantifiers_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
//FIXME : remove this include (github issue #1156)
#include "theory/bv/theory_bv_rewriter.h"
lem_conj.push_back( lem );
}
EvalSygusInvarianceTest vsit;
- vsit.d_result = d_quantEngine->getTermDatabase()->d_false;
+ vsit.d_result = d_quantEngine->getTermUtil()->d_false;
for( unsigned j=0; j<lem_conj.size(); j++ ){
Node lemc = lem_conj[j];
Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl;
Node lemcsu = d_quantEngine->getTermDatabaseSygus()->evaluateWithUnfolding( lemcs, vsit.d_visited );
Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl;
- if( lemcsu==d_quantEngine->getTermDatabase()->d_false ){
+ if( lemcsu==d_quantEngine->getTermUtil()->d_false ){
std::vector< Node > msu;
std::vector< Node > mexp;
msu.insert( msu.end(), ms.begin(), ms.end() );
void CegInstantiation::preregisterAssertion( Node n ) {
//check if it sygus conjecture
- if( TermDb::isSygusConjecture( n ) ){
+ if( QuantAttributes::checkSygusConjecture( n ) ){
//this is a sygus conjecture
Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
d_conj->preregisterConjecture( n );
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/datatypes/datatypes_rewriter.h"
using namespace CVC4;
const Datatype& cdt = ((DatatypeType)ctn.toType()).getDatatype();
for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
Kind ck = d_tds->getConsNumKind( ctn, j );
- if( ck!=UNDEFINED_KIND && TermDb::isBoolConnective( ck ) ){
+ if( ck!=UNDEFINED_KIND && TermUtil::isBoolConnective( ck ) ){
bool typeCorrect = true;
for( unsigned k=0; k<cdt[j].getNumArgs(); k++ ){
if( d_tds->getArgType( cdt[j], k )!=ctn ){
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
}else{
inst = d_single_inv;
}
- inst = TermDb::simpleNegate( inst );
+ inst = TermUtil::simpleNegate( inst );
Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
//register with the instantiator
if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){
qq = q[1][0][1];
}else{
- qq = TermDb::simpleNegate( q[1] );
+ qq = TermUtil::simpleNegate( q[1] );
}
//process the single invocation-ness of the property
if( !d_sip->init( progs, qq ) ){
// we now have determined whether we will do single invocation techniques
if( d_single_invocation ){
d_single_inv = d_sip->getSingleInvocation();
- d_single_inv = TermDb::simpleNegate( d_single_inv );
+ d_single_inv = TermUtil::simpleNegate( d_single_inv );
if( !d_sip->d_func_vars.empty() ){
Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars );
d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
Trace("cegqi-engine") << siss.str() << std::endl;
Assert( d_single_inv_var.size()==subs.size() );
lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
- if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){
+ if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){
Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
- lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem );
+ lem = d_qe->getTermUtil()->rewriteVtsSymbols( lem );
}
}
}
if( itw!=weak_imp.end() ){
cond = itw->second;
}
- cond = TermDb::simpleNegate( cond );
+ cond = TermUtil::simpleNegate( cond );
Node ite1 = d_inst[uindex][i];
Node ite2 = constructSolution( indices, i, index+1, weak_imp );
return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
Node s;
if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
- s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
+ s = d_qe->getTermUtil()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
}else{
Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
sol_index = d_prog_to_sol_index[prog];
std::vector< Node > si_subs;
Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
//do DER on conjunct
- Node cr = TermDb::getQuantSimplify( conj[i] );
+ Node cr = TermUtil::getQuantSimplify( conj[i] );
if( cr!=conj[i] ){
Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
}
Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl;
//now must check if it has other bound variables
std::vector< Node > bvs;
- TermDb::getBoundVars( cr, bvs );
+ TermUtil::getBoundVars( cr, bvs );
if( bvs.size()>d_si_vars.size() ){
- Trace("si-prt") << "...not ground single invocation." << std::endl;
- ngroundSingleInvocation = true;
- singleInvocation = false;
+ // getBoundVars also collects functions in the rare case that we are synthesizing a function with 0 arguments
+ // take these into account below.
+ unsigned n_const_synth_fun = 0;
+ for( unsigned j=0; j<bvs.size(); j++ ){
+ if( std::find( d_input_funcs.begin(), d_input_funcs.end(), bvs[j] )!=d_input_funcs.end() ){
+ n_const_synth_fun++;
+ }
+ }
+ if( bvs.size()-n_const_synth_fun>d_si_vars.size() ){
+ Trace("si-prt") << "...not ground single invocation." << std::endl;
+ ngroundSingleInvocation = true;
+ singleInvocation = false;
+ }else{
+ Trace("si-prt") << "...ground single invocation : success, after removing 0-arg synth functions." << std::endl;
+ }
}else{
Trace("si-prt") << "...ground single invocation : success." << std::endl;
}
singleInvocation = false;
//rename bound variables with maximal overlap with si_vars
std::vector< Node > bvs;
- TermDb::getBoundVars( cr, bvs );
+ TermUtil::getBoundVars( cr, bvs );
std::vector< Node > terms;
std::vector< Node > subs;
for( unsigned j=0; j<bvs.size(); j++ ){
cr = Rewriter::rewrite( cr );
Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl;
d_conjuncts[2].push_back( cr );
- TermDb::getBoundVars( cr, d_all_vars );
+ TermUtil::getBoundVars( cr, d_all_vars );
if( singleInvocation ){
//replace with single invocation formulation
Assert( si_terms.size()==si_subs.size() );
return false;
}else{
if( !pol ){
- n = TermDb::simpleNegate( n );
+ n = TermUtil::simpleNegate( n );
}
Trace("si-prt") << "Conjunct : " << n << std::endl;
conj.push_back( n );
return true;
}else{
bool ret = true;
- //if( TermDb::hasBoundVarAttr( n ) ){
+ //if( TermUtil::hasBoundVarAttr( n ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !processConjunct( n[i], visited, args, terms, subs ) ){
ret = false;
Node s;
for( unsigned r=0; r<2; r++ ){
if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){
- if( !TermDb::containsTerm( slit[1-r], slit[r] ) ){
+ if( !TermUtil::containsTerm( slit[1-r], slit[r] ) ){
v = slit[r];
s = slit[1-r];
break;
Node veq_c;
Node val;
int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
- if( ires!=0 && veq_c.isNull() && !TermDb::containsTerm( val, itm->first ) ){
+ if( ires!=0 && veq_c.isNull() && !TermUtil::containsTerm( val, itm->first ) ){
v = itm->first;
s = val;
}
}
if( i==0 || i==1 ){
// pre-condition and transition are negated
- ret = TermDb::simpleNegate( ret );
+ ret = TermUtil::simpleNegate( ret );
}
d_com[i].d_this = ret;
}
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
rem = pullITEs( rem );
Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
Node prev = s;
- s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
+ s = NodeManager::currentNM()->mkNode( ITE, TermUtil::simpleNegate( cond ), t, rem );
Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
success = true;
Node cond = n_ite[0][i];
orig_conj.push_back( cond );
if( n_ite[0].getKind()==OR ){
- cond = TermDb::simpleNegate( cond );
+ cond = TermUtil::simpleNegate( cond );
}
curr_conj.push_back( cond );
}
Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl;
return pol==ita->second;
}else if( n.isConst() ){
- return pol==(n==d_qe->getTermDatabase()->d_true);
+ return pol==(n==d_qe->getTermUtil()->d_true);
}else{
Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl;
assign[n] = pol;
Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
Node eqro = eq[r==0 ? 1 : 0 ];
- if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){
+ if( !d_qe->getTermUtil()->containsTerm( eqro, eq[r] ) ){
Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
new_vars.push_back( eq[r] );
new_subs.push_back( eqro );
std::vector< Node > children;
std::vector< Node > new_vars;
std::vector< Node > new_subs;
- Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false;
+ Node bc = sol.getKind()==OR ? d_qe->getTermUtil()->d_true : d_qe->getTermUtil()->d_false;
for( unsigned i=0; i<sol.getNumChildren(); i++ ){
bool do_exc = false;
Node c;
if( j!=i && ( j>i || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){
Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() );
sj = Rewriter::rewrite( sj );
- if( sj==( sol.getKind()==AND ? d_qe->getTermDatabase()->d_false : d_qe->getTermDatabase()->d_true ) ){
+ if( sj==( sol.getKind()==AND ? d_qe->getTermUtil()->d_false : d_qe->getTermUtil()->d_true ) ){
Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl;
red = true;
break;
std::vector< TypeNode > to_erase;
for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){
TypeNode stn = it->first;
- Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index );
+ Node ns = d_qe->getTermUtil()->getEnumerateTerm( stn, index );
if( ns.isNull() ){
to_erase.push_back( stn );
}else{
if( karg!=-1 ){
//collect the children of min_t
std::vector< Node > tchildren;
- if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
+ if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
tchildren.push_back( min_t[0] );
std::vector< Node > rem_children;
for( unsigned i=1; i<min_t.getNumChildren(); i++ ){
new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
}else if( curr.getKind()==OR || curr.getKind()==AND ){
- new_t = TermDb::simpleNegate( curr ).negate();
+ new_t = TermUtil::simpleNegate( curr ).negate();
}else if( curr.getKind()==NOT ){
- new_t = TermDb::simpleNegate( curr[0] );
+ new_t = TermUtil::simpleNegate( curr[0] );
}else{
new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
}
}
if( !eq.isNull() ){
eq = Rewriter::rewrite( eq );
- if( eq!=d_qe->getTermDatabase()->d_true ){
+ if( eq!=d_qe->getTermUtil()->d_true ){
success = false;
break;
}
#include "smt/term_formula_removal.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
nretc = Rewriter::rewrite( nretc );
//ensure that nret does not contain vars
- if( !TermDb::containsTerms( nretc, vars ) ){
+ if( !TermUtil::containsTerms( nretc, vars ) ){
//result is ( nret / pv_prop.d_coeff )
nret = nretc;
}else{
}else{
atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
atom_lhs = Rewriter::rewrite( atom_lhs );
- atom_rhs = getQuantifiersEngine()->getTermDatabase()->d_zero;
+ atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero;
}
//must be an eligible term
if( isEligible( atom_lhs ) ){
d_is_nested_quant = true;
}else if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( TermDb::isBoolConnectiveTerm( n ) ){
+ if( TermUtil::isBoolConnectiveTerm( n ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
collectCeAtoms( n[i], visited );
}
Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
- d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn );
+ d_closed_enum_type = qe->getTermUtil()->isClosedEnumerableType( tn );
}
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/trigger.h"
}
if( !delta_coeff.isNull() ){
//create delta here if necessary
- val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) );
+ val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) );
val = Rewriter::rewrite( val );
}
return val;
}
if( options::cbqiAll() ){
// when not pure LIA/LRA, we must check whether the lhs contains pv
- if( TermDb::containsTerm( val, pv ) ){
+ if( TermUtil::containsTerm( val, pv ) ){
Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
return 0;
}
if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
//redo, split integer/non-integer parts
bool useCoeff = false;
- Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst<Rational>().getNumerator();
+ Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst<Rational>().getNumerator();
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if( it->first.isNull() || it->first.getType().isInteger() ){
if( !it->second.isNull() ){
if( !vts_coeff[0].isNull() ){
vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
}
- realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
+ realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
//re-isolate
Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
}
void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
- d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false );
- d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false );
+ d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false );
+ d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false );
for( unsigned i=0; i<2; i++ ){
d_mbp_bounds[i].clear();
d_mbp_coeff[i].clear();
Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
cmp = Rewriter::rewrite( cmp );
Assert( cmp.isConst() );
- is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->d_true );
+ is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true );
}
}else{
is_upper = (r==0);
vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
}
}else{
- Node delta = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta();
+ Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta();
uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
uval = Rewriter::rewrite( uval );
}
}
int best_used[2];
std::vector< Node > t_values[3];
- Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero;
- Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one;
+ Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero;
+ Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one;
Node pv_value = ci->getModelValue( pv );
//try optimal bounds
for( unsigned r=0; r<2; r++ ){
if( use_inf ){
Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl;
//no bounds, we do +- infinity
- Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type );
+ Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type );
//TODO : rho value for infinity?
if( rr==0 ){
val = NodeManager::currentNM()->mkNode( UMINUS, val );
Kind k = rr==0 ? GEQ : LEQ;
Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] );
cmp_bound = Rewriter::rewrite( cmp_bound );
- if( cmp_bound!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ){
+ if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){
new_best = false;
break;
}
NodeManager::currentNM()->mkNode( ITE,
NodeManager::currentNM()->mkNode( EQUAL,
NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ),
- ci->getQuantifiersEngine()->getTermDatabase()->d_zero ),
- ci->getQuantifiersEngine()->getTermDatabase()->d_zero, ci->getQuantifiersEngine()->getTermDatabase()->d_one )
+ ci->getQuantifiersEngine()->getTermUtil()->d_zero ),
+ ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one )
);
}
}
}
if( !ret.isNull() ){
//ensure does not contain
- if( TermDb::containsTerm( ret, v ) ){
+ if( TermUtil::containsTerm( ret, v ) ){
ret = Node::null();
}
}
}
void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) {
- if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){
+ if( inst::Trigger::isAtomicTrigger( catom ) && TermUtil::containsTerm( catom, pv ) ){
Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl;
std::vector< Node > arg_reps;
for( unsigned j=0; j<catom.getNumChildren(); j++ ){
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
}
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
- return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i );
+ return d_quantEngine->getTermUtil()->getCanonicalFreeVar( tn, i );
}
bool ConjectureGenerator::isHandledTerm( TNode n ){
Trace("sg-proc-debug") << "...eqc : " << r << std::endl;
eqcs.push_back( r );
if( r.getType().isBoolean() ){
- if( areEqual( r, getTermDatabase()->d_true ) ){
- d_ground_eqc_map[r] = getTermDatabase()->d_true;
+ if( areEqual( r, getTermUtil()->d_true ) ){
+ d_ground_eqc_map[r] = getTermUtil()->d_true;
d_bool_eqc[0] = r;
- }else if( areEqual( r, getTermDatabase()->d_false ) ){
- d_ground_eqc_map[r] = getTermDatabase()->d_false;
+ }else if( areEqual( r, getTermUtil()->d_false ) ){
+ d_ground_eqc_map[r] = getTermUtil()->d_false;
d_bool_eqc[1] = r;
}
}
std::vector< TNode > args;
Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
Node n;
- if( getTermDatabase()->isInductionTerm( r ) ){
+ if( getTermUtil()->isInductionTerm( r ) ){
n = d_op_arg_index[r].getGroundTerm( this, args );
}else{
n = r;
TNode r = eqcs[i];
//print out members
bool firstTime = true;
- bool isFalse = areEqual( r, getTermDatabase()->d_false );
+ bool isFalse = areEqual( r, getTermUtil()->d_false );
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
if( d_tge.isRelevantTerm( eq ) ){
//make it canonical
Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
- eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq );
+ eq = d_quantEngine->getTermUtil()->getCanonicalTerm( eq );
}else{
eq = Node::null();
}
//check each skolem variable
bool disproven = true;
//std::vector< Node > sk;
- //getTermDatabase()->getSkolemConstants( q, sk, true );
+ //getTermUtil()->getSkolemConstants( q, sk, true );
Trace("sg-conjecture") << " CONJECTURE : ";
std::vector< Node > ce;
- for( unsigned j=0; j<getTermDatabase()->d_skolem_constants[q].size(); j++ ){
- TNode k = getTermDatabase()->d_skolem_constants[q][j];
+ for( unsigned j=0; j<getTermUtil()->d_skolem_constants[q].size(); j++ ){
+ TNode k = getTermUtil()->d_skolem_constants[q][j];
TNode rk = getRepresentative( k );
std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
//check if it is a ground term
Trace("sg-conjecture") << "ACTIVE : " << q;
if( Trace.isOn("sg-gen-eqc") ){
Trace("sg-conjecture") << " { ";
- for( unsigned k=0; k<getTermDatabase()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
+ for( unsigned k=0; k<getTermUtil()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
Trace("sg-conjecture") << "}";
}
Trace("sg-conjecture") << std::endl;
typ_to_subs_index[it->first] = sum;
sum += it->second;
for( unsigned i=0; i<it->second; i++ ){
- gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) );
+ gsubs_vars.push_back( d_quantEngine->getTermUtil()->getCanonicalFreeVar( it->first, i ) );
}
}
}
for( unsigned i=0; i<n.getNumChildren(); i++ ){
vec.push_back( 0 );
TypeNode tn = n[i].getType();
- if( getTermDatabase()->isClosedEnumerableType( tn ) ){
+ if( getTermUtil()->isClosedEnumerableType( tn ) ){
types.push_back( tn );
}else{
return;
vec.push_back( size_limit );
}else{
//see if we can iterate current
- if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){
+ if( vec_sum<size_limit && !getTermUtil()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){
vec[index]++;
vec_sum++;
vec.push_back( size_limit - vec_sum );
}
if( success ){
if( vec.size()==n.getNumChildren() ){
- Node lc = getTermDatabase()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] );
+ Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] );
if( !lc.isNull() ){
for( unsigned i=0; i<vec.size(); i++ ){
Trace("sg-gt-enum-debug") << vec[i] << " ";
std::vector< Node > children;
children.push_back( n.getOperator() );
for( unsigned i=0; i<(vec.size()-1); i++ ){
- Node nn = getTermDatabase()->getEnumerateTerm( types[i], vec[i] );
+ Node nn = getTermUtil()->getEnumerateTerm( types[i], vec[i] );
Assert( !nn.isNull() );
Assert( nn.getType()==n[i].getType() );
children.push_back( nn );
--- /dev/null
+/********************* */
+/*! \file equality_query.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities used for querying about equality information
+ **/
+
+#include "theory/quantifiers/equality_query.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
+
+}
+
+EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
+}
+
+bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
+ d_int_rep.clear();
+ d_reset_count++;
+ return processInferences( e );
+}
+
+bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
+ if( options::inferArithTriggerEq() ){
+ eq::EqualityEngine* ee = getEngine();
+ //updated implementation
+ EqualityInference * ei = d_qe->getEqualityInference();
+ while( d_eqi_counter.get()<ei->getNumPendingMerges() ){
+ Node eq = ei->getPendingMerge( d_eqi_counter.get() );
+ Node eq_exp = ei->getPendingMergeExplanation( d_eqi_counter.get() );
+ Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
+ Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl;
+ Assert( ee->hasTerm( eq[0] ) );
+ Assert( ee->hasTerm( eq[1] ) );
+ if( areDisequal( eq[0], eq[1] ) ){
+ Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
+ if( Trace.isOn("term-db-lemma") ){
+ Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
+ if( !d_qe->getTheoryEngine()->needCheck() ){
+ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
+ //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
+ Assert( false );
+ }
+ Trace("term-db-lemma") << " add split on : " << eq << std::endl;
+ }
+ d_qe->addSplit( eq );
+ return false;
+ }else{
+ ee->assertEquality( eq, true, eq_exp );
+ d_eqi_counter = d_eqi_counter.get() + 1;
+ }
+ }
+ Assert( ee->consistent() );
+ }
+ return true;
+}
+
+bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
+ return getEngine()->hasTerm( a );
+}
+
+Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) ){
+ return ee->getRepresentative( a );
+ }else{
+ return a;
+ }
+}
+
+bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
+ if( a==b ){
+ return true;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ return ee->areEqual( a, b );
+ }else{
+ return false;
+ }
+ }
+}
+
+bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
+ if( a==b ){
+ return false;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ return ee->areDisequal( a, b, false );
+ }else{
+ return a.isConst() && b.isConst();
+ }
+ }
+}
+
+Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
+ Assert( f.isNull() || f.getKind()==FORALL );
+ Node r = getRepresentative( a );
+ if( options::finiteModelFind() ){
+ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
+ //map back from values assigned by model, if any
+ if( d_qe->getModel() ){
+ std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
+ if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
+ r = it->second;
+ r = getRepresentative( r );
+ }else{
+ if( r.getType().isSort() ){
+ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+ //should never happen : UF constants should never escape model
+ Assert( false );
+ }
+ }
+ }
+ }
+ }
+ if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
+ return r;
+ }else{
+ TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
+ std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
+ if( itir==d_int_rep[v_tn].end() ){
+ //find best selection for representative
+ Node r_best;
+ //if( options::fmfRelevantDomain() && !f.isNull() ){
+ // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
+ // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
+ // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
+ //}
+ std::vector< Node > eqc;
+ getEquivalenceClass( r, eqc );
+ Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
+ for( unsigned i=0; i<eqc.size(); i++ ){
+ if( i>0 ) Trace("internal-rep-select") << ", ";
+ Trace("internal-rep-select") << eqc[i];
+ }
+ Trace("internal-rep-select") << " }, type = " << v_tn << std::endl;
+ int r_best_score = -1;
+ for( size_t i=0; i<eqc.size(); i++ ){
+ int score = getRepScore( eqc[i], f, index, v_tn );
+ if( score!=-2 ){
+ if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
+ r_best = eqc[i];
+ r_best_score = score;
+ }
+ }
+ }
+ if( r_best.isNull() ){
+ Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
+ r_best = r;
+ }
+ //now, make sure that no other member of the class is an instance
+ std::unordered_map<TNode, Node, TNodeHashFunction> cache;
+ r_best = getInstance( r_best, eqc, cache );
+ //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 << " with score " << r_best_score << std::endl;
+ Assert( r_best.getType().isSubtypeOf( v_tn ) );
+ d_int_rep[v_tn][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;
+ }
+ return r_best;
+ }else{
+ return itir->second;
+ }
+ }
+}
+
+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< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+ Trace("internal-rep-flatten") << itt->first << " : 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< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.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( itt->second.find( r )==itt->second.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;
+ itt->second[it->first] = ni[j];
+ changed = false;
+ success = true;
+ break;
+ }else{
+ Node ir = itt->second[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;
+ itt->second[it->first] = n;
+ temp_rep_map[n] = it->first;
+ }
+ }
+ }
+ }
+ }while( success );
+ Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+ for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+ Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+ }
+ }
+}
+
+eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
+ return d_qe->getActiveEqualityEngine();
+}
+
+void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) ){
+ Node rep = ee->getRepresentative( a );
+ eq::EqClassIterator eqc_iter( rep, ee );
+ while( !eqc_iter.isFinished() ){
+ eqc.push_back( *eqc_iter );
+ eqc_iter++;
+ }
+ }else{
+ eqc.push_back( a );
+ }
+ //a should be in its equivalence class
+ Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+}
+
+TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ return d_qe->getTermDatabase()->getCongruentTerm( f, args );
+}
+
+//helper functions
+
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
+ if(cache.find(n) != cache.end()) {
+ return cache[n];
+ }
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ Node nn = getInstance( n[i], eqc, cache );
+ if( !nn.isNull() ){
+ return cache[n] = nn;
+ }
+ }
+ if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
+ return cache[n] = n;
+ }else{
+ return cache[n] = Node::null();
+ }
+}
+
+//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
+int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+ if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject
+ return -2;
+ }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
+ return -2;
+ }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
+ return -1;
+ }else if( options::instMaxLevel()!=-1 ){
+ //score prefer lowest instantiation level
+ if( n.hasAttribute(InstLevelAttribute()) ){
+ return n.getAttribute(InstLevelAttribute());
+ }else{
+ return options::instLevelInputOnly() ? -1 : 0;
+ }
+ }else{
+ if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
+ //score prefers earliest use of this term as a representative
+ return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+ }else{
+ Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
+ return quantifiers::TermUtil::getTermDepth( n );
+ }
+ }
+}
--- /dev/null
+/********************* */
+/*! \file equality_query.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Equality query class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+// TODO : (as part of #1171, #1214) further document and clean this class.
+/** equality query object using theory engine */
+class EqualityQueryQuantifiersEngine : public EqualityQuery
+{
+private:
+ /** pointer to theory engine */
+ QuantifiersEngine* d_qe;
+ /** quantifiers equality inference */
+ context::CDO< unsigned > d_eqi_counter;
+ /** internal representatives */
+ std::map< TypeNode, std::map< Node, Node > > d_int_rep;
+ /** rep score */
+ std::map< Node, int > d_rep_score;
+ /** reset count */
+ int d_reset_count;
+
+ /** processInferences : will merge equivalence classes in master equality engine, if possible */
+ bool processInferences( Theory::Effort e );
+ /** node contains */
+ Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
+ /** get score */
+ int getRepScore( Node n, Node f, int index, TypeNode v_tn );
+ /** flatten representatives */
+ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
+public:
+ EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
+ virtual ~EqualityQueryQuantifiersEngine();
+ /** reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "EqualityQueryQE"; }
+ /** general queries about equality */
+ bool hasTerm( Node a );
+ Node getRepresentative( Node a );
+ bool areEqual( Node a, Node b );
+ bool areDisequal( Node a, Node b );
+ eq::EqualityEngine* getEngine();
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );
+ /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
+ If cbqi is active, this will return a term in the equivalence class of "a" that does
+ not contain instantiation constants, if such a term exists.
+ */
+ Node getInternalRepresentative( Node a, Node f, int index );
+}; /* EqualityQueryQuantifiersEngine */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#define USE_INDEX_ORDERING
int computeMaxVariableNum( Node n ){
if( n.getKind()==INST_CONSTANT ){
return n.getAttribute(InstVarNumAttribute());
- }else if( TermDb::hasInstConstAttr(n) ){
+ }else if( TermUtil::hasInstConstAttr(n) ){
int maxVal = -1;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
int val = getMaxVariableNum( n[i] );
}else{
//can happen for types not involved in quantified formulas
Trace("fmc-model-func") << "No type rep for " << tn << std::endl;
- v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
+ v = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
}
Trace("fmc-model-func") << "No term, assign " << v << std::endl;
}
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
using namespace std;
using namespace CVC4;
Node r = fm->getRepresentative( it->second[a] );
if( Trace.isOn("fmc-model-debug") ){
std::vector< Node > eqc;
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc );
Trace("fmc-model-debug") << " " << (it->second[a]==r);
Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
//Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
#include <vector>
#include "theory/quantifiers/fun_def_process.h"
-#include "theory/rewriter.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_util.h"
#include "proof/proof_manager.h"
using namespace CVC4;
std::map< int, Node > subs_head;
//first pass : find defined functions, transform quantifiers
for( unsigned i=0; i<assertions.size(); i++ ){
- Node n = TermDb::getFunDefHead( assertions[i] );
+ Node n = QuantAttributes::getFunDefHead( assertions[i] );
if( !n.isNull() ){
Assert( n.getKind()==APPLY_UF );
Node f = n.getOperator();
exit( 0 );
}
- Node bd = TermDb::getFunDefBody( assertions[i] );
+ Node bd = QuantAttributes::getFunDefBody( assertions[i] );
Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
if( !bd.isNull() ){
d_funcs.push_back( f );
#include "options/datatypes_options.h"
#include "theory/quantifiers/candidate_generator.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers_engine.h"
d_cg = NULL;
d_needsReset = true;
d_active_add = false;
- Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
+ Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
d_pattern = pat;
d_match_pattern = pat;
d_match_pattern_type = pat.getType();
//make sure the matching portion of the equality is on the LHS of d_pattern
// and record what d_match_pattern is
for( unsigned i=0; i<2; i++ ){
- if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
Node mp = d_match_pattern[1-i];
Node mpo = d_match_pattern[i];
if( mp.getKind()!=INST_CONSTANT ){
//now, collect children of d_match_pattern
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
- Node qa = quantifiers::TermDb::getInstConstAttr(d_match_pattern[i]);
+ Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
if( !qa.isNull() ){
InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, d_match_pattern[i] );
if( cimg ){
std::vector< int > prev;
//if t is null
Assert( !t.isNull() );
- Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
+ Assert( !quantifiers::TermUtil::hasInstConstAttr(t) );
Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() );
Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
//first, check if ground arguments are not equal, or a match is in conflict
Node t_match;
if( pol ){
if( pat.getKind()==GT ){
- t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermDatabase()->d_one);
+ t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one);
}else{
t_match = t;
}
}else{
if( pat.getKind()==EQUAL ){
if( t.getType().isBoolean() ){
- t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
+ t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
}else{
Assert( t.getType().isReal() );
- t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
}
}else if( pat.getKind()==GEQ ){
- t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
}else if( pat.getKind()==GT ){
t_match = t;
}
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
//order patterns to maximize eager matching failures
std::map< Node, std::vector< Node > > var_contains;
- qe->getTermDatabase()->getVarContains( q, pats, var_contains );
+ qe->getTermUtil()->getVarContains( q, pats, var_contains );
std::map< Node, std::vector< Node > > var_to_node;
for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
for( unsigned i=0; i<it->second.size(); i++ ){
d_f( q ){
Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl;
std::map< Node, std::vector< Node > > var_contains;
- qe->getTermDatabase()->getVarContains( q, pats, var_contains );
+ qe->getTermUtil()->getVarContains( q, pats, var_contains );
//convert to indicies
for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: ";
processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
}else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+ //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
Node n = m.get( curr_index );
if( n.isNull() ){
//if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
}
if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+ //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
//unique non-set variable, add to InstMatch
for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
InstMatch mn( &m );
if( d_match_pattern.getKind()==EQUAL ){
d_eqc = d_match_pattern[1];
d_match_pattern = d_match_pattern[0];
- Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) );
+ Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) );
}
Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==q ){
+ if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
}else{
d_var_num[i] = -1;
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory_engine.h"
Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
//add cbqi lemma
//get the counterexample literal
- Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
- Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+ Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+ Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q );
if( !ceBody.isNull() ){
//add counterexample lemma
Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
if( itc!=qepr->d_consts.end() ){
Assert( !itc->second.empty() );
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
+ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
std::vector< Node > disj;
for( unsigned j=0; j<itc->second.size(); j++ ){
disj.push_back( ic.eqNode( itc->second[j] ) );
//compute dependencies between quantified formulas
if( options::cbqiLitDepend() || options::cbqiInnermost() ){
std::vector< Node > ics;
- TermDb::computeVarContains( q, ics );
+ TermUtil::computeVarContains( q, ics );
d_parent_quant[q].clear();
d_children_quant[q].clear();
std::vector< Node > dep;
d_parent_quant[q].push_back( qi );
d_children_quant[qi].push_back( q );
Assert( hasAddedCbqiLemma( qi ) );
- Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
+ Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi );
dep.push_back( qi );
dep.push_back( qicel );
}
//must register all sub-quantifiers of counterexample lemma, register their lemmas
std::vector< Node > quants;
- TermDb::computeQuantContains( lem, quants );
+ TermUtil::computeQuantContains( lem, quants );
for( unsigned i=0; i<quants.size(); i++ ){
if( doCbqi( quants[i] ) ){
registerCbqiLemma( quants[i] );
if( options::cbqiNestedQE() ){
//record these as counterexample quantifiers
QAttributes qa;
- TermDb::computeQuantAttributes( quants[i], qa );
+ QuantAttributes::computeQuantAttributes( quants[i], qa );
if( !qa.d_qid_num.isNull() ){
d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
d_active_quant[q] = true;
Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
- Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+ Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
bool value;
if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
Node ret = n;
if( n.getKind()==FORALL ){
QAttributes qa;
- TermDb::computeQuantAttributes( n, qa );
+ QuantAttributes::computeQuantAttributes( n, qa );
if( qa.d_qid_num.isNull() ){
std::vector< Node > rc;
rc.push_back( n[0] );
//should not contain quantifiers
Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
}
- Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() );
+ Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() );
//replace inst constants with instantiation
- Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(),
- d_quantEngine->getTermDatabase()->d_inst_constants[q].end(),
+ Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
+ d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
inst_terms.begin(), inst_terms.end() );
if( doVts ){
//do virtual term substitution
ret = Rewriter::rewrite( ret );
- ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret );
+ ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret );
}
Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
Trace("cbqi-nqe") << " " << n << std::endl;
Node ret = n;
if( n.getKind()==FORALL ){
QAttributes qa;
- TermDb::computeQuantAttributes( n, qa );
+ QuantAttributes::computeQuantAttributes( n, qa );
if( !qa.d_qid_num.isNull() ){
//if it has an id, check whether we have done quantifier elimination for this id
std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
+ if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){
if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl;
return true;
std::map< Node, int >::iterator it = d_do_cbqi.find( q );
if( it==d_do_cbqi.end() ){
int ret = 2;
- if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
- Assert( !d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) );
+ if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){
+ Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) );
//if has an instantiation pattern, don't do it
if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
}
}
}
- if( d_quantEngine->getTermDatabase()->isQAttrSygus( q ) ){
+ if( d_quantEngine->getQuantAttributes()->isSygus( q ) ){
ret = 0;
}
if( ret!=0 ){
}
//then check self
if( hasAddedCbqiLemma( q ) ){
- Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+ Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
bool value;
if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
d_small_const = Rewriter::rewrite( d_small_const );
//heuristic for now, until we know how to do nested quantification
- Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
+ Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false );
if( !delta.isNull() ){
Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
}
std::vector< Node > inf;
- d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
+ d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false );
for( unsigned i=0; i<inf.size(); i++ ){
Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
Assert( !d_curr_quant.isNull() );
//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
- if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
+ if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
return true;
}else{
//check if we need virtual term substitution (if used delta or infinity)
- bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
+ bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
++(d_quantEngine->d_statistics.d_instantiations_cbqi);
//d_added_inst.insert( d_curr_quant );
}
}
//only legal if current quantified formula contains n
- return TermDb::containsTerm( d_curr_quant, n );
+ return TermUtil::containsTerm( d_curr_quant, n );
}
}else{
return true;
//must register with the instantiator
//must explicitly remove ITEs so that we record dependencies
std::vector< Node > ce_vars;
- for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
- ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
+ for( unsigned i=0; i<d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ); i++ ){
+ ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) );
}
std::vector< Node > lems;
lems.push_back( lem );
#include "theory/quantifiers/inst_strategy_e_matching.h"
#include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
using namespace std;
std::map< Node, inst::TriggerTermInfo > tinfo;
//well-defined function: can assume LHS is only trigger
if( options::quantFunWellDefined() ){
- Node hd = TermDb::getFunDefHead( f );
+ Node hd = QuantAttributes::getFunDefHead( f );
if( !hd.isNull() ){
- hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
+ hd = d_quantEngine->getTermUtil()->getInstConstantNode( hd, f );
patTermsF.push_back( hd );
tinfo[hd].init( f, hd );
}
}
//otherwise, use algorithm for collecting pattern terms
if( patTermsF.empty() ){
- Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+ Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true );
if( ntrivTriggers ){
sortTriggers st;
if( options::partialTriggers() ){
std::vector< Node > vcs[2];
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] );
}
for( unsigned i=0; i<2; i++ ){
if( tr ){
if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
//partial trigger : generate implication to mark user pattern
- Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermDatabase()->getVariableNode( tr->getInstPattern(), q ) );
+ Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermUtil()->getVariableNode( tr->getInstPattern(), q ) );
Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
Trace("auto-gen-trigger-partial") << " " << qq << std::endl;
std::map< Node, bool >::iterator itq = d_quant.find( f );
if( itq==d_quant.end() ){
//generate triggers
- Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+ Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
std::vector< Node > vars;
std::vector< Node > patTerms;
bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
d_quant[f] = ret;
//add all variables to trigger that don't already occur
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- Node x = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
patTerms.push_back( x );
}
std::map< Node, Node > reps_found;
for( unsigned j=0; j<ts; j++ ){
Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], j );
- if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr( gt ) ){
+ if( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr( gt ) ){
Node r = d_quantEngine->getEqualityQuery()->getRepresentative( gt );
if( reps_found.find( r )==reps_found.end() ){
reps_found[r] = gt;
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/inst_strategy_e_matching.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
//}
//take into account user patterns
if( f.getNumChildren()==3 ){
- Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
+ Node subsPat = d_quantEngine->getTermUtil()->getInstConstantNode( f[2], f );
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
#include "theory/quantifiers/local_theory_ext.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/first_order_model.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/rewriter.h"
}
bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
- Node icn = d_qe->getTermDatabase()->getInstConstantNode( n, f );
+ Node icn = d_qe->getTermUtil()->getInstConstantNode( n, f );
Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
std::vector< Node > var;
- d_qe->getTermDatabase()->getVarContainsNode( f, icn, var );
+ d_qe->getTermUtil()->getVarContainsNode( f, icn, var );
Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
std::vector< Node > trigger_var;
inst::Trigger::getTriggerVariables( icn, f, trigger_var );
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
//if evaluate(...)==1, then the instantiation is already true in the model
// depIndex is the index of the least significant variable that this evaluation relies upon
depIndex = riter.getNumTerms()-1;
- Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl;
- eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+ Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermUtil()->getInstConstantBody( f ) << std::endl;
+ eval = fmig->evaluate( d_qe->getTermUtil()->getInstConstantBody( f ), depIndex, &riter );
if( eval==1 ){
Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
}else{
// - determine selection literals
// - check which function/predicates have good and bad definitions for satisfying f
if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
- d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true );
+ d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true );
}
int selectLitScore = -1;
for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
// constant definitions.
bool isConst = true;
std::vector< Node > uf_terms;
- if( TermDb::hasInstConstAttr(n) ){
+ if( TermUtil::hasInstConstAttr(n) ){
isConst = false;
if( gn.getKind()==APPLY_UF ){
uf_terms.push_back( gn );
}else if( gn.getKind()==EQUAL ){
isConst = true;
for( int j=0; j<2; j++ ){
- if( TermDb::hasInstConstAttr(n[j]) ){
+ if( TermUtil::hasInstConstAttr(n[j]) ){
if( n[j].getKind()==APPLY_UF &&
fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
uf_terms.push_back( gn[j] );
for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
- Assert( TermDb::hasInstConstAttr(lit) );
+ Assert( TermUtil::hasInstConstAttr(lit) );
std::vector< Node > tr_terms;
if( lit.getKind()==APPLY_UF ){
//only match predicates that are contrary to this one, use literal matching
}else if( lit.getKind()==EQUAL ){
//collect trigger terms
for( int j=0; j<2; j++ ){
- if( TermDb::hasInstConstAttr(lit[j]) ){
+ if( TermUtil::hasInstConstAttr(lit[j]) ){
if( lit[j].getKind()==APPLY_UF ){
tr_terms.push_back( lit[j] );
}else{
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
if( Trace.isOn("fmf-exh-inst-debug") ){
Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+ Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " ";
}
Trace("fmf-exh-inst-debug") << std::endl;
}
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief quant conflict find class
+ ** \brief Implements conflict-based instantiation (Reynolds et al FMCAD 2014)
**
**/
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/theory_engine.h"
}
Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
}
- if( inst_eval.isNull() || inst_eval==p->getTermDatabase()->d_true || !isPropagatingInstance( p, inst_eval ) ){
+ if( inst_eval.isNull() || inst_eval==p->getTermUtil()->d_true || !isPropagatingInstance( p, inst_eval ) ){
Trace("qcf-instance-check") << "...spurious." << std::endl;
return true;
}else{
//check constraints
for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
//apply substitution to the tconstraint
- Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms );
+ Node cons = p->getTermUtil()->getInstantiatedNode( it->first, d_q, terms );
cons = it->second ? cons : cons.negate();
if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
return true;
}
bool MatchGen::isHandledBoolConnective( TNode n ) {
- return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
+ return TermUtil::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
}
bool MatchGen::isHandledUfTerm( TNode n ) {
Node r = (*eqcs_i);
if( getTermDatabase()->hasTermCurrent( r ) ){
TypeNode rtn = r.getType();
- if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+ if( !options::cbqi() || !TermUtil::hasInstConstAttr( r ) ){
d_eqcs[rtn].push_back( r );
}
}
#include "theory/quantifiers/quant_equality_engine.h"
#include "theory/rewriter.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
using namespace CVC4;
using namespace std;
Node t1;
Node t2;
if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
- lit = getTermDatabase()->getCanonicalTerm( lit );
+ lit = getTermUtil()->getCanonicalTerm( lit );
Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl;
if( lit.getKind()==APPLY_UF ){
t1 = getFunctionAppForPredicateApp( lit );
- t2 = pol ? getTermDatabase()->d_one : getTermDatabase()->d_zero;
+ t2 = pol ? getTermUtil()->d_one : getTermUtil()->d_zero;
pol = true;
lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
}else if( lit.getKind()==EQUAL ){
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
using namespace std;
return d_quantEngine->getTermDatabase();
}
+quantifiers::TermUtil * QuantifiersModule::getTermUtil() {
+ return d_quantEngine->getTermUtil();
+}
+
bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
c = n[0];
}
}
if( tn.isReal() ){
- if( quantifiers::TermDb::containsTerm( lit, v ) ){
+ if( quantifiers::TermUtil::containsTerm( lit, v ) ){
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( lit, msum ) ){
Node val, veqc;
for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;
if( it->first.getKind()==EQUAL ){
- if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){
- if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
+ if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
d_phase_reqs_equality[ it->first[0] ] = it->second;
Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
}
- }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
+ }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
d_phase_reqs_equality[ it->first[1] ] = it->second;
Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
namespace quantifiers {
class TermDb;
+ class TermUtil;
}
class QuantifiersModule {
bool areEqual( TNode n1, TNode n2 );
TNode getRepresentative( TNode n );
quantifiers::TermDb * getTermDatabase();
+ quantifiers::TermUtil * getTermUtil();
};/* class QuantifiersModule */
class QuantifiersUtil {
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers_engine.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/term_util.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
+QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) :
+d_quantEngine(qe) {
+
+}
+
+void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
if( attr=="axiom" ){
Trace("quant-attr-debug") << "Set axiom " << n << std::endl;
n.setAttribute( qepa, true );
}
}
+
+bool QuantAttributes::checkRewriteRule( Node q ) {
+ return !getRewriteRule( q ).isNull();
+}
+
+Node QuantAttributes::getRewriteRule( Node q ) {
+ if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
+ return q[2][0][0];
+ }else{
+ return Node::null();
+ }
+}
+
+bool QuantAttributes::checkFunDef( Node q ) {
+ return !getFunDefHead( q ).isNull();
+}
+
+bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
+ if( !ipl.isNull() ){
+ for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+ if( ipl[i].getKind()==INST_ATTRIBUTE ){
+ if( ipl[i][0].getAttribute(FunDefAttribute()) ){
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+Node QuantAttributes::getFunDefHead( Node q ) {
+ //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
+ if( q.getKind()==FORALL && q.getNumChildren()==3 ){
+
+ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ if( q[2][i].getKind()==INST_ATTRIBUTE ){
+ if( q[2][i][0].getAttribute(FunDefAttribute()) ){
+ return q[2][i][0];
+ }
+ }
+ }
+ }
+ return Node::null();
+}
+Node QuantAttributes::getFunDefBody( Node q ) {
+ Node h = getFunDefHead( q );
+ if( !h.isNull() ){
+ if( q[1].getKind()==EQUAL ){
+ if( q[1][0]==h ){
+ return q[1][1];
+ }else if( q[1][1]==h ){
+ return q[1][0];
+ }
+ }else{
+ Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
+ bool pol = q[1].getKind()!=NOT;
+ if( atom==h ){
+ return NodeManager::currentNM()->mkConst( pol );
+ }
+ }
+ }
+ return Node::null();
+}
+
+bool QuantAttributes::checkSygusConjecture( Node q ) {
+ return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false;
+}
+
+bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
+ if( !ipl.isNull() ){
+ for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+ if( ipl[i].getKind()==INST_ATTRIBUTE ){
+ Node avar = ipl[i][0];
+ if( avar.getAttribute(SygusAttribute()) ){
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
+ if( !ipl.isNull() ){
+ for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+ if( ipl[i].getKind()==INST_ATTRIBUTE ){
+ Node avar = ipl[i][0];
+ if( avar.getAttribute(QuantElimAttribute()) ){
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+void QuantAttributes::computeAttributes( Node q ) {
+ computeQuantAttributes( q, d_qattr[q] );
+ if( !d_qattr[q].d_rr.isNull() ){
+ 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(), 2 );
+ }
+ if( d_qattr[q].isFunDef() ){
+ Node f = d_qattr[q].d_fundef_f;
+ if( d_fun_defs.find( f )!=d_fun_defs.end() ){
+ Message() << "Cannot define function " << f << " more than once." << std::endl;
+ exit( 1 );
+ }
+ d_fun_defs[f] = true;
+ d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
+ }
+ if( d_qattr[q].d_sygus ){
+ 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(), 2 );
+ }
+ if( d_qattr[q].d_synthesis ){
+ 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(), 2 );
+ }
+}
+
+void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
+ Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
+ if( q.getNumChildren()==3 ){
+ qa.d_ipl = q[2];
+ 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_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
+ qa.d_hasPattern = true;
+ }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
+ Node avar = q[2][i][0];
+ if( avar.getAttribute(AxiomAttribute()) ){
+ Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
+ qa.d_axiom = true;
+ }
+ if( avar.getAttribute(ConjectureAttribute()) ){
+ Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
+ qa.d_conjecture = true;
+ }
+ if( avar.getAttribute(FunDefAttribute()) ){
+ Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
+ //get operator directly from pattern
+ qa.d_fundef_f = q[2][i][0].getOperator();
+ }
+ if( avar.getAttribute(SygusAttribute()) ){
+ //not necessarily nested existential
+ //Assert( q[1].getKind()==NOT );
+ //Assert( q[1][0].getKind()==FORALL );
+ Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
+ qa.d_sygus = true;
+ }
+ if( avar.getAttribute(SynthesisAttribute()) ){
+ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
+ qa.d_synthesis = true;
+ }
+ if( avar.hasAttribute(QuantInstLevelAttribute()) ){
+ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
+ Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
+ }
+ if( avar.hasAttribute(RrPriorityAttribute()) ){
+ qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
+ Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
+ }
+ if( avar.getAttribute(QuantElimAttribute()) ){
+ Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
+ qa.d_quant_elim = true;
+ //don't set owner, should happen naturally
+ }
+ if( avar.getAttribute(QuantElimPartialAttribute()) ){
+ Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
+ qa.d_quant_elim = true;
+ qa.d_quant_elim_partial = true;
+ //don't set owner, should happen naturally
+ }
+ if( avar.hasAttribute(QuantIdNumAttribute()) ){
+ qa.d_qid_num = avar;
+ Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
+ }
+ if( avar.getKind()==REWRITE_RULE ){
+ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
+ Assert( i==0 );
+ qa.d_rr = avar;
+ }
+ }
+ }
+ }
+}
+
+bool QuantAttributes::isConjecture( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_conjecture;
+ }
+}
+
+bool QuantAttributes::isAxiom( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_axiom;
+ }
+}
+
+bool QuantAttributes::isFunDef( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.isFunDef();
+ }
+}
+
+bool QuantAttributes::isSygus( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_sygus;
+ }
+}
+
+bool QuantAttributes::isSynthesis( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_synthesis;
+ }
+}
+
+int QuantAttributes::getQuantInstLevel( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return -1;
+ }else{
+ return it->second.d_qinstLevel;
+ }
+}
+
+int QuantAttributes::getRewriteRulePriority( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return -1;
+ }else{
+ return it->second.d_rr_priority;
+ }
+}
+
+bool QuantAttributes::isQuantElim( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_quant_elim;
+ }
+}
+
+bool QuantAttributes::isQuantElimPartial( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return false;
+ }else{
+ return it->second.d_quant_elim_partial;
+ }
+}
+
+int QuantAttributes::getQuantIdNum( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it!=d_qattr.end() ){
+ if( !it->second.d_qid_num.isNull() ){
+ return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
+ }
+ }
+ return -1;
+}
+
+Node QuantAttributes::getQuantIdNumNode( Node q ) {
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
+ return Node::null();
+ }else{
+ return it->second.d_qid_num;
+ }
+}
+
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
-#include "theory/rewriter.h"
-#include "theory/quantifiers_engine.h"
+#include "expr/attribute.h"
+#include "expr/node.h"
namespace CVC4 {
namespace theory {
+
+class QuantifiersEngine;
+
+/** Attribute true for quantifiers that are axioms */
+struct AxiomAttributeId {};
+typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
+
+/** Attribute true for quantifiers that are conjecture */
+struct ConjectureAttributeId {};
+typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
+
+/** Attribute true for function definition quantifiers */
+struct FunDefAttributeId {};
+typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
+
+/** Attribute true for quantifiers that we are doing quantifier elimination on */
+struct QuantElimAttributeId {};
+typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
+
+/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
+struct QuantElimPartialAttributeId {};
+typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
+
+/** Attribute true for quantifiers that are SyGus conjectures */
+struct SygusAttributeId {};
+typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
+
+/** Attribute true for quantifiers that are synthesis conjectures */
+struct SynthesisAttributeId {};
+typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+
namespace quantifiers {
/** Attribute priority for rewrite rules */
//struct RrPriorityAttributeId {};
//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
-struct QuantifiersAttributes
+
+/** This class stores attributes for quantified formulas
+* TODO : document (as part of #1171, #1215)
+*/
+class QAttributes{
+public:
+ QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
+ d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
+ ~QAttributes(){}
+ bool d_hasPattern;
+ Node d_rr;
+ bool d_conjecture;
+ bool d_axiom;
+ Node d_fundef_f;
+ bool d_sygus;
+ bool d_synthesis;
+ int d_rr_priority;
+ int d_qinstLevel;
+ bool d_quant_elim;
+ bool d_quant_elim_partial;
+ Node d_ipl;
+ Node d_qid_num;
+ bool isRewriteRule() { return !d_rr.isNull(); }
+ bool isFunDef() { return !d_fundef_f.isNull(); }
+};
+
+/** This class caches information about attributes of quantified formulas
+* It also has static utility functions used for determining attributes and information about
+* quantified formulas.
+*/
+class QuantAttributes
{
+public:
+ QuantAttributes( QuantifiersEngine * qe );
+ ~QuantAttributes(){}
+
/** set user attribute
* This function will apply a custom set of attributes to all top-level universal
* quantifiers contained in n
*/
static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
-};
+
+ //general queries concerning quantified formulas wrt modules
+ /** is quantifier treated as a rewrite rule? */
+ static bool checkRewriteRule( Node q );
+ /** get the rewrite rule associated with the quanfied formula */
+ static Node getRewriteRule( Node q );
+ /** is fun def */
+ static bool checkFunDef( Node q );
+ /** is fun def */
+ static bool checkFunDefAnnotation( Node ipl );
+ /** is sygus conjecture */
+ static bool checkSygusConjecture( Node q );
+ /** is sygus conjecture */
+ static bool checkSygusConjectureAnnotation( Node ipl );
+ /** get fun def body */
+ static Node getFunDefHead( Node q );
+ /** get fun def body */
+ static Node getFunDefBody( Node q );
+ /** is quant elim annotation */
+ static bool checkQuantElimAnnotation( Node ipl );
+ /** is conjecture */
+ bool isConjecture( Node q );
+ /** is axiom */
+ bool isAxiom( Node q );
+ /** is function definition */
+ bool isFunDef( Node q );
+ /** is sygus conjecture */
+ bool isSygus( Node q );
+ /** is synthesis conjecture */
+ bool isSynthesis( Node q );
+ /** get instantiation level */
+ int getQuantInstLevel( Node q );
+ /** get rewrite rule priority */
+ int getRewriteRulePriority( Node q );
+ /** is quant elim */
+ bool isQuantElim( Node q );
+ /** is quant elim partial */
+ bool isQuantElimPartial( Node q );
+ /** get quant id num */
+ int getQuantIdNum( Node q );
+ /** get quant id num */
+ Node getQuantIdNumNode( Node q );
+ /** compute quantifier attributes */
+ static void computeQuantAttributes( Node q, QAttributes& qa );
+ /** compute the attributes for q */
+ void computeAttributes( Node q );
+private:
+ /** pointer to quantifiers engine */
+ QuantifiersEngine * d_quantEngine;
+ /** cache of attributes */
+ std::map< Node, QAttributes > d_qattr;
+ /** function definitions */
+ std::map< Node, bool > d_fun_defs;
+};
}
}
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
using namespace std;
}else{
//compute attributes
QAttributes qa;
- TermDb::computeQuantAttributes( in, qa );
+ QuantAttributes::computeQuantAttributes( in, qa );
if( !qa.isRewriteRule() ){
for( int op=0; op<COMPUTE_LAST; op++ ){
if( doOperation( in, op, qa ) ){
std::map< Node, Node > cache;
std::map< Node, Node > icache;
if( qa.isFunDef() ){
- Node h = TermDb::getFunDefHead( q );
+ Node h = QuantAttributes::getFunDefHead( q );
Assert( !h.isNull() );
// if it is a function definition, rewrite the body independently
- Node fbody = TermDb::getFunDefBody( q );
+ Node fbody = QuantAttributes::getFunDefBody( q );
Assert( !body.isNull() );
Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false );
}else if( n.getKind()==EQUAL ){
for( unsigned i=0; i<2; i++ ){
if( n[i].getKind()==BOUND_VARIABLE ){
- if( !TermDb::containsTerm( n[1-i], n[i] ) ){
+ if( !TermUtil::containsTerm( n[1-i], n[i] ) ){
return true;
}
}
}
bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
- if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
+ if( TermUtil::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
return false;
}else{
return true;
if( lit.getKind()==GEQ || lit.getKind()==GT ){
//compute variables in itm->first, these are not eligible for elimination
std::vector< Node > bvs;
- TermDb::getBoundVars( itm->first, bvs );
+ TermUtil::getBoundVars( itm->first, bvs );
for( unsigned j=0; j<bvs.size(); j++ ){
Trace("var-elim-ineq-debug") << "...ineligible " << bvs[j] << " since it is contained in monomial." << std::endl;
num_bounds[bvs[j]][true].clear();
NodeBuilder<> tb(kind::OR);
for( unsigned i=0; i<body.getNumChildren(); i++ ){
Node trm = body[i];
- if( TermDb::containsTerms( body[i], args ) ){
+ if( TermUtil::containsTerms( body[i], args ) ){
tb << trm;
}else{
body_split << trm;
Node sub;
std::vector< unsigned > sub_vars;
//return skolemized body
- return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
+ return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
}
}else{
//check if it contains a quantifier as a subterm
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/first_order_model.h"
using namespace std;
std::map< Node, Node > rterms;
for( unsigned i=0; i<d_terms.size(); i++ ){
Node r = d_terms[i];
- if( !TermDb::hasInstConstAttr( d_terms[i] ) ){
+ if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
r = qe->getEqualityQuery()->getRepresentative( d_terms[i] );
}
if( rterms.find( r )==rterms.end() ){
FirstOrderModel* fm = d_qe->getModel();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
- Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
+ Node icf = d_qe->getTermUtil()->getInstConstantBody( q );
Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
computeRelevantDomain( q, icf, true, true );
}
}
}
- if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
+ if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
//compute the information for what this literal does
computeRelevantDomainLit( q, hasPol, pol, n );
if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
if( n.getKind()==INST_CONSTANT ){
- Node q = d_qe->getTermDatabase()->getInstConstAttr( n );
+ Node q = d_qe->getTermUtil()->getInstConstAttr( n );
//merge the RDomains
unsigned id = n.getAttribute(InstVarNumAttribute());
Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
- Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
+ Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl;
RDomain * rq = getRDomain( q, id );
if( rf!=rq ){
rq->merge( rf );
}
- }else if( !TermDb::hasInstConstAttr( n ) ){
+ }else if( !TermUtil::hasInstConstAttr( n ) ){
Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
//term to add
rf->addTerm( n );
if( hasPol && !pol ){
d_rel_dom_lit[hasPol][pol][n].d_merge = false;
}
- }else if( !r_add.isNull() && !TermDb::hasInstConstAttr( r_add ) ){
+ }else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){
Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
//the negative occurrence adds the term to the domain
if( !hasPol || !pol ){
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/inst_match_generator.h"
#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
using namespace CVC4;
}
double RewriteEngine::getPriority( Node f ) {
- Node rr = TermDb::getRewriteRule( f );
+ Node rr = QuantAttributes::getRewriteRule( f );
Node rrr = rr[2];
Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
bool deterministic = rrr[1].getKind()!=OR;
if( it!=d_qinfo.end() ){
QuantInfo * qi = &it->second;
if( qi->matchGeneratorIsValid() ){
- Node rr = TermDb::getRewriteRule( f );
+ Node rr = QuantAttributes::getRewriteRule( f );
Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl;
qi->reset_round( qcf );
Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl;
}
void RewriteEngine::registerQuantifier( Node f ) {
- Node rr = TermDb::getRewriteRule( f );
+ Node rr = QuantAttributes::getRewriteRule( f );
if( !rr.isNull() ){
Trace("rr-register") << "Register quantifier " << f << std::endl;
Trace("rr-register") << " rewrite rule is : " << rr << std::endl;
body_c.push_back( d_rr[f][1][j].negate() );
}
}
- }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){
+ }else if( d_rr[f][1]!=d_quantEngine->getTermUtil()->d_true ){
if( MatchGen::isHandled( d_rr[f][1] ) ){
body_c.push_back( d_rr[f][1].negate() );
}
Node RewriteEngine::getInstConstNode( Node n, Node q ) {
std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
if( it==d_inst_const_node[q].end() ){
- Node nn = d_quantEngine->getTermDatabase()->getInstConstantNode( n, q );
+ Node nn = d_quantEngine->getTermUtil()->getInstConstantNode( n, q );
d_inst_const_node[q][n] = nn;
return nn;
}else{
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
using namespace CVC4::kind;
using namespace std;
Node op;
std::vector< Type > argTypes;
if( templ.getNumChildren()==0 ){
- // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg )
+ // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg )
op = templ;
}else{
Assert( templ.hasOperator() );
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
TermDb::TermDb(context::Context* c, context::UserContext* u,
QuantifiersEngine* qe)
: d_quantEngine(qe),
- d_inactive_map(c),
- d_op_id_count(0),
- d_typ_id_count(0),
- d_sygus_tdb(NULL) {
+ d_inactive_map(c) {
d_consistent_ee = true;
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- if (options::ceGuidedInst()) {
- d_sygus_tdb = new TermDbSygus(c, qe);
- }
}
+
TermDb::~TermDb(){
- if(d_sygus_tdb) {
- delete d_sygus_tdb;
+
+}
+
+void TermDb::registerQuantifier( Node q ) {
+ Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) );
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
+ setTermInactive( ic );
}
}
bool rec = false;
if( d_processed.find( n )==d_processed.end() ){
d_processed.insert(n);
- if( !TermDb::hasInstConstAttr(n) ){
+ if( !TermUtil::hasInstConstAttr(n) ){
Trace("term-db-debug") << "register term : " << n << std::endl;
d_type_map[ n.getType() ].push_back( n );
//if this is an atomic trigger, consider adding it
d_op_map[op].push_back( n );
added.insert( n );
- if( d_sygus_tdb ){
- d_sygus_tdb->registerEvalTerm( n );
+ if( d_quantEngine->getTermDatabaseSygus() ){
+ d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n );
}
}
}else{
}
if( options::instMaxLevel()!=-1 ){
if( n.hasAttribute(InstLevelAttribute()) ){
- int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f );
+ int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
unsigned ml = fml>=0 ? fml : options::instMaxLevel();
if( n.getAttribute(InstLevelAttribute())>ml ){
return d_func_map_trie[f].existsTerm( args );
}
+
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
if( tn.isInteger() || tn.isReal() ){
- mbt = d_zero;
- }else if( isClosedEnumerableType( tn ) ){
+ mbt = NodeManager::currentNM()->mkConst(Rational(0));
+ }else if( d_quantEngine->getTermUtil()->isClosedEnumerableType( tn ) ){
mbt = tn.mkGroundTerm();
}else{
if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) );
}
}
- Node gn = n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(),
+ Node gn = n.substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
+ d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() );
return gn;
}
Node TermDb::getModelBasisBody( Node q ){
if( d_model_basis_body.find( q )==d_model_basis_body.end() ){
- Node n = getInstConstantBody( q );
+ Node n = d_quantEngine->getTermUtil()->getInstConstantBody( q );
d_model_basis_body[q] = getModelBasis( q, n );
}
return d_model_basis_body[q];
}
}
-void TermDb::makeInstantiationConstantsFor( Node q ){
- if( d_inst_constants.find( q )==d_inst_constants.end() ){
- Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- d_vars[q].push_back( q[0][i] );
- d_var_num[q][q[0][i]] = i;
- //make instantiation constants
- Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
- d_inst_constants_map[ic] = q;
- d_inst_constants[ q ].push_back( ic );
- Debug("quantifiers-engine") << " " << ic << std::endl;
- //set the var number attribute
- InstVarNumAttribute ivna;
- ic.setAttribute( ivna, i );
- InstConstantAttribute ica;
- ic.setAttribute( ica, q );
- //also set the term inactive
- setTermInactive( ic );
- }
- }
-}
-
-void TermDb::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- if( n.getKind()==BOUND_VARIABLE ){
- if( std::find( vars.begin(), vars.end(), n )==vars.end() ) {
- vars.push_back( n );
- }
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- getBoundVars2( n[i], vars, visited );
- }
- }
-}
-
-Node TermDb::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
- std::map< Node, Node >::iterator it = visited.find( n );
- if( it!=visited.end() ){
- return it->second;
- }else{
- Node ret = n;
- if( n.getKind()==FORALL ){
- ret = getRemoveQuantifiers2( n[1], visited );
- }else if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- bool childrenChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node ni = getRemoveQuantifiers2( n[i], visited );
- childrenChanged = childrenChanged || ni!=n[i];
- children.push_back( ni );
- }
- if( childrenChanged ){
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), n.getOperator() );
- }
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- visited[n] = ret;
- return ret;
- }
-}
-
-Node TermDb::getInstConstAttr( Node n ) {
- if (!n.hasAttribute(InstConstantAttribute()) ){
- Node q;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- q = getInstConstAttr(n[i]);
- if( !q.isNull() ){
- break;
- }
- }
- InstConstantAttribute ica;
- n.setAttribute(ica, q);
- }
- return n.getAttribute(InstConstantAttribute());
-}
-
-bool TermDb::hasInstConstAttr( Node n ) {
- return !getInstConstAttr(n).isNull();
-}
-
-Node TermDb::getBoundVarAttr( Node n ) {
- if (!n.hasAttribute(BoundVarAttribute()) ){
- Node bv;
- if( n.getKind()==BOUND_VARIABLE ){
- bv = n;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bv = getBoundVarAttr(n[i]);
- if( !bv.isNull() ){
- break;
- }
- }
- }
- BoundVarAttribute bva;
- n.setAttribute(bva, bv);
- }
- return n.getAttribute(BoundVarAttribute());
-}
-
-bool TermDb::hasBoundVarAttr( Node n ) {
- return !getBoundVarAttr(n).isNull();
-}
-
-void TermDb::getBoundVars( Node n, std::vector< Node >& vars ) {
- std::map< Node, bool > visited;
- return getBoundVars2( n, vars, visited );
-}
-
-//remove quantifiers
-Node TermDb::getRemoveQuantifiers( Node n ) {
- std::map< Node, Node > visited;
- return getRemoveQuantifiers2( n, visited );
-}
-
-//quantified simplify
-Node TermDb::getQuantSimplify( Node n ) {
- std::vector< Node > bvs;
- getBoundVars( n, bvs );
- if( bvs.empty() ) {
- return Rewriter::rewrite( n );
- }else{
- Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n );
- q = Rewriter::rewrite( q );
- return getRemoveQuantifiers( q );
- }
-}
-
-/** get the i^th instantiation constant of q */
-Node TermDb::getInstantiationConstant( Node q, int i ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
- if( it!=d_inst_constants.end() ){
- return it->second[i];
- }else{
- return Node::null();
- }
-}
-
-/** get number of instantiation constants for q */
-unsigned TermDb::getNumInstantiationConstants( Node q ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
- if( it!=d_inst_constants.end() ){
- return it->second.size();
- }else{
- return 0;
- }
-}
-
-Node TermDb::getInstConstantBody( Node q ){
- std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
- if( it==d_inst_const_body.end() ){
- Node n = getInstConstantNode( q[1], q );
- d_inst_const_body[ q ] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node TermDb::getCounterexampleLiteral( Node q ){
- if( d_ce_lit.find( q )==d_ce_lit.end() ){
- /*
- Node ceBody = getInstConstantBody( f );
- //check if any variable are of bad types, and fail if so
- for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
- if( d_inst_constants[f][i].getType().isBoolean() ){
- d_ce_lit[ f ] = Node::null();
- return Node::null();
- }
- }
- */
- Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
- //otherwise, ensure literal
- Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
- d_ce_lit[ q ] = ceLit;
- }
- return d_ce_lit[ q ];
-}
-
-Node TermDb::getInstConstantNode( Node n, Node q ){
- makeInstantiationConstantsFor( q );
- return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
-}
-
-Node TermDb::getVariableNode( Node n, Node q ) {
- makeInstantiationConstantsFor( q );
- return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
-}
-
-Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
- Assert( d_vars[q].size()==terms.size() );
- return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
-}
-
-
-void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
- TypeNode tspec;
- if( dt.isParametric() ){
- tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
- Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
- Assert( tspec.getNumChildren()==dc.getNumArgs() );
- }
- Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
- for( unsigned j=0; j<dc.getNumArgs(); j++ ){
- std::vector< Node > ssc;
- if( dt.isParametric() ){
- Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
- if( tspec[j]==ntn ){
- ssc.push_back( n );
- }
- }else{
- TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
- Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
- if( tn==ntn ){
- ssc.push_back( n );
- }
- }
- /* TODO: more than weak structural induction
- else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
- visited.push_back( tn );
- const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
- std::vector< Node > disj;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- getSelfSel( dt[i], n, ntn, ssc );
- }
- visited.pop_back();
- }
- */
- for( unsigned k=0; k<ssc.size(); k++ ){
- Node ss = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n );
- if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){
- selfSel.push_back( ss );
- }
- }
- }
-}
-
-
-Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
- std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
- Assert( sk.empty() || sk.size()==f[0].getNumChildren() );
- //calculate the variables and substitution
- std::vector< TNode > ind_vars;
- std::vector< unsigned > ind_var_indicies;
- std::vector< TNode > vars;
- std::vector< unsigned > var_indicies;
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- if( isInductionTerm( f[0][i] ) ){
- ind_vars.push_back( f[0][i] );
- ind_var_indicies.push_back( i );
- }else{
- vars.push_back( f[0][i] );
- var_indicies.push_back( i );
- }
- Node s;
- //make the new function symbol or use existing
- if( i>=sk.size() ){
- if( argTypes.empty() ){
- s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
- }else{
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
- Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
- //DOTHIS: set attribute on op, marking that it should not be selected as trigger
- std::vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
- s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
- }
- sk.push_back( s );
- }else{
- Assert( sk[i].getType()==f[0][i].getType() );
- }
- }
- Node ret;
- if( vars.empty() ){
- ret = n;
- }else{
- std::vector< Node > var_sk;
- for( unsigned i=0; i<var_indicies.size(); i++ ){
- var_sk.push_back( sk[var_indicies[i]] );
- }
- Assert( vars.size()==var_sk.size() );
- ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
- }
- if( !ind_vars.empty() ){
- Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
- Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
- Node n_str_ind;
- TypeNode tn = ind_vars[0].getType();
- Node k = sk[ind_var_indicies[0]];
- Node nret = ret.substitute( ind_vars[0], k );
- //note : everything is under a negation
- //the following constructs ~( R( x, k ) => ~P( x ) )
- if( options::dtStcInduction() && tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- std::vector< Node > disj;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- std::vector< Node > selfSel;
- getSelfSel( dt, dt[i], k, tn, selfSel );
- std::vector< Node > conj;
- conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
- for( unsigned j=0; j<selfSel.size(); j++ ){
- conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() );
- }
- disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
- }
- Assert( !disj.empty() );
- n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
- }else if( options::intWfInduction() && tn.isInteger() ){
- Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) );
- Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate();
- n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret );
- n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind );
- }else{
- Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl;
- Assert( false );
- }
- Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
-
- std::vector< Node > rem_ind_vars;
- rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() );
- if( !rem_ind_vars.empty() ){
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars );
- nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret );
- nret = Rewriter::rewrite( nret );
- sub = nret;
- sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() );
- n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate();
- }
- ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
- }
- Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
- //if it has an instantiation level, set the skolemized body to that level
- if( f.hasAttribute(InstLevelAttribute()) ){
- theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
- }
-
- if( Trace.isOn("quantifiers-sk") ){
- Trace("quantifiers-sk") << "Skolemize : ";
- for( unsigned i=0; i<sk.size(); i++ ){
- Trace("quantifiers-sk") << sk[i] << " ";
- }
- Trace("quantifiers-sk") << "for " << std::endl;
- Trace("quantifiers-sk") << " " << f << std::endl;
- }
-
- return ret;
-}
-
-Node TermDb::getSkolemizedBody( Node f ){
- Assert( f.getKind()==FORALL );
- if( d_skolem_body.find( f )==d_skolem_body.end() ){
- std::vector< TypeNode > fvTypes;
- std::vector< TNode > fvs;
- Node sub;
- std::vector< unsigned > sub_vars;
- d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
- //store sub quantifier information
- if( !sub.isNull() ){
- //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them
- Assert( d_skolem_constants[sub].empty() );
- for( unsigned i=0; i<sub_vars.size(); i++ ){
- d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] );
- }
- }
- Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
- if( options::sortInference() ){
- for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
- //carry information for sort inference
- d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
- }
- }
- }
- return d_skolem_body[ f ];
-}
-
-Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
- Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
- 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];
-}
-
-bool TermDb::isClosedEnumerableType( TypeNode tn ) {
- std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
- if( it==d_typ_closed_enum.end() ){
- d_typ_closed_enum[tn] = true;
- bool ret = true;
- if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){
- ret = false;
- }else if( tn.isSet() ){
- ret = isClosedEnumerableType( tn.getSetElementType() );
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
- if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
- ret = false;
- break;
- }
- }
- if( !ret ){
- break;
- }
- }
- }
- //TODO: other parametric sorts go here
- d_typ_closed_enum[tn] = ret;
- return ret;
- }else{
- return it->second;
- }
-}
-
-//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
-bool TermDb::mayComplete( TypeNode tn ) {
- std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
- if( it==d_may_complete.end() ){
- bool mc = false;
- if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
- Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
- Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
- Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
- eq = Rewriter::rewrite( eq );
- mc = eq==d_true;
- }
- d_may_complete[tn] = mc;
- return mc;
- }else{
- return it->second;
- }
-}
-
-void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
- std::map< Node, bool > visited;
- computeVarContains2( n, INST_CONSTANT, varContains, visited );
-}
-
-void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) {
- std::map< Node, bool > visited;
- computeVarContains2( n, FORALL, quantContains, visited );
-}
-
-
-void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- if( n.getKind()==k ){
- if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){
- varContains.push_back( n );
- }
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- computeVarContains2( n[i], k, varContains, visited );
- }
- }
- }
-}
-
-void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
- for( unsigned i=0; i<pats.size(); i++ ){
- varContains[ pats[i] ].clear();
- getVarContainsNode( f, pats[i], varContains[ pats[i] ] );
- }
-}
-
-void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
- std::vector< Node > vars;
- computeVarContains( n, vars );
- for( unsigned j=0; j<vars.size(); j++ ){
- Node v = vars[j];
- if( v.getAttribute(InstConstantAttribute())==f ){
- if( std::find( varContains.begin(), varContains.end(), v )==varContains.end() ){
- varContains.push_back( v );
- }
- }
- }
-}
-
-int TermDb::isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ){
- if( n1==n2 ){
- return 1;
- }else if( n1.getKind()==n2.getKind() ){
- if( n1.getKind()==APPLY_UF ){
- if( n1.getOperator()==n2.getOperator() ){
- int result = 0;
- for( int i=0; i<(int)n1.getNumChildren(); i++ ){
- if( n1[i]!=n2[i] ){
- int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 );
- if( cResult==0 ){
- return 0;
- }else if( cResult!=result ){
- if( result!=0 ){
- return 0;
- }else{
- result = cResult;
- }
- }
- }
- }
- return result;
- }
- }
- return 0;
- }else if( n2.getKind()==INST_CONSTANT ){
- //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
- // return 1;
- //}
- if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){
- return 1;
- }
- }else if( n1.getKind()==INST_CONSTANT ){
- //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
- // return -1;
- //}
- if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){
- return 1;
- }
- }
- return 0;
-}
-
-int TermDb::isInstanceOf( Node n1, Node n2 ){
- std::vector< Node > varContains1;
- std::vector< Node > varContains2;
- computeVarContains( n1, varContains1 );
- computeVarContains( n1, varContains2 );
- return isInstanceOf2( n1, n2, varContains1, varContains2 );
-}
-
-bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
- if( n1==n2 ){
- return true;
- }else if( n2.getKind()==INST_CONSTANT ){
- //if( !node_contains( n1, n2 ) ){
- // return false;
- //}
- if( subs.find( n2 )==subs.end() ){
- subs[n2] = n1;
- }else if( subs[n2]!=n1 ){
- return false;
- }
- return true;
- }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
- if( n1.getOperator()!=n2.getOperator() ){
- return false;
- }
- for( int i=0; i<(int)n1.getNumChildren(); i++ ){
- if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
- return false;
- }
- }
- return true;
- }else{
- return false;
- }
-}
-
-void TermDb::filterInstances( std::vector< Node >& nodes ){
- std::vector< bool > active;
- active.resize( nodes.size(), true );
- std::map< int, std::vector< Node > > varContains;
- for( unsigned i=0; i<nodes.size(); i++ ){
- computeVarContains( nodes[i], varContains[i] );
- }
- for( unsigned i=0; i<nodes.size(); i++ ){
- for( unsigned j=i+1; j<nodes.size(); j++ ){
- if( active[i] && active[j] ){
- int result = isInstanceOf2( nodes[i], nodes[j], varContains[i], varContains[j] );
- if( result==1 ){
- Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
- active[j] = false;
- }else if( result==-1 ){
- Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
- active[i] = false;
- }
- }
- }
- }
- std::vector< Node > temp;
- for( unsigned i=0; i<nodes.size(); i++ ){
- if( active[i] ){
- temp.push_back( nodes[i] );
- }
- }
- nodes.clear();
- nodes.insert( nodes.begin(), temp.begin(), temp.end() );
-}
-
-int TermDb::getIdForOperator( Node op ) {
- std::map< Node, int >::iterator it = d_op_id.find( op );
- if( it==d_op_id.end() ){
- d_op_id[op] = d_op_id_count;
- d_op_id_count++;
- return d_op_id[op];
- }else{
- return it->second;
- }
-}
-
-int TermDb::getIdForType( TypeNode t ) {
- std::map< TypeNode, int >::iterator it = d_typ_id.find( t );
- if( it==d_typ_id.end() ){
- d_typ_id[t] = d_typ_id_count;
- d_typ_id_count++;
- return d_typ_id[t];
- }else{
- return it->second;
- }
-}
-
-bool TermDb::getTermOrder( Node a, Node b ) {
- if( a.getKind()==BOUND_VARIABLE ){
- if( b.getKind()==BOUND_VARIABLE ){
- return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute());
- }else{
- return true;
- }
- }else if( b.getKind()!=BOUND_VARIABLE ){
- Node aop = a.hasOperator() ? a.getOperator() : a;
- Node bop = b.hasOperator() ? b.getOperator() : b;
- Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
- Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
- if( aop==bop ){
- if( a.getNumChildren()==b.getNumChildren() ){
- for( unsigned i=0; i<a.getNumChildren(); i++ ){
- if( a[i]!=b[i] ){
- //first distinct child determines the ordering
- return getTermOrder( a[i], b[i] );
- }
- }
- }else{
- return aop.getNumChildren()<bop.getNumChildren();
- }
- }else{
- return getIdForOperator( aop )<getIdForOperator( bop );
- }
- }
- return false;
-}
-
-
-
-Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
- Assert( !tn.isNull() );
- while( d_cn_free_var[tn].size()<=i ){
- std::stringstream oss;
- oss << tn;
- std::string typ_name = oss.str();
- while( typ_name[0]=='(' ){
- typ_name.erase( typ_name.begin() );
- }
- std::stringstream os;
- os << typ_name[0] << i;
- Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
- InstVarNumAttribute ivna;
- x.setAttribute(ivna,d_cn_free_var[tn].size());
- d_cn_free_var[tn].push_back( x );
- }
- return d_cn_free_var[tn][i];
-}
-
-struct sortTermOrder {
- TermDb* d_tdb;
- //std::map< Node, std::map< Node, bool > > d_cache;
- bool operator() (Node i, Node j) {
- /*
- //must consult cache since term order is partial?
- std::map< Node, bool >::iterator it = d_cache[j].find( i );
- if( it!=d_cache[j].end() && it->second ){
- return false;
- }else{
- bool ret = d_tdb->getTermOrder( i, j );
- d_cache[i][j] = ret;
- return ret;
- }
- */
- return d_tdb->getTermOrder( i, j );
- }
-};
-
-//this function makes a canonical representation of a term (
-// - orders variables left to right
-// - if apply_torder, then sort direct subterms of commutative operators
-Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) {
- Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
- if( n.getKind()==BOUND_VARIABLE ){
- std::map< TNode, TNode >::iterator it = subs.find( n );
- if( it==subs.end() ){
- TypeNode tn = n.getType();
- //allocate variable
- unsigned vn = var_count[tn];
- var_count[tn]++;
- subs[n] = getCanonicalFreeVar( tn, vn );
- Trace("canon-term-debug") << "...allocate variable." << std::endl;
- return subs[n];
- }else{
- Trace("canon-term-debug") << "...return variable in subs." << std::endl;
- return it->second;
- }
- }else if( n.getNumChildren()>0 ){
- std::map< TNode, Node >::iterator it = visited.find( n );
- if( it!=visited.end() ){
- return it->second;
- }else{
- //collect children
- Trace("canon-term-debug") << "Collect children" << std::endl;
- std::vector< Node > cchildren;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- cchildren.push_back( n[i] );
- }
- //if applicable, first sort by term order
- if( apply_torder && isComm( n.getKind() ) ){
- Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
- sortTermOrder sto;
- sto.d_tdb = this;
- std::sort( cchildren.begin(), cchildren.end(), sto );
- }
- //now make canonical
- Trace("canon-term-debug") << "Make canonical children" << std::endl;
- for( unsigned i=0; i<cchildren.size(); i++ ){
- cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
- }
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
- cchildren.insert( cchildren.begin(), n.getOperator() );
- }
- Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
- Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
- Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
- visited[n] = ret;
- return ret;
- }
- }else{
- Trace("canon-term-debug") << "...return 0-child term." << std::endl;
- return n;
- }
-}
-
-Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
- std::map< TypeNode, unsigned > var_count;
- std::map< TNode, TNode > subs;
- std::map< TNode, Node > visited;
- return getCanonicalTerm( n, var_count, subs, apply_torder, visited );
-}
-
-void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
- if( inc_delta ){
- Node delta = getVtsDelta( isFree, create );
- if( !delta.isNull() ){
- t.push_back( delta );
- }
- }
- for( unsigned r=0; r<2; r++ ){
- Node inf = getVtsInfinityIndex( r, isFree, create );
- if( !inf.isNull() ){
- t.push_back( inf );
- }
- }
-}
-
-Node TermDb::getVtsDelta( bool isFree, bool create ) {
- if( create ){
- if( d_vts_delta_free.isNull() ){
- d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
- Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero );
- d_quantEngine->getOutputChannel().lemma( delta_lem );
- }
- if( d_vts_delta.isNull() ){
- d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" );
- //mark as a virtual term
- VirtualTermSkolemAttribute vtsa;
- d_vts_delta.setAttribute(vtsa,true);
- }
- }
- return isFree ? d_vts_delta_free : d_vts_delta;
-}
-
-Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
- if( create ){
- if( d_vts_inf_free[tn].isNull() ){
- d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" );
- }
- if( d_vts_inf[tn].isNull() ){
- d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" );
- //mark as a virtual term
- VirtualTermSkolemAttribute vtsa;
- d_vts_inf[tn].setAttribute(vtsa,true);
- }
- }
- return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
-}
-
-Node TermDb::getVtsInfinityIndex( int i, bool isFree, bool create ) {
- if( i==0 ){
- return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create );
- }else if( i==1 ){
- return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create );
- }else{
- Assert( false );
- return Node::null();
- }
-}
-
-Node TermDb::substituteVtsFreeTerms( Node n ) {
- std::vector< Node > vars;
- getVtsTerms( vars, false, false );
- std::vector< Node > vars_free;
- getVtsTerms( vars_free, true, false );
- Assert( vars.size()==vars_free.size() );
- if( !vars.empty() ){
- return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
- }else{
- return n;
- }
-}
-
-Node TermDb::rewriteVtsSymbols( Node n ) {
- if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){
- Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
- Node rew_vts_inf;
- bool rew_delta = false;
- //rewriting infinity always takes precedence over rewriting delta
- for( unsigned r=0; r<2; r++ ){
- Node inf = getVtsInfinityIndex( r, false, false );
- if( !inf.isNull() && containsTerm( n, inf ) ){
- if( rew_vts_inf.isNull() ){
- rew_vts_inf = inf;
- }else{
- //for mixed int/real with multiple infinities
- Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl;
- std::vector< Node > subs_lhs;
- subs_lhs.push_back( inf );
- std::vector< Node > subs_rhs;
- subs_lhs.push_back( rew_vts_inf );
- n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
- n = Rewriter::rewrite( n );
- //may have cancelled
- if( !containsTerm( n, rew_vts_inf ) ){
- rew_vts_inf = Node::null();
- }
- }
- }
- }
- if( rew_vts_inf.isNull() ){
- if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
- rew_delta = true;
- }
- }
- if( !rew_vts_inf.isNull() || rew_delta ){
- std::map< Node, Node > msum;
- if( QuantArith::getMonomialSumLit( n, msum ) ){
- if( Trace.isOn("quant-vts-debug") ){
- Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
- QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
- }
- Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta;
- Assert( !vts_sym.isNull() );
- Node iso_n;
- Node nlit;
- int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true );
- if( res!=0 ){
- Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl;
- Node slv = iso_n[res==1 ? 1 : 0];
- //ensure the vts terms have been eliminated
- if( containsVtsTerm( slv ) ){
- Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl;
- nlit = substituteVtsFreeTerms( n );
- Trace("quant-vts-debug") << "...return " << nlit << std::endl;
- //Assert( false );
- //safe case: just convert to free symbols
- return nlit;
- }else{
- if( !rew_vts_inf.isNull() ){
- nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false;
- }else{
- Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta );
- if( n.getKind()==EQUAL ){
- nlit = d_false;
- }else if( res==1 ){
- nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
- }else{
- nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
- }
- }
- }
- Trace("quant-vts-debug") << "Return " << nlit << std::endl;
- return nlit;
- }else{
- Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl;
- //safe case: just convert to free symbols
- nlit = substituteVtsFreeTerms( n );
- Trace("quant-vts-debug") << "...return " << nlit << std::endl;
- //Assert( false );
- return nlit;
- }
- }
- }
- return n;
- }else if( n.getKind()==FORALL ){
- //cannot traverse beneath quantifiers
- return substituteVtsFreeTerms( n );
- }else{
- bool childChanged = false;
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nn = rewriteVtsSymbols( n[i] );
- children.push_back( nn );
- childChanged = childChanged || nn!=n[i];
- }
- if( childChanged ){
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), n.getOperator() );
- }
- Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- Trace("quant-vts-debug") << "...make node " << ret << std::endl;
- return ret;
- }else{
- return n;
- }
- }
-}
-
-bool TermDb::containsVtsTerm( Node n, bool isFree ) {
- std::vector< Node > t;
- getVtsTerms( t, isFree, false );
- return containsTerms( n, t );
-}
-
-bool TermDb::containsVtsTerm( std::vector< Node >& n, bool isFree ) {
- std::vector< Node > t;
- getVtsTerms( t, isFree, false );
- if( !t.empty() ){
- for( unsigned i=0; i<n.size(); i++ ){
- if( containsTerms( n[i], t ) ){
- return true;
- }
- }
- }
- return false;
-}
-
-bool TermDb::containsVtsInfinity( Node n, bool isFree ) {
- std::vector< Node > t;
- getVtsTerms( t, isFree, false, false );
- return containsTerms( n, t );
-}
-
-Node TermDb::ensureType( Node n, TypeNode tn ) {
- TypeNode ntn = n.getType();
- Assert( ntn.isComparableTo( tn ) );
- if( ntn.isSubtypeOf( tn ) ){
- return n;
- }else{
- if( tn.isInteger() ){
- return NodeManager::currentNM()->mkNode( TO_INTEGER, n );
- }
- return Node::null();
- }
-}
-
-void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
- if( n.getKind()==APPLY_SELECTOR_TOTAL ){
- // don't worry about relevancy conditions if using shared selectors
- if( !options::dtSharedSelectors() ){
- unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());
- const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
- Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate();
- if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){
- cond.push_back( rc );
- }
- getRelevancyCondition( n[0], cond );
- }
- }
-}
-
-bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
- if( n==t ){
- return true;
- }else{
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( containsTerm2( n[i], t, visited ) ){
- return true;
- }
- }
- }
- return false;
- }
-}
-
-bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
- if( visited.find( n )==visited.end() ){
- if( std::find( t.begin(), t.end(), n )!=t.end() ){
- return true;
- }else{
- visited[n] = true;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( containsTerms2( n[i], t, visited ) ){
- return true;
- }
- }
- }
- }
- return false;
-}
-
-bool TermDb::containsTerm( Node n, Node t ) {
- std::map< Node, bool > visited;
- return containsTerm2( n, t, visited );
-}
-
-bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
- if( t.empty() ){
- return false;
- }else{
- std::map< Node, bool > visited;
- return containsTerms2( n, t, visited );
- }
-}
-
-int TermDb::getTermDepth( Node n ) {
- if (!n.hasAttribute(TermDepthAttribute()) ){
- int maxDepth = -1;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int depth = getTermDepth( n[i] );
- if( depth>maxDepth ){
- maxDepth = depth;
- }
- }
- TermDepthAttribute tda;
- n.setAttribute(tda,1+maxDepth);
- }
- return n.getAttribute(TermDepthAttribute());
-}
-
-bool TermDb::containsUninterpretedConstant( Node n ) {
- if (!n.hasAttribute(ContainsUConstAttribute()) ){
- bool ret = false;
- if( n.getKind()==UNINTERPRETED_CONSTANT ){
- ret = true;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( containsUninterpretedConstant( n[i] ) ){
- ret = true;
- break;
- }
- }
- }
- ContainsUConstAttribute cuca;
- n.setAttribute(cuca, ret ? 1 : 0);
- }
- return n.getAttribute(ContainsUConstAttribute())!=0;
-}
-
-Node TermDb::simpleNegate( Node n ){
- if( n.getKind()==OR || n.getKind()==AND ){
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- children.push_back( simpleNegate( n[i] ) );
- }
- return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children );
- }else{
- return n.negate();
- }
-}
-
-bool TermDb::isAssoc( Kind k ) {
- return k==PLUS || k==MULT || k==AND || k==OR ||
- k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
- k==STRING_CONCAT;
-}
-
-bool TermDb::isComm( Kind k ) {
- return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR ||
- k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
-}
-
-bool TermDb::isNonAdditive( Kind k ) {
- return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR;
-}
-
-bool TermDb::isBoolConnective( Kind k ) {
- return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
-}
-
-bool TermDb::isBoolConnectiveTerm( TNode n ) {
- return isBoolConnective( n.getKind() ) &&
- ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) &&
- ( n.getKind()!=ITE || n.getType().isBoolean() );
-}
-
-void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
- if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
- d_op_triggers[op].push_back( tr );
- }
-}
-
-Node TermDb::getHoTypeMatchPredicate( TypeNode tn ) {
- std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn );
- if( ithp==d_ho_type_match_pred.end() ){
- TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
- Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" );
- d_ho_type_match_pred[tn] = k;
- return k;
- }else{
- return ithp->second;
- }
-}
-
-bool TermDb::isInductionTerm( Node n ) {
- TypeNode tn = n.getType();
- if( options::dtStcInduction() && tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- return !dt.isCodatatype();
- }
- if( options::intWfInduction() && n.getType().isInteger() ){
- return true;
- }
- return false;
-}
-
-bool TermDb::isRewriteRule( Node q ) {
- return !getRewriteRule( q ).isNull();
-}
-
-Node TermDb::getRewriteRule( Node q ) {
- if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
- return q[2][0][0];
- }else{
- return Node::null();
- }
-}
-
-bool TermDb::isFunDef( Node q ) {
- return !getFunDefHead( q ).isNull();
-}
-
-bool TermDb::isFunDefAnnotation( Node ipl ) {
- if( !ipl.isNull() ){
- for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
- if( ipl[i].getKind()==INST_ATTRIBUTE ){
- if( ipl[i][0].getAttribute(FunDefAttribute()) ){
- return true;
- }
- }
- }
- }
- return false;
-}
-
-Node TermDb::getFunDefHead( Node q ) {
- //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
- if( q.getKind()==FORALL && q.getNumChildren()==3 ){
-
- for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
- if( q[2][i].getKind()==INST_ATTRIBUTE ){
- if( q[2][i][0].getAttribute(FunDefAttribute()) ){
- return q[2][i][0];
- }
- }
- }
- }
- return Node::null();
-}
-Node TermDb::getFunDefBody( Node q ) {
- Node h = getFunDefHead( q );
- if( !h.isNull() ){
- if( q[1].getKind()==EQUAL ){
- if( q[1][0]==h ){
- return q[1][1];
- }else if( q[1][1]==h ){
- return q[1][0];
- }
- }else{
- Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
- bool pol = q[1].getKind()!=NOT;
- if( atom==h ){
- return NodeManager::currentNM()->mkConst( pol );
- }
- }
- }
- return Node::null();
-}
-
-bool TermDb::isSygusConjecture( Node q ) {
- return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? isSygusConjectureAnnotation( q[2] ) : false;
-}
-
-bool TermDb::isSygusConjectureAnnotation( Node ipl ){
- if( !ipl.isNull() ){
- for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
- if( ipl[i].getKind()==INST_ATTRIBUTE ){
- Node avar = ipl[i][0];
- if( avar.getAttribute(SygusAttribute()) ){
- return true;
- }
- }
- }
- }
- return false;
-}
-
-bool TermDb::isQuantElimAnnotation( Node ipl ) {
- if( !ipl.isNull() ){
- for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
- if( ipl[i].getKind()==INST_ATTRIBUTE ){
- Node avar = ipl[i][0];
- if( avar.getAttribute(QuantElimAttribute()) ){
- return true;
- }
- }
- }
- }
- return false;
-}
-
-void TermDb::computeAttributes( Node q ) {
- computeQuantAttributes( q, d_qattr[q] );
- if( !d_qattr[q].d_rr.isNull() ){
- 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(), 2 );
- }
- if( d_qattr[q].isFunDef() ){
- Node f = d_qattr[q].d_fundef_f;
- if( d_fun_defs.find( f )!=d_fun_defs.end() ){
- Message() << "Cannot define function " << f << " more than once." << std::endl;
- exit( 1 );
- }
- d_fun_defs[f] = true;
- d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
- }
- if( d_qattr[q].d_sygus ){
- 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(), 2 );
- }
- if( d_qattr[q].d_synthesis ){
- 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(), 2 );
- }
-}
-
-void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
- Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
- if( q.getNumChildren()==3 ){
- qa.d_ipl = q[2];
- 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_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
- qa.d_hasPattern = true;
- }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
- Node avar = q[2][i][0];
- if( avar.getAttribute(AxiomAttribute()) ){
- Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
- qa.d_axiom = true;
- }
- if( avar.getAttribute(ConjectureAttribute()) ){
- Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
- qa.d_conjecture = true;
- }
- if( avar.getAttribute(FunDefAttribute()) ){
- Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
- //get operator directly from pattern
- qa.d_fundef_f = q[2][i][0].getOperator();
- }
- if( avar.getAttribute(SygusAttribute()) ){
- //not necessarily nested existential
- //Assert( q[1].getKind()==NOT );
- //Assert( q[1][0].getKind()==FORALL );
- Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
- qa.d_sygus = true;
- }
- if( avar.getAttribute(SynthesisAttribute()) ){
- Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
- qa.d_synthesis = true;
- }
- if( avar.hasAttribute(QuantInstLevelAttribute()) ){
- qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
- Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
- }
- if( avar.hasAttribute(RrPriorityAttribute()) ){
- qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
- Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
- }
- if( avar.getAttribute(QuantElimAttribute()) ){
- Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
- qa.d_quant_elim = true;
- //don't set owner, should happen naturally
- }
- if( avar.getAttribute(QuantElimPartialAttribute()) ){
- Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
- qa.d_quant_elim = true;
- qa.d_quant_elim_partial = true;
- //don't set owner, should happen naturally
- }
- if( avar.hasAttribute(QuantIdNumAttribute()) ){
- qa.d_qid_num = avar;
- Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
- }
- if( avar.getKind()==REWRITE_RULE ){
- Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
- Assert( i==0 );
- qa.d_rr = avar;
- }
- }
- }
- }
-}
-
-bool TermDb::isQAttrConjecture( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_conjecture;
- }
-}
-
-bool TermDb::isQAttrAxiom( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_axiom;
- }
-}
-
-bool TermDb::isQAttrFunDef( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.isFunDef();
- }
-}
-
-bool TermDb::isQAttrSygus( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_sygus;
- }
-}
-
-bool TermDb::isQAttrSynthesis( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_synthesis;
- }
-}
-
-int TermDb::getQAttrQuantInstLevel( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return -1;
- }else{
- return it->second.d_qinstLevel;
- }
-}
-
-int TermDb::getQAttrRewriteRulePriority( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return -1;
- }else{
- return it->second.d_rr_priority;
- }
-}
-
-bool TermDb::isQAttrQuantElim( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_quant_elim;
- }
-}
-
-bool TermDb::isQAttrQuantElimPartial( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return false;
- }else{
- return it->second.d_quant_elim_partial;
- }
-}
-
-int TermDb::getQAttrQuantIdNum( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it!=d_qattr.end() ){
- if( !it->second.d_qid_num.isNull() ){
- return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
- }
- }
- return -1;
-}
-
-Node TermDb::getQAttrQuantIdNumNode( Node q ) {
- std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
- if( it==d_qattr.end() ){
- return Node::null();
- }else{
- return it->second.d_qid_num;
- }
-}
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "theory/type_enumerator.h"
#include "theory/quantifiers/quant_util.h"
-
namespace CVC4 {
namespace theory {
-/** Attribute true for quantifiers that are axioms */
-struct AxiomAttributeId {};
-typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
-
-/** Attribute true for quantifiers that are conjecture */
-struct ConjectureAttributeId {};
-typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
-
-/** Attribute true for function definition quantifiers */
-struct FunDefAttributeId {};
-typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
-
-/** Attribute true for quantifiers that are SyGus conjectures */
-struct SygusAttributeId {};
-typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
-
-/** Attribute true for quantifiers that are synthesis conjectures */
-struct SynthesisAttributeId {};
-typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-
-// attribute for "contains instantiation constants from"
-struct InstConstantAttributeId {};
-typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
-
-struct BoundVarAttributeId {};
-typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
-
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
-struct InstVarNumAttributeId {};
-typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
-
-struct TermDepthAttributeId {};
-typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
-
-struct ContainsUConstAttributeId {};
-typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
-
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
-//for bounded integers
-struct BoundIntLitAttributeId {};
-typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
-
-//for quantifier instantiation level
-struct QuantInstLevelAttributeId {};
-typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
-
-//rewrite-rule priority
-struct RrPriorityAttributeId {};
-typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
-
-/** Attribute true for quantifiers that do not need to be partially instantiated */
-struct LtePartialInstAttributeId {};
-typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
-
-// attribute for "contains instantiation constants from"
-struct SygusProxyAttributeId {};
-typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
-
-// attribute for associating a synthesis function with a first order variable
-struct SygusSynthFunAttributeId {};
-typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute;
-
-// attribute for associating a variable list with a synth fun
-struct SygusSynthFunVarListAttributeId {};
-typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> SygusSynthFunVarListAttribute;
-
-//attribute for fun-def abstraction type
-struct AbsTypeFunDefAttributeId {};
-typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
-
-/** Attribute true for quantifiers that we are doing quantifier elimination on */
-struct QuantElimAttributeId {};
-typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
-
-/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
-struct QuantElimPartialAttributeId {};
-typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
-
-/** Attribute for id number */
-struct QuantIdNumAttributeId {};
-typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
-
-/** sygus var num */
-struct SygusVarNumAttributeId {};
-typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
-
-/** Attribute to mark Skolems as virtual terms */
-struct VirtualTermSkolemAttributeId {};
-typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
-
-
class QuantifiersEngine;
namespace inst{
void clear() { d_data.clear(); }
};/* class TermArgTrie */
-
-class QAttributes{
-public:
- QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
- d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
- ~QAttributes(){}
- bool d_hasPattern;
- Node d_rr;
- bool d_conjecture;
- bool d_axiom;
- Node d_fundef_f;
- bool d_sygus;
- bool d_synthesis;
- int d_rr_priority;
- int d_qinstLevel;
- bool d_quant_elim;
- bool d_quant_elim_partial;
- Node d_ipl;
- Node d_qid_num;
- bool isRewriteRule() { return !d_rr.isNull(); }
- bool isFunDef() { return !d_fundef_f.isNull(); }
-};
-
namespace fmcheck {
class FullModelChecker;
}
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
/** whether master equality engine is UF-inconsistent */
bool d_consistent_ee;
-
- public:
- TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
- ~TermDb();
/** boolean terms */
Node d_true;
Node d_false;
- /** constants */
- Node d_zero;
- Node d_one;
-
- public:
+public:
+ TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+ ~TermDb();
+
+ /** register quantified formula */
+ void registerQuantifier( Node q );
+public:
/** presolve (called once per user check-sat) */
void presolve();
/** reset (calculate which terms are active) */
bool reset( Theory::Effort effort );
/** identify */
std::string identify() const { return "TermDb"; }
- private:
+private:
/** map from operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
/** map from type nodes to terms of that type */
Node getModelBasis( Node q, Node n );
//get model basis body
Node getModelBasisBody( Node q );
-
-//for inst constant
-private:
- /** map from universal quantifiers to the list of variables */
- std::map< Node, std::vector< Node > > d_vars;
- std::map< Node, std::map< Node, unsigned > > d_var_num;
- /** map from universal quantifiers to their inst constant body */
- std::map< Node, Node > d_inst_const_body;
- /** map from universal quantifiers to their counterexample literals */
- std::map< Node, Node > d_ce_lit;
- /** instantiation constants to universal quantifiers */
- std::map< Node, Node > d_inst_constants_map;
- /** make instantiation constants for */
- void makeInstantiationConstantsFor( Node q );
-public:
- /** map from universal quantifiers to the list of instantiation constants */
- std::map< Node, std::vector< Node > > d_inst_constants;
- /** get variable number */
- unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
- /** get the i^th instantiation constant of q */
- Node getInstantiationConstant( Node q, int i ) const;
- /** get number of instantiation constants for q */
- unsigned getNumInstantiationConstants( Node q ) const;
- /** get the ce body q[e/x] */
- Node getInstConstantBody( Node q );
- /** get counterexample literal (for cbqi) */
- Node getCounterexampleLiteral( Node q );
- /** returns node n with bound vars of q replaced by instantiation constants of q
- node n : is the future pattern
- node q : is the quantifier containing which bind the variable
- return a pattern where the variable are replaced by variable for
- instantiation.
- */
- Node getInstConstantNode( Node n, Node q );
- Node getVariableNode( Node n, Node q );
- /** get substituted node */
- Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
-
- static Node getInstConstAttr( Node n );
- static bool hasInstConstAttr( Node n );
- static Node getBoundVarAttr( Node n );
- static bool hasBoundVarAttr( Node n );
-private:
- /** get bound vars */
- static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
- /** get bound vars */
- static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited );
-public:
- //get the bound variables in this node
- static void getBoundVars( Node n, std::vector< Node >& vars );
- //remove quantifiers
- static Node getRemoveQuantifiers( Node n );
- //quantified simplify (treat free variables in n as quantified and run rewriter)
- static Node getQuantSimplify( Node n );
-
-//for skolem
-private:
- /** map from universal quantifiers to their skolemized body */
- std::map< Node, Node > d_skolem_body;
-public:
- /** map from universal quantifiers to the list of skolem constants */
- std::map< Node, std::vector< Node > > d_skolem_constants;
- /** make the skolemized body f[e/x] */
- static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
- 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;
- // closed enumerable type cache
- std::map< TypeNode, bool > d_typ_closed_enum;
- /** may complete */
- std::map< TypeNode, bool > d_may_complete;
-public:
- //get nth term for type
- Node getEnumerateTerm( TypeNode tn, unsigned index );
- //does this type have an enumerator that produces constants that are handled by ground theory solvers
- bool isClosedEnumerableType( TypeNode tn );
- // may complete
- bool mayComplete( TypeNode tn );
-
-//for triggers
-private:
- /** helper function for compute var contains */
- static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
- /** triggers for each operator */
- std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
- /** helper for is instance of */
- static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
- /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
- static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
-public:
- /** compute var contains */
- static void computeVarContains( Node n, std::vector< Node >& varContains );
- /** get var contains for each of the patterns in pats */
- static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
- /** get var contains for node n */
- static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
- /** compute quant contains */
- static void computeQuantContains( Node n, std::vector< Node >& quantContains );
- /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
- static int isInstanceOf( Node n1, Node n2 );
- /** filter all nodes that have instances */
- static void filterInstances( std::vector< Node >& nodes );
- /** register trigger (for eager quantifier instantiation) */
- void registerTrigger( inst::Trigger* tr, Node op );
-
-//for term ordering
-private:
- /** operator id count */
- int d_op_id_count;
- /** map from operators to id */
- std::map< Node, int > d_op_id;
- /** type id count */
- int d_typ_id_count;
- /** map from type to id */
- std::map< TypeNode, int > d_typ_id;
- //free variables
- std::map< TypeNode, std::vector< Node > > d_cn_free_var;
- // get canonical term, return null if it contains a term apart from handled signature
- Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder,
- std::map< TNode, Node >& visited );
-public:
- /** get id for operator */
- int getIdForOperator( Node op );
- /** get id for type */
- int getIdForType( TypeNode t );
- /** get term order */
- bool getTermOrder( Node a, Node b );
- /** get canonical free variable #i of type tn */
- Node getCanonicalFreeVar( TypeNode tn, unsigned i );
- /** get canonical term */
- Node getCanonicalTerm( TNode n, bool apply_torder = false );
-
-//for virtual term substitution
-private:
- Node d_vts_delta;
- std::map< TypeNode, Node > d_vts_inf;
- Node d_vts_delta_free;
- std::map< TypeNode, Node > d_vts_inf_free;
- /** get vts infinity index */
- Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true );
- /** substitute vts free terms */
- Node substituteVtsFreeTerms( Node n );
-public:
- /** get vts delta */
- Node getVtsDelta( bool isFree = false, bool create = true );
- /** get vts infinity */
- Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true );
- /** get all vts terms */
- void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true );
- /** rewrite delta */
- Node rewriteVtsSymbols( Node n );
- /** simple check for contains term */
- bool containsVtsTerm( Node n, bool isFree = false );
- /** simple check for contains term */
- bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
- /** simple check for contains term */
- bool containsVtsInfinity( Node n, bool isFree = false );
- /** ensure type */
- static Node ensureType( Node n, TypeNode tn );
- /** get relevancy condition */
- static void getRelevancyCondition( Node n, std::vector< Node >& cond );
-private:
- //helper for contains term
- static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
- static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
-//general utilities
-public:
- /** simple check for whether n contains t as subterm */
- static bool containsTerm( Node n, Node t );
- /** simple check for contains term, true if contains at least one term in t */
- static bool containsTerms( Node n, std::vector< Node >& t );
- /** contains uninterpreted constant */
- static bool containsUninterpretedConstant( Node n );
- /** get the term depth of n */
- static int getTermDepth( Node n );
- /** simple negate */
- static Node simpleNegate( Node n );
- /** is assoc */
- static bool isAssoc( Kind k );
- /** is comm */
- static bool isComm( Kind k );
- /** ( x k ... ) k x = ( x k ... ) */
- static bool isNonAdditive( Kind k );
- /** is bool connective */
- static bool isBoolConnective( Kind k );
- /** is bool connective term */
- static bool isBoolConnectiveTerm( TNode n );
-
-//for higher-order
-private:
- /** dummy predicate that states terms should be considered first-class members of equality engine */
- std::map< TypeNode, Node > d_ho_type_match_pred;
-public:
- /** get higher-order type match predicate
- * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the
- * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh
- * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma.
- * TODO: we may eliminate this depending on how github issue #1115 is resolved.
- */
- Node getHoTypeMatchPredicate( TypeNode tn );
-
-//for sygus
-private:
- TermDbSygus * d_sygus_tdb;
-public:
- TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
-
-private:
- std::map< Node, bool > d_fun_defs;
-public: //general queries concerning quantified formulas wrt modules
- /** is quantifier treated as a rewrite rule? */
- static bool isRewriteRule( Node q );
- /** get the rewrite rule associated with the quanfied formula */
- static Node getRewriteRule( Node q );
- /** is fun def */
- static bool isFunDef( Node q );
- /** is fun def */
- static bool isFunDefAnnotation( Node ipl );
- /** is sygus conjecture */
- static bool isSygusConjecture( Node q );
- /** is sygus conjecture */
- static bool isSygusConjectureAnnotation( Node ipl );
- /** get fun def body */
- static Node getFunDefHead( Node q );
- /** get fun def body */
- static Node getFunDefBody( Node q );
- /** is quant elim annotation */
- static bool isQuantElimAnnotation( Node ipl );
-//attributes
-private:
- std::map< Node, QAttributes > d_qattr;
- //record attributes
- void computeAttributes( Node q );
-public:
- /** is conjecture */
- bool isQAttrConjecture( Node q );
- /** is axiom */
- bool isQAttrAxiom( Node q );
- /** is function definition */
- bool isQAttrFunDef( Node q );
- /** is sygus conjecture */
- bool isQAttrSygus( Node q );
- /** is synthesis conjecture */
- bool isQAttrSynthesis( Node q );
- /** get instantiation level */
- int getQAttrQuantInstLevel( Node q );
- /** get rewrite rule priority */
- int getQAttrRewriteRulePriority( Node q );
- /** is quant elim */
- bool isQAttrQuantElim( Node q );
- /** is quant elim partial */
- bool isQAttrQuantElimPartial( Node q );
- /** get quant id num */
- int getQAttrQuantIdNum( Node q );
- /** get quant id num */
- Node getQAttrQuantIdNumNode( Node q );
- /** compute quantifier attributes */
- static void computeQuantAttributes( Node q, QAttributes& qa );
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fun_def_engine.h"
-#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
return p==n;
}else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){
//try both ways?
- unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
+ unsigned rmax = TermUtil::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
std::vector< int > new_tmp;
for( unsigned r=0; r<rmax; r++ ){
bool success = true;
int pc = getKindConsNum( tnp, pk );
if( k==pk ){
//check for associativity
- if( quantifiers::TermDb::isAssoc( k ) ){
+ if( quantifiers::TermUtil::isAssoc( k ) ){
//if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
int firstArg = getFirstArgOccurrence( pdt[pc], tn );
Assert( firstArg!=-1 );
Assert( dt.isSygus() );
Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
- Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn );
+ Node bTerm = sygusToBuiltin( vn, tn );
Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
std::vector< Node > vars;
Node var_list = Node::fromExpr( dt.getSygusVarList() );
--- /dev/null
+/********************* */
+/*! \file term_util.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of term utilities class
+ **/
+
+#include "theory/quantifiers/term_util.h"
+
+#include "expr/datatype.h"
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "options/datatypes_options.h"
+#include "options/uf_options.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TermUtil::TermUtil(QuantifiersEngine * qe) :
+d_quantEngine(qe),
+d_op_id_count(0),
+d_typ_id_count(0){
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+ d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(Rational(1));
+}
+
+TermUtil::~TermUtil(){
+
+}
+
+void TermUtil::registerQuantifier( Node q ){
+ if( d_inst_constants.find( q )==d_inst_constants.end() ){
+ Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ d_vars[q].push_back( q[0][i] );
+ d_var_num[q][q[0][i]] = i;
+ //make instantiation constants
+ Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
+ d_inst_constants_map[ic] = q;
+ d_inst_constants[ q ].push_back( ic );
+ Debug("quantifiers-engine") << " " << ic << std::endl;
+ //set the var number attribute
+ InstVarNumAttribute ivna;
+ ic.setAttribute( ivna, i );
+ InstConstantAttribute ica;
+ ic.setAttribute( ica, q );
+ }
+ }
+}
+
+void TermUtil::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==BOUND_VARIABLE ){
+ if( std::find( vars.begin(), vars.end(), n )==vars.end() ) {
+ vars.push_back( n );
+ }
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ getBoundVars2( n[i], vars, visited );
+ }
+ }
+}
+
+Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+ Node ret = n;
+ if( n.getKind()==FORALL ){
+ ret = getRemoveQuantifiers2( n[1], visited );
+ }else if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ bool childrenChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node ni = getRemoveQuantifiers2( n[i], visited );
+ childrenChanged = childrenChanged || ni!=n[i];
+ children.push_back( ni );
+ }
+ if( childrenChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ visited[n] = ret;
+ return ret;
+ }
+}
+
+Node TermUtil::getInstConstAttr( Node n ) {
+ if (!n.hasAttribute(InstConstantAttribute()) ){
+ Node q;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ q = getInstConstAttr(n[i]);
+ if( !q.isNull() ){
+ break;
+ }
+ }
+ InstConstantAttribute ica;
+ n.setAttribute(ica, q);
+ }
+ return n.getAttribute(InstConstantAttribute());
+}
+
+bool TermUtil::hasInstConstAttr( Node n ) {
+ return !getInstConstAttr(n).isNull();
+}
+
+Node TermUtil::getBoundVarAttr( Node n ) {
+ if (!n.hasAttribute(BoundVarAttribute()) ){
+ Node bv;
+ if( n.getKind()==BOUND_VARIABLE ){
+ bv = n;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bv = getBoundVarAttr(n[i]);
+ if( !bv.isNull() ){
+ break;
+ }
+ }
+ }
+ BoundVarAttribute bva;
+ n.setAttribute(bva, bv);
+ }
+ return n.getAttribute(BoundVarAttribute());
+}
+
+bool TermUtil::hasBoundVarAttr( Node n ) {
+ return !getBoundVarAttr(n).isNull();
+}
+
+void TermUtil::getBoundVars( Node n, std::vector< Node >& vars ) {
+ std::map< Node, bool > visited;
+ return getBoundVars2( n, vars, visited );
+}
+
+//remove quantifiers
+Node TermUtil::getRemoveQuantifiers( Node n ) {
+ std::map< Node, Node > visited;
+ return getRemoveQuantifiers2( n, visited );
+}
+
+//quantified simplify
+Node TermUtil::getQuantSimplify( Node n ) {
+ std::vector< Node > bvs;
+ getBoundVars( n, bvs );
+ if( bvs.empty() ) {
+ return Rewriter::rewrite( n );
+ }else{
+ Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n );
+ q = Rewriter::rewrite( q );
+ return getRemoveQuantifiers( q );
+ }
+}
+
+/** get the i^th instantiation constant of q */
+Node TermUtil::getInstantiationConstant( Node q, int i ) const {
+ std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
+ if( it!=d_inst_constants.end() ){
+ return it->second[i];
+ }else{
+ return Node::null();
+ }
+}
+
+/** get number of instantiation constants for q */
+unsigned TermUtil::getNumInstantiationConstants( Node q ) const {
+ std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
+ if( it!=d_inst_constants.end() ){
+ return it->second.size();
+ }else{
+ return 0;
+ }
+}
+
+Node TermUtil::getInstConstantBody( Node q ){
+ std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
+ if( it==d_inst_const_body.end() ){
+ Node n = getInstConstantNode( q[1], q );
+ d_inst_const_body[ q ] = n;
+ return n;
+ }else{
+ return it->second;
+ }
+}
+
+Node TermUtil::getCounterexampleLiteral( Node q ){
+ if( d_ce_lit.find( q )==d_ce_lit.end() ){
+ /*
+ Node ceBody = getInstConstantBody( f );
+ //check if any variable are of bad types, and fail if so
+ for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
+ if( d_inst_constants[f][i].getType().isBoolean() ){
+ d_ce_lit[ f ] = Node::null();
+ return Node::null();
+ }
+ }
+ */
+ Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+ //otherwise, ensure literal
+ Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
+ d_ce_lit[ q ] = ceLit;
+ }
+ return d_ce_lit[ q ];
+}
+
+Node TermUtil::getInstConstantNode( Node n, Node q ){
+ registerQuantifier( q );
+ return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
+}
+
+Node TermUtil::getVariableNode( Node n, Node q ) {
+ registerQuantifier( q );
+ return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
+}
+
+Node TermUtil::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
+ Assert( d_vars[q].size()==terms.size() );
+ return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
+}
+
+
+void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+ TypeNode tspec;
+ if( dt.isParametric() ){
+ tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
+ Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
+ Assert( tspec.getNumChildren()==dc.getNumArgs() );
+ }
+ Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
+ for( unsigned j=0; j<dc.getNumArgs(); j++ ){
+ std::vector< Node > ssc;
+ if( dt.isParametric() ){
+ Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
+ if( tspec[j]==ntn ){
+ ssc.push_back( n );
+ }
+ }else{
+ TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
+ Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+ if( tn==ntn ){
+ ssc.push_back( n );
+ }
+ }
+ /* TODO: more than weak structural induction
+ else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
+ visited.push_back( tn );
+ const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
+ std::vector< Node > disj;
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ getSelfSel( dt[i], n, ntn, ssc );
+ }
+ visited.pop_back();
+ }
+ */
+ for( unsigned k=0; k<ssc.size(); k++ ){
+ Node ss = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n );
+ if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){
+ selfSel.push_back( ss );
+ }
+ }
+ }
+}
+
+
+Node TermUtil::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
+ std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
+ Assert( sk.empty() || sk.size()==f[0].getNumChildren() );
+ //calculate the variables and substitution
+ std::vector< TNode > ind_vars;
+ std::vector< unsigned > ind_var_indicies;
+ std::vector< TNode > vars;
+ std::vector< unsigned > var_indicies;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ if( isInductionTerm( f[0][i] ) ){
+ ind_vars.push_back( f[0][i] );
+ ind_var_indicies.push_back( i );
+ }else{
+ vars.push_back( f[0][i] );
+ var_indicies.push_back( i );
+ }
+ Node s;
+ //make the new function symbol or use existing
+ if( i>=sk.size() ){
+ if( argTypes.empty() ){
+ s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
+ }else{
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
+ Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
+ //DOTHIS: set attribute on op, marking that it should not be selected as trigger
+ std::vector< Node > funcArgs;
+ funcArgs.push_back( op );
+ funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
+ s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+ }
+ sk.push_back( s );
+ }else{
+ Assert( sk[i].getType()==f[0][i].getType() );
+ }
+ }
+ Node ret;
+ if( vars.empty() ){
+ ret = n;
+ }else{
+ std::vector< Node > var_sk;
+ for( unsigned i=0; i<var_indicies.size(); i++ ){
+ var_sk.push_back( sk[var_indicies[i]] );
+ }
+ Assert( vars.size()==var_sk.size() );
+ ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
+ }
+ if( !ind_vars.empty() ){
+ Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
+ Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
+ Node n_str_ind;
+ TypeNode tn = ind_vars[0].getType();
+ Node k = sk[ind_var_indicies[0]];
+ Node nret = ret.substitute( ind_vars[0], k );
+ //note : everything is under a negation
+ //the following constructs ~( R( x, k ) => ~P( x ) )
+ if( options::dtStcInduction() && tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ std::vector< Node > disj;
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ std::vector< Node > selfSel;
+ getSelfSel( dt, dt[i], k, tn, selfSel );
+ std::vector< Node > conj;
+ conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
+ for( unsigned j=0; j<selfSel.size(); j++ ){
+ conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() );
+ }
+ disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
+ }
+ Assert( !disj.empty() );
+ n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
+ }else if( options::intWfInduction() && tn.isInteger() ){
+ Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) );
+ Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate();
+ n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret );
+ n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind );
+ }else{
+ Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl;
+ Assert( false );
+ }
+ Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
+
+ std::vector< Node > rem_ind_vars;
+ rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() );
+ if( !rem_ind_vars.empty() ){
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars );
+ nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret );
+ nret = Rewriter::rewrite( nret );
+ sub = nret;
+ sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() );
+ n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate();
+ }
+ ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
+ }
+ Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
+ //if it has an instantiation level, set the skolemized body to that level
+ if( f.hasAttribute(InstLevelAttribute()) ){
+ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
+ }
+
+ if( Trace.isOn("quantifiers-sk") ){
+ Trace("quantifiers-sk") << "Skolemize : ";
+ for( unsigned i=0; i<sk.size(); i++ ){
+ Trace("quantifiers-sk") << sk[i] << " ";
+ }
+ Trace("quantifiers-sk") << "for " << std::endl;
+ Trace("quantifiers-sk") << " " << f << std::endl;
+ }
+
+ return ret;
+}
+
+Node TermUtil::getSkolemizedBody( Node f ){
+ Assert( f.getKind()==FORALL );
+ if( d_skolem_body.find( f )==d_skolem_body.end() ){
+ std::vector< TypeNode > fvTypes;
+ std::vector< TNode > fvs;
+ Node sub;
+ std::vector< unsigned > sub_vars;
+ d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
+ //store sub quantifier information
+ if( !sub.isNull() ){
+ //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them
+ Assert( d_skolem_constants[sub].empty() );
+ for( unsigned i=0; i<sub_vars.size(); i++ ){
+ d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] );
+ }
+ }
+ Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
+ if( options::sortInference() ){
+ for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
+ //carry information for sort inference
+ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
+ }
+ }
+ }
+ return d_skolem_body[ f ];
+}
+
+Node TermUtil::getEnumerateTerm( TypeNode tn, unsigned index ) {
+ Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
+ 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];
+}
+
+bool TermUtil::isClosedEnumerableType( TypeNode tn ) {
+ std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
+ if( it==d_typ_closed_enum.end() ){
+ d_typ_closed_enum[tn] = true;
+ bool ret = true;
+ if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){
+ ret = false;
+ }else if( tn.isSet() ){
+ ret = isClosedEnumerableType( tn.getSetElementType() );
+ }else if( tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+ TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
+ if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
+ ret = false;
+ break;
+ }
+ }
+ if( !ret ){
+ break;
+ }
+ }
+ }
+ //TODO: other parametric sorts go here
+ d_typ_closed_enum[tn] = ret;
+ return ret;
+ }else{
+ return it->second;
+ }
+}
+
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
+bool TermUtil::mayComplete( TypeNode tn ) {
+ std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
+ if( it==d_may_complete.end() ){
+ bool mc = false;
+ if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
+ Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
+ Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
+ Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
+ eq = Rewriter::rewrite( eq );
+ mc = eq==d_true;
+ }
+ d_may_complete[tn] = mc;
+ return mc;
+ }else{
+ return it->second;
+ }
+}
+
+void TermUtil::computeVarContains( Node n, std::vector< Node >& varContains ) {
+ std::map< Node, bool > visited;
+ computeVarContains2( n, INST_CONSTANT, varContains, visited );
+}
+
+void TermUtil::computeQuantContains( Node n, std::vector< Node >& quantContains ) {
+ std::map< Node, bool > visited;
+ computeVarContains2( n, FORALL, quantContains, visited );
+}
+
+
+void TermUtil::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==k ){
+ if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){
+ varContains.push_back( n );
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ computeVarContains2( n[i], k, varContains, visited );
+ }
+ }
+ }
+}
+
+void TermUtil::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
+ for( unsigned i=0; i<pats.size(); i++ ){
+ varContains[ pats[i] ].clear();
+ getVarContainsNode( f, pats[i], varContains[ pats[i] ] );
+ }
+}
+
+void TermUtil::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
+ std::vector< Node > vars;
+ computeVarContains( n, vars );
+ for( unsigned j=0; j<vars.size(); j++ ){
+ Node v = vars[j];
+ if( v.getAttribute(InstConstantAttribute())==f ){
+ if( std::find( varContains.begin(), varContains.end(), v )==varContains.end() ){
+ varContains.push_back( v );
+ }
+ }
+ }
+}
+
+int TermUtil::isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ){
+ if( n1==n2 ){
+ return 1;
+ }else if( n1.getKind()==n2.getKind() ){
+ if( n1.getKind()==APPLY_UF ){
+ if( n1.getOperator()==n2.getOperator() ){
+ int result = 0;
+ for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+ if( n1[i]!=n2[i] ){
+ int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 );
+ if( cResult==0 ){
+ return 0;
+ }else if( cResult!=result ){
+ if( result!=0 ){
+ return 0;
+ }else{
+ result = cResult;
+ }
+ }
+ }
+ }
+ return result;
+ }
+ }
+ return 0;
+ }else if( n2.getKind()==INST_CONSTANT ){
+ //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
+ // return 1;
+ //}
+ if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){
+ return 1;
+ }
+ }else if( n1.getKind()==INST_CONSTANT ){
+ //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
+ // return -1;
+ //}
+ if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){
+ return 1;
+ }
+ }
+ return 0;
+}
+
+int TermUtil::isInstanceOf( Node n1, Node n2 ){
+ std::vector< Node > varContains1;
+ std::vector< Node > varContains2;
+ computeVarContains( n1, varContains1 );
+ computeVarContains( n1, varContains2 );
+ return isInstanceOf2( n1, n2, varContains1, varContains2 );
+}
+
+bool TermUtil::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
+ if( n1==n2 ){
+ return true;
+ }else if( n2.getKind()==INST_CONSTANT ){
+ //if( !node_contains( n1, n2 ) ){
+ // return false;
+ //}
+ if( subs.find( n2 )==subs.end() ){
+ subs[n2] = n1;
+ }else if( subs[n2]!=n1 ){
+ return false;
+ }
+ return true;
+ }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
+ if( n1.getOperator()!=n2.getOperator() ){
+ return false;
+ }
+ for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+ if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
+ return false;
+ }
+ }
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void TermUtil::filterInstances( std::vector< Node >& nodes ){
+ std::vector< bool > active;
+ active.resize( nodes.size(), true );
+ std::map< int, std::vector< Node > > varContains;
+ for( unsigned i=0; i<nodes.size(); i++ ){
+ computeVarContains( nodes[i], varContains[i] );
+ }
+ for( unsigned i=0; i<nodes.size(); i++ ){
+ for( unsigned j=i+1; j<nodes.size(); j++ ){
+ if( active[i] && active[j] ){
+ int result = isInstanceOf2( nodes[i], nodes[j], varContains[i], varContains[j] );
+ if( result==1 ){
+ Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
+ active[j] = false;
+ }else if( result==-1 ){
+ Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
+ active[i] = false;
+ }
+ }
+ }
+ }
+ std::vector< Node > temp;
+ for( unsigned i=0; i<nodes.size(); i++ ){
+ if( active[i] ){
+ temp.push_back( nodes[i] );
+ }
+ }
+ nodes.clear();
+ nodes.insert( nodes.begin(), temp.begin(), temp.end() );
+}
+
+int TermUtil::getIdForOperator( Node op ) {
+ std::map< Node, int >::iterator it = d_op_id.find( op );
+ if( it==d_op_id.end() ){
+ d_op_id[op] = d_op_id_count;
+ d_op_id_count++;
+ return d_op_id[op];
+ }else{
+ return it->second;
+ }
+}
+
+int TermUtil::getIdForType( TypeNode t ) {
+ std::map< TypeNode, int >::iterator it = d_typ_id.find( t );
+ if( it==d_typ_id.end() ){
+ d_typ_id[t] = d_typ_id_count;
+ d_typ_id_count++;
+ return d_typ_id[t];
+ }else{
+ return it->second;
+ }
+}
+
+bool TermUtil::getTermOrder( Node a, Node b ) {
+ if( a.getKind()==BOUND_VARIABLE ){
+ if( b.getKind()==BOUND_VARIABLE ){
+ return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute());
+ }else{
+ return true;
+ }
+ }else if( b.getKind()!=BOUND_VARIABLE ){
+ Node aop = a.hasOperator() ? a.getOperator() : a;
+ Node bop = b.hasOperator() ? b.getOperator() : b;
+ Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
+ Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
+ if( aop==bop ){
+ if( a.getNumChildren()==b.getNumChildren() ){
+ for( unsigned i=0; i<a.getNumChildren(); i++ ){
+ if( a[i]!=b[i] ){
+ //first distinct child determines the ordering
+ return getTermOrder( a[i], b[i] );
+ }
+ }
+ }else{
+ return aop.getNumChildren()<bop.getNumChildren();
+ }
+ }else{
+ return getIdForOperator( aop )<getIdForOperator( bop );
+ }
+ }
+ return false;
+}
+
+
+
+Node TermUtil::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
+ Assert( !tn.isNull() );
+ while( d_cn_free_var[tn].size()<=i ){
+ std::stringstream oss;
+ oss << tn;
+ std::string typ_name = oss.str();
+ while( typ_name[0]=='(' ){
+ typ_name.erase( typ_name.begin() );
+ }
+ std::stringstream os;
+ os << typ_name[0] << i;
+ Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
+ InstVarNumAttribute ivna;
+ x.setAttribute(ivna,d_cn_free_var[tn].size());
+ d_cn_free_var[tn].push_back( x );
+ }
+ return d_cn_free_var[tn][i];
+}
+
+struct sortTermOrder {
+ TermUtil* d_tu;
+ //std::map< Node, std::map< Node, bool > > d_cache;
+ bool operator() (Node i, Node j) {
+ /*
+ //must consult cache since term order is partial?
+ std::map< Node, bool >::iterator it = d_cache[j].find( i );
+ if( it!=d_cache[j].end() && it->second ){
+ return false;
+ }else{
+ bool ret = d_tdb->getTermOrder( i, j );
+ d_cache[i][j] = ret;
+ return ret;
+ }
+ */
+ return d_tu->getTermOrder( i, j );
+ }
+};
+
+//this function makes a canonical representation of a term (
+// - orders variables left to right
+// - if apply_torder, then sort direct subterms of commutative operators
+Node TermUtil::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) {
+ Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
+ if( n.getKind()==BOUND_VARIABLE ){
+ std::map< TNode, TNode >::iterator it = subs.find( n );
+ if( it==subs.end() ){
+ TypeNode tn = n.getType();
+ //allocate variable
+ unsigned vn = var_count[tn];
+ var_count[tn]++;
+ subs[n] = getCanonicalFreeVar( tn, vn );
+ Trace("canon-term-debug") << "...allocate variable." << std::endl;
+ return subs[n];
+ }else{
+ Trace("canon-term-debug") << "...return variable in subs." << std::endl;
+ return it->second;
+ }
+ }else if( n.getNumChildren()>0 ){
+ std::map< TNode, Node >::iterator it = visited.find( n );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+ //collect children
+ Trace("canon-term-debug") << "Collect children" << std::endl;
+ std::vector< Node > cchildren;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ cchildren.push_back( n[i] );
+ }
+ //if applicable, first sort by term order
+ if( apply_torder && isComm( n.getKind() ) ){
+ Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
+ sortTermOrder sto;
+ sto.d_tu = this;
+ std::sort( cchildren.begin(), cchildren.end(), sto );
+ }
+ //now make canonical
+ Trace("canon-term-debug") << "Make canonical children" << std::endl;
+ for( unsigned i=0; i<cchildren.size(); i++ ){
+ cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
+ }
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
+ cchildren.insert( cchildren.begin(), n.getOperator() );
+ }
+ Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
+ Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+ Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
+ visited[n] = ret;
+ return ret;
+ }
+ }else{
+ Trace("canon-term-debug") << "...return 0-child term." << std::endl;
+ return n;
+ }
+}
+
+Node TermUtil::getCanonicalTerm( TNode n, bool apply_torder ){
+ std::map< TypeNode, unsigned > var_count;
+ std::map< TNode, TNode > subs;
+ std::map< TNode, Node > visited;
+ return getCanonicalTerm( n, var_count, subs, apply_torder, visited );
+}
+
+void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
+ if( inc_delta ){
+ Node delta = getVtsDelta( isFree, create );
+ if( !delta.isNull() ){
+ t.push_back( delta );
+ }
+ }
+ for( unsigned r=0; r<2; r++ ){
+ Node inf = getVtsInfinityIndex( r, isFree, create );
+ if( !inf.isNull() ){
+ t.push_back( inf );
+ }
+ }
+}
+
+Node TermUtil::getVtsDelta( bool isFree, bool create ) {
+ if( create ){
+ if( d_vts_delta_free.isNull() ){
+ d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
+ Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero );
+ d_quantEngine->getOutputChannel().lemma( delta_lem );
+ }
+ if( d_vts_delta.isNull() ){
+ d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" );
+ //mark as a virtual term
+ VirtualTermSkolemAttribute vtsa;
+ d_vts_delta.setAttribute(vtsa,true);
+ }
+ }
+ return isFree ? d_vts_delta_free : d_vts_delta;
+}
+
+Node TermUtil::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
+ if( create ){
+ if( d_vts_inf_free[tn].isNull() ){
+ d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" );
+ }
+ if( d_vts_inf[tn].isNull() ){
+ d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" );
+ //mark as a virtual term
+ VirtualTermSkolemAttribute vtsa;
+ d_vts_inf[tn].setAttribute(vtsa,true);
+ }
+ }
+ return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
+}
+
+Node TermUtil::getVtsInfinityIndex( int i, bool isFree, bool create ) {
+ if( i==0 ){
+ return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create );
+ }else if( i==1 ){
+ return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create );
+ }else{
+ Assert( false );
+ return Node::null();
+ }
+}
+
+Node TermUtil::substituteVtsFreeTerms( Node n ) {
+ std::vector< Node > vars;
+ getVtsTerms( vars, false, false );
+ std::vector< Node > vars_free;
+ getVtsTerms( vars_free, true, false );
+ Assert( vars.size()==vars_free.size() );
+ if( !vars.empty() ){
+ return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
+ }else{
+ return n;
+ }
+}
+
+Node TermUtil::rewriteVtsSymbols( Node n ) {
+ if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){
+ Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
+ Node rew_vts_inf;
+ bool rew_delta = false;
+ //rewriting infinity always takes precedence over rewriting delta
+ for( unsigned r=0; r<2; r++ ){
+ Node inf = getVtsInfinityIndex( r, false, false );
+ if( !inf.isNull() && containsTerm( n, inf ) ){
+ if( rew_vts_inf.isNull() ){
+ rew_vts_inf = inf;
+ }else{
+ //for mixed int/real with multiple infinities
+ Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl;
+ std::vector< Node > subs_lhs;
+ subs_lhs.push_back( inf );
+ std::vector< Node > subs_rhs;
+ subs_lhs.push_back( rew_vts_inf );
+ n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+ n = Rewriter::rewrite( n );
+ //may have cancelled
+ if( !containsTerm( n, rew_vts_inf ) ){
+ rew_vts_inf = Node::null();
+ }
+ }
+ }
+ }
+ if( rew_vts_inf.isNull() ){
+ if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
+ rew_delta = true;
+ }
+ }
+ if( !rew_vts_inf.isNull() || rew_delta ){
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( n, msum ) ){
+ if( Trace.isOn("quant-vts-debug") ){
+ Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
+ }
+ Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta;
+ Assert( !vts_sym.isNull() );
+ Node iso_n;
+ Node nlit;
+ int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true );
+ if( res!=0 ){
+ Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl;
+ Node slv = iso_n[res==1 ? 1 : 0];
+ //ensure the vts terms have been eliminated
+ if( containsVtsTerm( slv ) ){
+ Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl;
+ nlit = substituteVtsFreeTerms( n );
+ Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+ //Assert( false );
+ //safe case: just convert to free symbols
+ return nlit;
+ }else{
+ if( !rew_vts_inf.isNull() ){
+ nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false;
+ }else{
+ Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta );
+ if( n.getKind()==EQUAL ){
+ nlit = d_false;
+ }else if( res==1 ){
+ nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
+ }else{
+ nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
+ }
+ }
+ }
+ Trace("quant-vts-debug") << "Return " << nlit << std::endl;
+ return nlit;
+ }else{
+ Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl;
+ //safe case: just convert to free symbols
+ nlit = substituteVtsFreeTerms( n );
+ Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+ //Assert( false );
+ return nlit;
+ }
+ }
+ }
+ return n;
+ }else if( n.getKind()==FORALL ){
+ //cannot traverse beneath quantifiers
+ return substituteVtsFreeTerms( n );
+ }else{
+ bool childChanged = false;
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nn = rewriteVtsSymbols( n[i] );
+ children.push_back( nn );
+ childChanged = childChanged || nn!=n[i];
+ }
+ if( childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ Trace("quant-vts-debug") << "...make node " << ret << std::endl;
+ return ret;
+ }else{
+ return n;
+ }
+ }
+}
+
+bool TermUtil::containsVtsTerm( Node n, bool isFree ) {
+ std::vector< Node > t;
+ getVtsTerms( t, isFree, false );
+ return containsTerms( n, t );
+}
+
+bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) {
+ std::vector< Node > t;
+ getVtsTerms( t, isFree, false );
+ if( !t.empty() ){
+ for( unsigned i=0; i<n.size(); i++ ){
+ if( containsTerms( n[i], t ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool TermUtil::containsVtsInfinity( Node n, bool isFree ) {
+ std::vector< Node > t;
+ getVtsTerms( t, isFree, false, false );
+ return containsTerms( n, t );
+}
+
+Node TermUtil::ensureType( Node n, TypeNode tn ) {
+ TypeNode ntn = n.getType();
+ Assert( ntn.isComparableTo( tn ) );
+ if( ntn.isSubtypeOf( tn ) ){
+ return n;
+ }else{
+ if( tn.isInteger() ){
+ return NodeManager::currentNM()->mkNode( TO_INTEGER, n );
+ }
+ return Node::null();
+ }
+}
+
+void TermUtil::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
+ if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+ // don't worry about relevancy conditions if using shared selectors
+ if( !options::dtSharedSelectors() ){
+ unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());
+ const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
+ Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate();
+ if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){
+ cond.push_back( rc );
+ }
+ getRelevancyCondition( n[0], cond );
+ }
+ }
+}
+
+bool TermUtil::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
+ if( n==t ){
+ return true;
+ }else{
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( containsTerm2( n[i], t, visited ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+}
+
+bool TermUtil::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ if( std::find( t.begin(), t.end(), n )!=t.end() ){
+ return true;
+ }else{
+ visited[n] = true;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( containsTerms2( n[i], t, visited ) ){
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+bool TermUtil::containsTerm( Node n, Node t ) {
+ std::map< Node, bool > visited;
+ return containsTerm2( n, t, visited );
+}
+
+bool TermUtil::containsTerms( Node n, std::vector< Node >& t ) {
+ if( t.empty() ){
+ return false;
+ }else{
+ std::map< Node, bool > visited;
+ return containsTerms2( n, t, visited );
+ }
+}
+
+int TermUtil::getTermDepth( Node n ) {
+ if (!n.hasAttribute(TermDepthAttribute()) ){
+ int maxDepth = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int depth = getTermDepth( n[i] );
+ if( depth>maxDepth ){
+ maxDepth = depth;
+ }
+ }
+ TermDepthAttribute tda;
+ n.setAttribute(tda,1+maxDepth);
+ }
+ return n.getAttribute(TermDepthAttribute());
+}
+
+bool TermUtil::containsUninterpretedConstant( Node n ) {
+ if (!n.hasAttribute(ContainsUConstAttribute()) ){
+ bool ret = false;
+ if( n.getKind()==UNINTERPRETED_CONSTANT ){
+ ret = true;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( containsUninterpretedConstant( n[i] ) ){
+ ret = true;
+ break;
+ }
+ }
+ }
+ ContainsUConstAttribute cuca;
+ n.setAttribute(cuca, ret ? 1 : 0);
+ }
+ return n.getAttribute(ContainsUConstAttribute())!=0;
+}
+
+Node TermUtil::simpleNegate( Node n ){
+ if( n.getKind()==OR || n.getKind()==AND ){
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ children.push_back( simpleNegate( n[i] ) );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children );
+ }else{
+ return n.negate();
+ }
+}
+
+bool TermUtil::isAssoc( Kind k ) {
+ return k==PLUS || k==MULT || k==AND || k==OR ||
+ k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
+ k==STRING_CONCAT;
+}
+
+bool TermUtil::isComm( Kind k ) {
+ return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR ||
+ k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+}
+
+bool TermUtil::isNonAdditive( Kind k ) {
+ return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR;
+}
+
+bool TermUtil::isBoolConnective( Kind k ) {
+ return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
+}
+
+bool TermUtil::isBoolConnectiveTerm( TNode n ) {
+ return isBoolConnective( n.getKind() ) &&
+ ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) &&
+ ( n.getKind()!=ITE || n.getType().isBoolean() );
+}
+
+void TermUtil::registerTrigger( theory::inst::Trigger* tr, Node op ){
+ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
+ d_op_triggers[op].push_back( tr );
+ }
+}
+
+Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) {
+ std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn );
+ if( ithp==d_ho_type_match_pred.end() ){
+ TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
+ Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" );
+ d_ho_type_match_pred[tn] = k;
+ return k;
+ }else{
+ return ithp->second;
+ }
+}
+
+bool TermUtil::isInductionTerm( Node n ) {
+ TypeNode tn = n.getType();
+ if( options::dtStcInduction() && tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ return !dt.isCodatatype();
+ }
+ if( options::intWfInduction() && n.getType().isInteger() ){
+ return true;
+ }
+ return false;
+}
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file term_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief term utilities class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/attribute.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+
+// attribute for "contains instantiation constants from"
+struct InstConstantAttributeId {};
+typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
+
+struct BoundVarAttributeId {};
+typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
+
+struct InstLevelAttributeId {};
+typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+
+struct InstVarNumAttributeId {};
+typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
+
+struct TermDepthAttributeId {};
+typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
+
+struct ContainsUConstAttributeId {};
+typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId {};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+
+//for bounded integers
+struct BoundIntLitAttributeId {};
+typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
+
+//for quantifier instantiation level
+struct QuantInstLevelAttributeId {};
+typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
+
+//rewrite-rule priority
+struct RrPriorityAttributeId {};
+typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
+
+/** Attribute true for quantifiers that do not need to be partially instantiated */
+struct LtePartialInstAttributeId {};
+typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
+
+// attribute for "contains instantiation constants from"
+struct SygusProxyAttributeId {};
+typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
+
+// attribute for associating a synthesis function with a first order variable
+struct SygusSynthFunAttributeId {};
+typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute;
+
+// attribute for associating a variable list with a synth fun
+struct SygusSynthFunVarListAttributeId {};
+typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> SygusSynthFunVarListAttribute;
+
+//attribute for fun-def abstraction type
+struct AbsTypeFunDefAttributeId {};
+typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
+
+/** Attribute for id number */
+struct QuantIdNumAttributeId {};
+typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
+
+/** sygus var num */
+struct SygusVarNumAttributeId {};
+typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
+
+/** Attribute to mark Skolems as virtual terms */
+struct VirtualTermSkolemAttributeId {};
+typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
+
+class QuantifiersEngine;
+
+namespace inst{
+ class Trigger;
+ class HigherOrderTrigger;
+}
+
+namespace quantifiers {
+
+class TermDatabase;
+
+// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
+class TermUtil {
+ // TODO : remove these
+ friend class ::CVC4::theory::QuantifiersEngine;
+ friend class TermDatabase;
+private:
+ /** reference to the quantifiers engine */
+ QuantifiersEngine* d_quantEngine;
+public:
+ TermUtil(QuantifiersEngine * qe);
+ ~TermUtil();
+ /** boolean terms */
+ Node d_true;
+ Node d_false;
+ /** constants */
+ Node d_zero;
+ Node d_one;
+
+ /** register quantifier */
+ void registerQuantifier( Node q );
+
+//for inst constant
+private:
+ /** map from universal quantifiers to the list of variables */
+ std::map< Node, std::vector< Node > > d_vars;
+ std::map< Node, std::map< Node, unsigned > > d_var_num;
+ /** map from universal quantifiers to their inst constant body */
+ std::map< Node, Node > d_inst_const_body;
+ /** map from universal quantifiers to their counterexample literals */
+ std::map< Node, Node > d_ce_lit;
+ /** instantiation constants to universal quantifiers */
+ std::map< Node, Node > d_inst_constants_map;
+public:
+ /** map from universal quantifiers to the list of instantiation constants */
+ std::map< Node, std::vector< Node > > d_inst_constants;
+ /** get variable number */
+ unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
+ /** get the i^th instantiation constant of q */
+ Node getInstantiationConstant( Node q, int i ) const;
+ /** get number of instantiation constants for q */
+ unsigned getNumInstantiationConstants( Node q ) const;
+ /** get the ce body q[e/x] */
+ Node getInstConstantBody( Node q );
+ /** get counterexample literal (for cbqi) */
+ Node getCounterexampleLiteral( Node q );
+ /** returns node n with bound vars of q replaced by instantiation constants of q
+ node n : is the future pattern
+ node q : is the quantifier containing which bind the variable
+ return a pattern where the variable are replaced by variable for
+ instantiation.
+ */
+ Node getInstConstantNode( Node n, Node q );
+ Node getVariableNode( Node n, Node q );
+ /** get substituted node */
+ Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
+
+ static Node getInstConstAttr( Node n );
+ static bool hasInstConstAttr( Node n );
+ static Node getBoundVarAttr( Node n );
+ static bool hasBoundVarAttr( Node n );
+
+private:
+ /** get bound vars */
+ static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
+ /** get bound vars */
+ static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited );
+public:
+ //get the bound variables in this node
+ static void getBoundVars( Node n, std::vector< Node >& vars );
+ //remove quantifiers
+ static Node getRemoveQuantifiers( Node n );
+ //quantified simplify (treat free variables in n as quantified and run rewriter)
+ static Node getQuantSimplify( Node n );
+
+//for skolem
+private:
+ /** map from universal quantifiers to their skolemized body */
+ std::map< Node, Node > d_skolem_body;
+public:
+ /** map from universal quantifiers to the list of skolem constants */
+ std::map< Node, std::vector< Node > > d_skolem_constants;
+ /** make the skolemized body f[e/x] */
+ static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
+ 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;
+ // closed enumerable type cache
+ std::map< TypeNode, bool > d_typ_closed_enum;
+ /** may complete */
+ std::map< TypeNode, bool > d_may_complete;
+public:
+ //get nth term for type
+ Node getEnumerateTerm( TypeNode tn, unsigned index );
+ //does this type have an enumerator that produces constants that are handled by ground theory solvers
+ bool isClosedEnumerableType( TypeNode tn );
+ // may complete
+ bool mayComplete( TypeNode tn );
+
+//for triggers
+private:
+ /** helper function for compute var contains */
+ static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
+ /** triggers for each operator */
+ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
+ /** helper for is instance of */
+ static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
+ /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+ static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
+public:
+ /** compute var contains */
+ static void computeVarContains( Node n, std::vector< Node >& varContains );
+ /** get var contains for each of the patterns in pats */
+ static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
+ /** get var contains for node n */
+ static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+ /** compute quant contains */
+ static void computeQuantContains( Node n, std::vector< Node >& quantContains );
+ /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+ static int isInstanceOf( Node n1, Node n2 );
+ /** filter all nodes that have instances */
+ static void filterInstances( std::vector< Node >& nodes );
+ /** register trigger (for eager quantifier instantiation) */
+ void registerTrigger( inst::Trigger* tr, Node op );
+
+//for term ordering
+private:
+ /** operator id count */
+ int d_op_id_count;
+ /** map from operators to id */
+ std::map< Node, int > d_op_id;
+ /** type id count */
+ int d_typ_id_count;
+ /** map from type to id */
+ std::map< TypeNode, int > d_typ_id;
+ //free variables
+ std::map< TypeNode, std::vector< Node > > d_cn_free_var;
+ // get canonical term, return null if it contains a term apart from handled signature
+ Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder,
+ std::map< TNode, Node >& visited );
+public:
+ /** get id for operator */
+ int getIdForOperator( Node op );
+ /** get id for type */
+ int getIdForType( TypeNode t );
+ /** get term order */
+ bool getTermOrder( Node a, Node b );
+ /** get canonical free variable #i of type tn */
+ Node getCanonicalFreeVar( TypeNode tn, unsigned i );
+ /** get canonical term */
+ Node getCanonicalTerm( TNode n, bool apply_torder = false );
+
+//for virtual term substitution
+private:
+ Node d_vts_delta;
+ std::map< TypeNode, Node > d_vts_inf;
+ Node d_vts_delta_free;
+ std::map< TypeNode, Node > d_vts_inf_free;
+ /** get vts infinity index */
+ Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true );
+ /** substitute vts free terms */
+ Node substituteVtsFreeTerms( Node n );
+public:
+ /** get vts delta */
+ Node getVtsDelta( bool isFree = false, bool create = true );
+ /** get vts infinity */
+ Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true );
+ /** get all vts terms */
+ void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true );
+ /** rewrite delta */
+ Node rewriteVtsSymbols( Node n );
+ /** simple check for contains term */
+ bool containsVtsTerm( Node n, bool isFree = false );
+ /** simple check for contains term */
+ bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
+ /** simple check for contains term */
+ bool containsVtsInfinity( Node n, bool isFree = false );
+ /** ensure type */
+ static Node ensureType( Node n, TypeNode tn );
+ /** get relevancy condition */
+ static void getRelevancyCondition( Node n, std::vector< Node >& cond );
+
+//general utilities
+private:
+ //helper for contains term
+ static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
+ static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
+public:
+ /** simple check for whether n contains t as subterm */
+ static bool containsTerm( Node n, Node t );
+ /** simple check for contains term, true if contains at least one term in t */
+ static bool containsTerms( Node n, std::vector< Node >& t );
+ /** contains uninterpreted constant */
+ static bool containsUninterpretedConstant( Node n );
+ /** get the term depth of n */
+ static int getTermDepth( Node n );
+ /** simple negate */
+ static Node simpleNegate( Node n );
+ /** is assoc */
+ static bool isAssoc( Kind k );
+ /** is comm */
+ static bool isComm( Kind k );
+ /** ( x k ... ) k x = ( x k ... ) */
+ static bool isNonAdditive( Kind k );
+ /** is bool connective */
+ static bool isBoolConnective( Kind k );
+ /** is bool connective term */
+ static bool isBoolConnectiveTerm( TNode n );
+
+//for higher-order
+private:
+ /** dummy predicate that states terms should be considered first-class members of equality engine */
+ std::map< TypeNode, Node > d_ho_type_match_pred;
+public:
+ /** get higher-order type match predicate
+ * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the
+ * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh
+ * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma.
+ * TODO: we may eliminate this depending on how github issue #1115 is resolved.
+ */
+ Node getHoTypeMatchPredicate( TypeNode tn );
+};/* class TermUtil */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/valuation.h"
void TheoryQuantifiers::preRegisterTerm(TNode n) {
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
if( n.getKind()==FORALL ){
- if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+ if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
getQuantifiersEngine()->registerQuantifier( n );
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
}
void TheoryQuantifiers::assertUniversal( Node n ){
Assert( n.getKind()==FORALL );
- if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+ if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
getQuantifiersEngine()->assertQuantifier( n, true );
}
}
void TheoryQuantifiers::assertExistential( Node n ){
Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
- if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
+ if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){
getQuantifiersEngine()->assertQuantifier( n[0], false );
}
}
void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
- QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
+ QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
}
#include "theory/quantifiers/candidate_generator.h"
#include "theory/quantifiers/inst_match_generator.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
if( d_fv.empty() ){
- quantifiers::TermDb::getVarContainsNode( q, n, d_fv );
+ quantifiers::TermUtil::getVarContainsNode( q, n, d_fv );
}
if( d_reqPol==0 ){
d_reqPol = reqPol;
std::map< Node, std::vector< Node > > patterns;
size_t varCount = 0;
std::map< Node, std::vector< Node > > varContains;
- quantifiers::TermDb::getVarContains( q, temp, varContains );
+ quantifiers::TermUtil::getVarContains( q, temp, varContains );
for( unsigned i=0; i<temp.size(); i++ ){
bool foundVar = false;
for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
Node v = varContains[ temp[i] ][j];
- Assert( quantifiers::TermDb::getInstConstAttr(v)==q );
+ Assert( quantifiers::TermUtil::getInstConstAttr(v)==q );
if( vars.find( v )==vars.end() ){
varCount++;
vars[ v ] = true;
}
bool Trigger::isUsable( Node n, Node q ){
- if( quantifiers::TermDb::getInstConstAttr(n)==q ){
+ if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
if( isAtomicTrigger( n ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !isUsable( n[i], q ) ){
Assert( isRelationalTrigger( n ) );
for( unsigned i=0; i<2; i++) {
if( isUsableEqTerms( q, n[i], n[1-i] ) ){
- if( i==1 && n.getKind()==EQUAL && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
+ if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
}else{
return n;
bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
if( n1.getKind()==INST_CONSTANT ){
if( options::relationalTriggers() ){
- if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
return true;
}else if( n2.getKind()==INST_CONSTANT ){
return true;
}
}
}else if( isUsableAtomicTrigger( n1, q ) ){
- if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){
+ if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermUtil::containsTerm( n1, n2 ) ){
return true;
- }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+ }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
return true;
}
}
return rtr2;
}
}else{
- Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
+ Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
if( isUsableAtomicTrigger( n, q ) ){
return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
}
}
bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
- return quantifiers::TermDb::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
+ return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
}
bool Trigger::isUsableTrigger( Node n, Node q ){
}
bool Trigger::isCbqiKind( Kind k ) {
- if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
+ if( quantifiers::TermUtil::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
return true;
}else{
//CBQI typically works for satisfaction-complete theories
bool Trigger::isSimpleTrigger( Node n ){
Node t = n.getKind()==NOT ? n[0] : n;
if( t.getKind()==EQUAL ){
- if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){
+ if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){
t = t[0];
}
}
if( isAtomicTrigger( t ) ){
for( unsigned i=0; i<t.getNumChildren(); i++ ){
- if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(t[i]) ){
+ if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
return false;
}
}
Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
Node reqEq;
if( nu.getKind()==EQUAL ){
- if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
+ if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
if( hasPol ){
reqEq = nu[1];
}
nu = nu[0];
}
}
- Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
+ Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) );
Assert( isUsableTrigger( nu, q ) );
//tinfo.find( nu )==tinfo.end()
Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
}
bool Trigger::isPureTheoryTrigger( Node n ) {
- if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermDb::hasInstConstAttr( n ) ){
+ if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
return false;
}else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( options::relationalTriggers() ){
if( isRelationalTrigger( n ) ){
for( unsigned i=0; i<2; i++ ){
- if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){
+ if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
return 0;
}
}
collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
std::vector< Node > temp;
temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
- quantifiers::TermDb::filterInstances( temp );
+ quantifiers::TermUtil::filterInstances( temp );
if( temp.size()!=patTerms2.size() ){
Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
Trace("trigger-filter-instance") << "Old: ";
}else if( n.getKind()==PLUS || n.getKind()==MULT ){
Node ret;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
if( ret.isNull() ){
ret = getInversionVariable( n[i] );
if( ret.isNull() ){
}else if( n.getKind()==PLUS || n.getKind()==MULT ){
int cindex = -1;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
if( n.getKind()==PLUS ){
x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
}else if( n.getKind()==MULT ){
collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo );
//collect all variables from all patterns in patTerms, add to t_vars
for( unsigned i=0; i<patTerms.size(); i++ ){
- quantifiers::TermDb::getVarContainsNode( q, patTerms[i], t_vars );
+ quantifiers::TermUtil::getVarContainsNode( q, patTerms[i], t_vars );
}
}
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/ceg_t_instantiator.h"
#include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/fun_def_engine.h"
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/local_theory_ext.h"
#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_equality_engine.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/anti_skolem.h"
d_presolve_cache_wq(u),
d_presolve_cache_wic(u){
//utilities
- d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
+ d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
d_util.push_back( d_eq_query );
d_term_db = new quantifiers::TermDb( c, u, this );
d_util.push_back( d_term_db );
+
+ d_term_util = new quantifiers::TermUtil( this );
+
+ if (options::ceGuidedInst()) {
+ d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
+ }else{
+ d_sygus_tdb = NULL;
+ }
+
+ d_quant_attr = new quantifiers::QuantAttributes( this );
if( options::instPropagate() ){
// notice that this option is incompatible with options::qcfAllConflict()
}else{
d_inst_prop = NULL;
}
+
+ if( options::inferArithTriggerEq() ){
+ d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
+ }else{
+ d_eq_inference = NULL;
+ }
d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QEFFORT_NONE;
d_hasAddedLemma = false;
d_useModelEe = false;
//don't add true lemma
- d_lemmas_produced_c[d_term_db->d_true] = true;
+ d_lemmas_produced_c[d_term_util->d_true] = true;
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
delete d_model;
delete d_tr_trie;
delete d_term_db;
+ delete d_sygus_tdb;
+ delete d_term_util;
+ delete d_eq_inference;
delete d_eq_query;
delete d_sg_gen;
delete d_ceg_inst;
delete d_inst_prop;
}
-EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
+EqualityQuery* QuantifiersEngine::getEqualityQuery() {
return d_eq_query;
}
TypeNode tn = v.getType();
if( tn.isSort() && options::finiteModelFind() ){
return true;
- }else if( getTermDatabase()->mayComplete( tn ) ){
+ }else if( getTermUtil()->mayComplete( tn ) ){
return true;
}
}
d_quants[f] = false;
return false;
}else{
- //make instantiation constants for f
- d_term_db->makeInstantiationConstantsFor( f );
- d_term_db->computeAttributes( f );
+ // register with utilities : TODO (#1163) make this a standard call
+
+ d_term_util->registerQuantifier( f );
+ d_term_db->registerQuantifier( f );
+ d_quant_attr->computeAttributes( f );
+ //register with quantifier relevance
+ if( d_quant_rel ){
+ d_quant_rel->registerQuantifier( f );
+ }
+
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->preRegisterQuantifier( f );
if( qm!=NULL ){
Trace("quant") << " Owner : " << qm->identify() << std::endl;
}
- //register with quantifier relevance
- if( d_quant_rel ){
- d_quant_rel->registerQuantifier( f );
- }
//register with each module
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->registerQuantifier( f );
}
//TODO: remove this
- Node ceBody = d_term_db->getInstConstantBody( f );
+ Node ceBody = d_term_util->getInstConstantBody( f );
//also register it with the strong solver
//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
if( !reduceQuantifier( f ) ){
//do skolemization
if( d_skolemized.find( f )==d_skolemized.end() ){
- Node body = d_term_db->getSkolemizedBody( f );
+ Node body = d_term_util->getSkolemizedBody( f );
NodeBuilder<> nb(kind::OR);
nb << f << body.notNode();
Node lem = nb;
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->assertNode( f );
}
- addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
+ addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
}
}
}
return dec;
}
-quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
- return getTermDatabase()->getTermDatabaseSygus();
-}
-
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
if( options::incrementalSolving() ){
if( d_presolve_in.find( n )==d_presolve_in.end() ){
void QuantifiersEngine::eqNotifyNewClass(TNode t) {
addTermToDatabase( t );
- if( d_eq_query->getEqualityInference() ){
- d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
+ if( d_eq_inference ){
+ d_eq_inference->eqNotifyNewClass( t );
}
}
void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
- if( d_eq_query->getEqualityInference() ){
- d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
+ if( d_eq_inference ){
+ d_eq_inference->eqNotifyMerge( t1, t2 );
}
}
Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
ret = terms[n.getAttribute(InstVarNumAttribute())];
}else{
- //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+ //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){
//Debug("check-inst") << "No inst const attr : " << n << std::endl;
//return n;
//}else{
body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
}else{
//do optimized version
- Node icb = d_term_db->getInstConstantBody( q );
+ Node icb = d_term_util->getInstConstantBody( q );
std::map< Node, Node > visited;
body = getSubstitute( icb, terms, visited );
if( Debug.isOn("check-inst") ){
//do virtual term substitution
body = Rewriter::rewrite( body );
Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
- Node body_r = d_term_db->rewriteVtsSymbols( body );
+ Node body_r = d_term_util->rewriteVtsSymbols( body );
Trace("quant-vts-debug") << " ...result: " << body_r << std::endl;
body = body_r;
}
}
Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
- Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
- return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
+ Assert( d_term_util->d_vars.find( q )!=d_term_util->d_vars.end() );
+ return getInstantiation( q, d_term_util->d_vars[q], terms, doVts );
}
/*
terms[i] = getInternalRepresentative( terms[i], q, i );
}else{
//ensure the type is correct
- terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
+ terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() );
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if( terms[i].isNull() ){
}else{
//get relevancy conditions
if( options::instRelevantCond() ){
- quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
+ quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond );
}
}
#ifdef CVC4_ASSERTIONS
bool bad_inst = false;
- if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+ if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){
Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
bad_inst = true;
}else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
bad_inst = true;
}else if( options::cbqi() ){
- Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
+ Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
if( !icf.isNull() ){
if( icf==q ){
Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
bad_inst = true;
- }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
+ }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){
Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
bad_inst = true;
}
//construct the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- Assert( d_term_db->d_vars[q].size()==terms.size() );
- Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution
+ Assert( d_term_util->d_vars[q].size()==terms.size() );
+ Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution
Node orig_body = body;
if( options::cbqiNestedQE() && d_i_cbqi ){
body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
if( d_useModelEe && options::instNoModelTrue() ){
Node val_body = d_model->getValue( body );
- if( val_body==d_term_db->d_true ){
+ if( val_body==d_term_util->d_true ){
Trace("inst-add-debug") << " --> True in model." << std::endl;
++(d_statistics.d_inst_duplicate_model_true);
return false;
printed = true;
out << "(skolem " << q << std::endl;
out << " ( ";
- for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){
+ for( unsigned i=0; i<d_term_util->d_skolem_constants[q].size(); i++ ){
if( i>0 ){ out << " "; }
- out << d_term_db->d_skolem_constants[q][i];
+ out << d_term_util->d_skolem_constants[q][i];
}
out << " )" << std::endl;
out << ")" << std::endl;
}
//have to remove q, TODO: avoid this in a better way
TNode tq = q;
- TNode tt = d_term_db->d_true;
+ TNode tt = d_term_util->d_true;
ret = ret.substitute( tq, tt );
return ret;
}
}
}
-
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
- if( options::inferArithTriggerEq() ){
- d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
- }else{
- d_eq_inference = NULL;
- }
-}
-
-EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
- delete d_eq_inference;
-}
-
-bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
- d_int_rep.clear();
- d_reset_count++;
- return processInferences( e );
-}
-
-bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
- if( options::inferArithTriggerEq() ){
- eq::EqualityEngine* ee = getEngine();
- //updated implementation
- while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
- Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
- Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() );
- Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
- Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl;
- Assert( ee->hasTerm( eq[0] ) );
- Assert( ee->hasTerm( eq[1] ) );
- if( areDisequal( eq[0], eq[1] ) ){
- Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
- if( Trace.isOn("term-db-lemma") ){
- Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
- if( !d_qe->getTheoryEngine()->needCheck() ){
- Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
- //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
- Assert( false );
- }
- Trace("term-db-lemma") << " add split on : " << eq << std::endl;
- }
- d_qe->addSplit( eq );
- return false;
- }else{
- ee->assertEquality( eq, true, eq_exp );
- d_eqi_counter = d_eqi_counter.get() + 1;
- }
- }
- Assert( ee->consistent() );
- }
- return true;
-}
-
-bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
- return getEngine()->hasTerm( a );
-}
-
-Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- return ee->getRepresentative( a );
- }else{
- return a;
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areEqual( a, b );
- }else{
- return false;
- }
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areDisequal( a, b, false );
- }else{
- return a.isConst() && b.isConst();
- }
- }
-}
-
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
- Assert( f.isNull() || f.getKind()==FORALL );
- Node r = getRepresentative( a );
- if( options::finiteModelFind() ){
- if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){
- //map back from values assigned by model, if any
- if( d_qe->getModel() ){
- std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
- if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
- r = it->second;
- r = getRepresentative( r );
- }else{
- if( r.getType().isSort() ){
- Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
- //should never happen : UF constants should never escape model
- Assert( false );
- }
- }
- }
- }
- }
- if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
- return r;
- }else{
- TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
- std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
- if( itir==d_int_rep[v_tn].end() ){
- //find best selection for representative
- Node r_best;
- //if( options::fmfRelevantDomain() && !f.isNull() ){
- // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
- // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
- // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
- //}
- std::vector< Node > eqc;
- getEquivalenceClass( r, eqc );
- Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
- for( unsigned i=0; i<eqc.size(); i++ ){
- if( i>0 ) Trace("internal-rep-select") << ", ";
- Trace("internal-rep-select") << eqc[i];
- }
- Trace("internal-rep-select") << " }, type = " << v_tn << std::endl;
- int r_best_score = -1;
- for( size_t i=0; i<eqc.size(); i++ ){
- int score = getRepScore( eqc[i], f, index, v_tn );
- if( score!=-2 ){
- if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
- r_best = eqc[i];
- r_best_score = score;
- }
- }
- }
- if( r_best.isNull() ){
- Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
- r_best = r;
- }
- //now, make sure that no other member of the class is an instance
- std::unordered_map<TNode, Node, TNodeHashFunction> cache;
- r_best = getInstance( r_best, eqc, cache );
- //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 << " with score " << r_best_score << std::endl;
- Assert( r_best.getType().isSubtypeOf( v_tn ) );
- d_int_rep[v_tn][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;
- }
- return r_best;
- }else{
- return itir->second;
- }
- }
-}
-
-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< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : 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< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.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( itt->second.find( r )==itt->second.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;
- itt->second[it->first] = ni[j];
- changed = false;
- success = true;
- break;
- }else{
- Node ir = itt->second[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;
- itt->second[it->first] = n;
- temp_rep_map[n] = it->first;
- }
- }
- }
- }
- }while( success );
- Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
- }
- }
-}
-
-eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
- return d_qe->getActiveEqualityEngine();
-}
-
-void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- Node rep = ee->getRepresentative( a );
- eq::EqClassIterator eqc_iter( rep, ee );
- while( !eqc_iter.isFinished() ){
- eqc.push_back( *eqc_iter );
- eqc_iter++;
- }
- }else{
- eqc.push_back( a );
- }
- //a should be in its equivalence class
- Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
-}
-
-TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
- return d_qe->getTermDatabase()->getCongruentTerm( f, args );
-}
-
-//helper functions
-
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
- if(cache.find(n) != cache.end()) {
- return cache[n];
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- Node nn = getInstance( n[i], eqc, cache );
- if( !nn.isNull() ){
- return cache[n] = nn;
- }
- }
- if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
- return cache[n] = n;
- }else{
- return cache[n] = Node::null();
- }
-}
-
-//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
- if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject
- return -2;
- }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
- return -2;
- }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
- return -1;
- }else if( options::instMaxLevel()!=-1 ){
- //score prefer lowest instantiation level
- if( n.hasAttribute(InstLevelAttribute()) ){
- return n.getAttribute(InstLevelAttribute());
- }else{
- return options::instLevelInputOnly() ? -1 : 0;
- }
- }else{
- if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
- //score prefers earliest use of this term as a representative
- return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
- }else{
- Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
- return quantifiers::TermDb::getTermDepth( n );
- }
- }
-}
//utilities
class TermDb;
class TermDbSygus;
+ class TermUtil;
class FirstOrderModel;
+ class QuantAttributes;
class RelevantDomain;
class BvInverter;
class InstPropagator;
+ class EqualityInference;
+ class EqualityQueryQuantifiersEngine;
//modules, these are "subsolvers" of the quantifiers theory.
class InstantiationEngine;
class ModelEngine;
class TriggerTrie;
}/* CVC4::theory::inst */
-//class EfficientEMatcher;
-class EqualityQueryQuantifiersEngine;
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
/** instantiation notify */
std::vector< InstantiationNotify* > d_inst_notify;
/** equality query class */
- EqualityQueryQuantifiersEngine* d_eq_query;
+ quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
+ /** equality inference class */
+ quantifiers::EqualityInference* d_eq_inference;
/** for computing relevance of quantifiers */
QuantRelevance * d_quant_rel;
/** relevant domain */
BoolMap d_skolemized;
/** term database */
quantifiers::TermDb* d_term_db;
+ /** term database */
+ quantifiers::TermDbSygus* d_sygus_tdb;
+ /** term utilities */
+ quantifiers::TermUtil* d_term_util;
+ /** quantifiers attributes */
+ quantifiers::QuantAttributes* d_quant_attr;
/** all triggers will be stored in this trie */
inst::TriggerTrie* d_tr_trie;
/** extended model object */
/** get theory engine */
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query */
- EqualityQueryQuantifiersEngine* getEqualityQuery();
+ EqualityQuery* getEqualityQuery();
+ /** get the equality inference */
+ quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; }
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
/** get default sat context for quantifiers engine */
/** get term database */
quantifiers::TermDb* getTermDatabase() { return d_term_db; }
/** get term database sygus */
- quantifiers::TermDbSygus* getTermDatabaseSygus();
+ quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
+ /** get term utilities */
+ quantifiers::TermUtil* getTermUtil() { return d_term_util; }
+ /** get quantifiers attributes */
+ quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr; }
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
Statistics d_statistics;
};/* class QuantifiersEngine */
-
-
-/** equality query object using theory engine */
-class EqualityQueryQuantifiersEngine : public EqualityQuery
-{
-private:
- /** pointer to theory engine */
- QuantifiersEngine* d_qe;
- /** quantifiers equality inference */
- quantifiers::EqualityInference * d_eq_inference;
- context::CDO< unsigned > d_eqi_counter;
- /** internal representatives */
- std::map< TypeNode, std::map< Node, Node > > d_int_rep;
- /** rep score */
- std::map< Node, int > d_rep_score;
- /** reset count */
- int d_reset_count;
-
- /** processInferences : will merge equivalence classes in master equality engine, if possible */
- bool processInferences( Theory::Effort e );
- /** node contains */
- Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
- /** get score */
- int getRepScore( Node n, Node f, int index, TypeNode v_tn );
- /** flatten representatives */
- void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-public:
- EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
- virtual ~EqualityQueryQuantifiersEngine();
- /** reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "EqualityQueryQE"; }
- /** general queries about equality */
- bool hasTerm( Node a );
- Node getRepresentative( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- eq::EqualityEngine* getEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
- /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
- If cbqi is active, this will return a term in the equivalence class of "a" that does
- not contain instantiation constants, if such a term exists.
- */
- Node getInternalRepresentative( Node a, Node f, int index );
- /** get quantifiers equality inference */
- quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
-}; /* EqualityQueryQuantifiersEngine */
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
#include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/first_order_model.h"
using namespace std;
// terms in rep_set are now constants which mapped to terms through TheoryModel
// thus, should introduce a constant and a term. for now, just a term.
- //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
+ //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
Node var = d_qe->getModel()->getSomeDomainElement( tn );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( tn, var );
}
if( !tn.isSort() ){
if( inc ){
- if( d_qe->getTermDatabase()->mayComplete( tn ) ){
+ if( d_qe->getTermUtil()->mayComplete( tn ) ){
Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
d_rep_set->complete( tn );
//must have succeeded
for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl;
- varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) );
+ varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) );
}
for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
#include "smt/logic_exception.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "options/quantifiers_options.h"
using namespace std;
if( getLogicInfo().isQuantified() ){
Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() );
Node a = d_guard_to_assertion[g];
- Node q = quantifiers::TermDb::getInstConstAttr( a );
+ Node q = quantifiers::TermUtil::getInstConstAttr( a );
if( !q.isNull() ){
//must wait to decide on counterexample literal from quantified formula
- Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q );
+ Node cel = getQuantifiersEngine()->getTermUtil()->getCounterexampleLiteral( q );
bool value;
if( d_valuation.hasSatValue( cel, value ) ){
Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl;
TypeNode tn1 = n[0].getType();
TypeNode tn2 = n[1].getType();
registerRefDataTypes( tn1, tn2, n );
- if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
+ if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){
if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
// still valid : bound on heap models will include Herbrand universe of n[0].getType()
#include "expr/attribute.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
* Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not.
*/
static inline bool canUseAsApplyUfOperator(TNode n){
- return n.isVar() && n.getKind()!=kind::BOUND_VARIABLE;
+ return n.isVar();
}
};/* class TheoryUfRewriter */
projects / cvc5.git / commitdiff