}
}
-Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) {
+Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException) {
SmtScope smts(this);
+ if(!d_logic.isPure(THEORY_ARITH)){
+ Warning() << "Unexpected logic for quantifier elimination." << endl;
+ }
Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
- Result r = query(e);
+ Node n_e = Node::fromExpr( e );
+ if( n_e.getKind()!=kind::EXISTS ){
+ throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
+ }
+ //tag the quantified formula with the quant-elim attribute
+ TypeNode t = NodeManager::currentNM()->booleanType();
+ Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
+ std::vector< Node > node_values;
+ d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+ n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
+ n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
+ std::vector< Node > e_children;
+ e_children.push_back( n_e[0] );
+ e_children.push_back( n_e[1] );
+ e_children.push_back( n_attr );
+ Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
+ Trace("smt-qe-debug") << "Query : " << nn_e << std::endl;
+ Assert( nn_e.getNumChildren()==3 );
+ Result r = query(nn_e.toExpr());
Trace("smt-qe") << "Query returned " << r << std::endl;
- if(r.asSatisfiabilityResult().isSat() == Result::SAT) {
- Node input = Node::fromExpr( e );
- input = Rewriter::rewrite( input );
- Trace("smt-qe") << "Replace instances in rewritten input: " << input << std::endl;
+ if(r.asSatisfiabilityResult().isSat() == Result::SAT || ( !doFull && r.asSatisfiabilityResult().isSat() != Result::UNSAT ) ) {
+ //get the instantiations for all quantified formulas
std::map< Node, std::vector< Node > > insts;
d_theoryEngine->getInstantiations( insts );
+ //find the quantified formula that corresponds to the input
+ Node top_q;
+ for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
+ Trace("smt-qe-debug") << "* quantifier " << it->first << " had " << it->second.size() << " instances." << std::endl;
+ if( it->first.getNumChildren()==3 && it->first[2]==n_attr ){
+ top_q = it->first;
+ }
+ }
std::map< Node, Node > visited;
- Node en = d_private->replaceQuantifiersWithInstantiations( input, insts, visited );
+ Node ret_n;
+ if( top_q.isNull() ){
+ //no instances needed
+ ret_n = NodeManager::currentNM()->mkConst(true);
+ visited[top_q] = ret_n;
+ }else{
+ //replace by a conjunction of instances
+ ret_n = d_private->replaceQuantifiersWithInstantiations( top_q, insts, visited );
+ }
//ensure all instantiations were accounted for
for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
if( visited.find( it->first )==visited.end() ){
stringstream ss;
ss << "While performing quantifier elimination, processed a quantified formula : " << it->first;
- ss << " that was not related to the query. Try option --simplification=none." << std::endl;
+ ss << " that was not related to the query. Try option --simplification=none.";
InternalError(ss.str().c_str());
}
}
- Trace("smt-qe") << "Returned : " << en << std::endl;
- en = Rewriter::rewrite( en );
- return en.toExpr();
- }else{
- return NodeManager::currentNM()->mkConst(false).toExpr();
+ Trace("smt-qe") << "Returned : " << ret_n << std::endl;
+ ret_n = Rewriter::rewrite( ret_n.negate() );
+ return ret_n.toExpr();
+ }else {
+ if(r.asSatisfiabilityResult().isSat() != Result::UNSAT){
+ stringstream ss;
+ ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
+ InternalError(ss.str().c_str());
+ }
+ return NodeManager::currentNM()->mkConst(true).toExpr();
}
}
/**
* Do quantifier elimination, doFull false means just output one disjunct
*/
- Expr doQuantifierElimination(const Expr& e, bool doFull);
+ Expr doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException);
/**
* Get an unsatisfiable core (only if immediately preceded by an
}
}
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const {
+void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const {
if( terms.size()==q[0].getNumChildren() ){
- insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+ //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+ insts.push_back( qe->getInstantiation( q, terms, true ) );
}else{
for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
terms.push_back( it->first );
- it->second.getInstantiations( insts, q, vars, terms );
+ it->second.getInstantiations( insts, q, terms, qe );
terms.pop_back();
}
}
}
}
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{
+void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const{
if( d_valid.get() ){
if( terms.size()==q[0].getNumChildren() ){
- insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+ //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+ insts.push_back( qe->getInstantiation( q, terms, true ) );
}else{
for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
terms.push_back( it->first );
- it->second->getInstantiations( insts, q, vars, terms );
+ it->second->getInstantiations( insts, q, terms, qe );
terms.pop_back();
}
}
std::map< Node, InstMatchTrie > d_data;
private:
void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
- void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const;
+ void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
public:
InstMatchTrie(){}
~InstMatchTrie(){}
std::vector< TNode > terms;
print( out, q, terms );
}
- void getInstantiations( std::vector< Node >& insts, Node q ) {
- std::vector< TNode > terms;
- std::vector< TNode > vars;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- vars.push_back( q[0][i] );
- }
- getInstantiations( insts, q, vars, terms );
+ void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+ std::vector< Node > terms;
+ getInstantiations( insts, q, terms, qe );
}
void clear() { d_data.clear(); }
};/* class InstMatchTrie */
context::CDO< bool > d_valid;
private:
void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
- void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const;
+ void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
public:
CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
~CDInstMatchTrie(){}
std::vector< TNode > terms;
print( out, q, terms );
}
- void getInstantiations( std::vector< Node >& insts, Node q ) {
- std::vector< TNode > terms;
- std::vector< TNode > vars;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- vars.push_back( q[0][i] );
- }
- getInstantiations( insts, q, vars, terms );
+ void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+ std::vector< Node > terms;
+ getInstantiations( insts, q, terms, qe );
}
};/* class CDInstMatchTrie */
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
- : QuantifiersModule( qe )
- , d_added_cbqi_lemma( qe->getUserContext() ){
+ : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) {
}
InstStrategyCbqi::~InstStrategyCbqi() throw(){}
}else{
Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
}
+ //if doing partial quantifier elimination, do not process this if already processed once
+ if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){
+ if( d_added_inst.find( q )!=d_added_inst.end() ){
+ d_quantEngine->getModel()->setQuantifierActive( q, false );
+ d_cbqi_set_quant_inactive = true;
+ d_incomplete_check = true;
+ }
+ }
}
}
}
std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
if( it==d_do_cbqi.end() ){
bool ret = false;
- //if has an instantiation pattern, don't do it
- if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
- ret = false;
+ if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
+ ret = true;
}else{
- if( options::cbqiAll() ){
- ret = true;
+ //if has an instantiation pattern, don't do it
+ if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
+ ret = false;
}else{
- //if quantifier has a non-arithmetic variable, then do not use cbqi
- //if quantifier has an APPLY_UF term, then do not use cbqi
- Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
- std::map< Node, bool > visited;
- ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+ if( options::cbqiAll() ){
+ ret = true;
+ }else{
+ //if quantifier has a non-arithmetic variable, then do not use cbqi
+ //if quantifier has an APPLY_UF term, then do not use cbqi
+ Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+ std::map< Node, bool > visited;
+ ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+ }
}
}
+ Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
d_do_cbqi[q] = ret;
return ret;
}else{
Assert( !d_curr_quant.isNull() );
//check if we need virtual term substitution (if used delta or infinity)
bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
- return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts );
+ if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+ d_added_inst.insert( d_curr_quant );
+ return true;
+ }else{
+ return false;
+ }
}
bool InstStrategyCegqi::addLemma( Node lem ) {
bool d_incomplete_check;
/** whether we have added cbqi lemma */
NodeSet d_added_cbqi_lemma;
+ /** whether we have instantiated quantified formulas */
+ NodeSet d_added_inst;
/** whether to do cbqi for this quantified formula */
std::map< Node, bool > d_do_cbqi;
/** register ce lemma */
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 ){
+void QuantifiersAttributes::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;
Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
RrPriorityAttribute rrpa;
n.setAttribute( rrpa, lvl );
+ }else if( attr=="quant-elim" ){
+ Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
+ QuantElimAttribute qea;
+ n.setAttribute( qea, true );
+ }else if( attr=="quant-elim-partial" ){
+ Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
+ QuantElimPartialAttribute qepa;
+ n.setAttribute( qepa, true );
}
}
* 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 );
+ static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
};
RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
- if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
- RewriteStatus status = REWRITE_DONE;
- Node ret = in;
- //get the arguments
- std::vector< Node > args;
- for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
- args.push_back( in[0][i] );
- }
- //get the instantiation pattern list
- Node ipl;
+ RewriteStatus status = REWRITE_DONE;
+ Node ret = in;
+ //get the body
+ if( in.getKind()==EXISTS ){
+ std::vector< Node > children;
+ children.push_back( in[0] );
+ children.push_back( in[1].negate() );
if( in.getNumChildren()==3 ){
- ipl = in[2];
- }
- //get the body
- if( in.getKind()==EXISTS ){
- std::vector< Node > children;
- children.push_back( in[0] );
- children.push_back( in[1].negate() );
- if( in.getNumChildren()==3 ){
- children.push_back( in[2] );
- }
- ret = NodeManager::currentNM()->mkNode( FORALL, children );
- ret = ret.negate();
- status = REWRITE_AGAIN_FULL;
- }else{
+ children.push_back( in[2] );
+ }
+ ret = NodeManager::currentNM()->mkNode( FORALL, children );
+ ret = ret.negate();
+ status = REWRITE_AGAIN_FULL;
+ }else if( in.getKind()==FORALL ){
+ //compute attributes
+ QAttributes qa;
+ TermDb::computeQuantAttributes( in, qa );
+ if( !qa.isRewriteRule() ){
for( int op=0; op<COMPUTE_LAST; op++ ){
- //TODO : compute isNested (necessary?)
- bool isNested = false;
- if( doOperation( in, isNested, op ) ){
- ret = computeOperation( in, isNested, op );
+ if( doOperation( in, op, qa ) ){
+ ret = computeOperation( in, op, qa );
if( ret!=in ){
status = REWRITE_AGAIN_FULL;
break;
}
}
}
- //print if changed
- if( in!=ret ){
- Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
- Trace("quantifiers-rewrite") << " to " << std::endl;
- Trace("quantifiers-rewrite") << ret << std::endl;
- }
- return RewriteResponse( status, ret );
}
- return RewriteResponse(REWRITE_DONE, in);
+ //print if changed
+ if( in!=ret ){
+ Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+ Trace("quantifiers-rewrite") << " to " << std::endl;
+ Trace("quantifiers-rewrite") << ret << std::endl;
+ }
+ return RewriteResponse( status, ret );
}
Node QuantifiersRewriter::computeElimSymbols( Node body ) {
}
}
-Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ){
+Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){
std::map< Node, bool > curr_cond;
std::map< Node, Node > cache;
std::map< Node, Node > icache;
- Node h = TermDb::getFunDefHead( q );
- if( !h.isNull() ){
+ if( qa.isFunDef() ){
+ Node h = TermDb::getFunDefHead( q );
+ Assert( !h.isNull() );
// if it is a function definition, rewrite the body independently
Node fbody = TermDb::getFunDefBody( q );
Assert( !body.isNull() );
return false;
}
-Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){
+Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){
Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
std::map< Node, Node > pcons;
}
}
if( options::condVarSplitQuant() ){
- if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){
+ if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){
+ Assert( !qa.isFunDef() );
Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
bool do_split = false;
unsigned index_max = body.getKind()==ITE ? 0 : 1;
return false;
}
-Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){
+Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){
Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
QuantPhaseReq qpr( body );
std::vector< Node > vars;
//remake with eliminated nodes
body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
body = Rewriter::rewrite( body );
- if( !ipl.isNull() ){
- ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ if( !qa.d_ipl.isNull() ){
+ qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
}
Trace("var-elim-quant") << "Return " << body << std::endl;
}
return body;
}
-Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
+Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){
//the parent id's for each variable, if using purifyQuant
std::map< Node, std::vector< int > > var_parent;
if( options::purifyQuant() ){
Node prev;
do{
prev = body;
- body = computeVarElimination2( body, args, ipl, var_parent );
+ body = computeVarElimination2( body, args, qa, var_parent );
}while( prev!=body && !args.empty() );
}
return body;
return f;
}
-Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
+Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){
std::vector< Node > activeArgs;
//if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
- if( options::ceGuidedInst() && TermDb::isSygusConjectureAnnotation( ipl ) ){
+ if( options::ceGuidedInst() && qa.d_sygus ){
activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
}else{
- computeArgVec2( args, activeArgs, body, ipl );
+ computeArgVec2( args, activeArgs, body, qa.d_ipl );
}
if( activeArgs.empty() ){
return body;
std::vector< Node > children;
children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
children.push_back( body );
- if( !ipl.isNull() ){
- children.push_back( ipl );
+ if( !qa.d_ipl.isNull() ){
+ children.push_back( qa.d_ipl );
}
return NodeManager::currentNM()->mkNode( kind::FORALL, children );
}
}
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){
+Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){
if( body.getKind()==FORALL ){
//combine arguments
std::vector< Node > newArgs;
newArgs.push_back( body[0][i] );
}
newArgs.insert( newArgs.end(), args.begin(), args.end() );
- return mkForAll( newArgs, body[ 1 ], ipl );
+ return mkForAll( newArgs, body[ 1 ], qa );
}else{
if( body.getKind()==NOT ){
//push not downwards
if( body[0].getKind()==NOT ){
- return computeMiniscoping( f, args, body[0][0], ipl );
+ return computeMiniscoping( f, args, body[0][0], qa );
}else if( body[0].getKind()==AND ){
if( options::miniscopeQuantFreeVar() ){
NodeBuilder<> t(kind::OR);
for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
}
- return computeMiniscoping( f, args, t.constructNode(), ipl );
+ return computeMiniscoping( f, args, t.constructNode(), qa );
}
}else if( body[0].getKind()==OR ){
if( options::miniscopeQuant() ){
NodeBuilder<> t(kind::AND);
for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
Node trm = body[0][i].negate();
- t << computeMiniscoping( f, args, trm, ipl );
+ t << computeMiniscoping( f, args, trm, qa );
}
return t.constructNode();
}
//break apart
NodeBuilder<> t(kind::AND);
for( unsigned i=0; i<body.getNumChildren(); i++ ){
- t << computeMiniscoping( f, args, body[i], ipl );
+ t << computeMiniscoping( f, args, body[i], qa );
}
Node retVal = t;
return retVal;
return body_split;
}else if( body_split.getNumChildren()>0 ){
newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
- body_split << mkForAll( args, newBody, ipl );
+ body_split << mkForAll( args, newBody, qa );
return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
}
}
//if( body==f[1] ){
// return f;
//}else{
- return mkForAll( args, body, ipl );
+ return mkForAll( args, body, qa );
//}
}
return n;
}
}
- return mkForAll( args, body, Node::null() );
+ QAttributes qa;
+ return mkForAll( args, body, qa );
}
-bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
+bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){
+ bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef();
if( computeOption==COMPUTE_ELIM_SYMBOLS ){
return true;
}else if( computeOption==COMPUTE_MINISCOPING ){
- return true;
+ return is_std;
}else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
- return options::aggressiveMiniscopeQuant();
+ return options::aggressiveMiniscopeQuant() && is_std;
}else if( computeOption==COMPUTE_NNF ){
return options::nnfQuant();
}else if( computeOption==COMPUTE_PROCESS_TERMS ){
return true;
//return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
}else if( computeOption==COMPUTE_COND_SPLIT ){
- return options::iteDtTesterSplitQuant() || options::condVarSplitQuant();
+ return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std;
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant();
+ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
//}else if( computeOption==COMPUTE_CNF ){
// return options::cnfQuant();
}else if( computeOption==COMPUTE_PURIFY_EXPAND ){
}
//general method for computing various rewrites
-Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){
- if( f.getKind()==FORALL ){
- Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl;
- std::vector< Node > args;
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- args.push_back( f[0][i] );
- }
- Node n = f[1];
- Node ipl;
- if( f.getNumChildren()==3 ){
- ipl = f[2];
- }
- if( computeOption==COMPUTE_ELIM_SYMBOLS ){
- n = computeElimSymbols( n );
- }else if( computeOption==COMPUTE_MINISCOPING ){
- //return directly
- return computeMiniscoping( f, args, n, ipl );
- }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
- return computeAggressiveMiniscoping( args, n );
- }else if( computeOption==COMPUTE_NNF ){
- n = computeNNF( n );
- }else if( computeOption==COMPUTE_PROCESS_TERMS ){
- std::vector< Node > new_conds;
- n = computeProcessTerms( n, args, new_conds, f );
- if( !new_conds.empty() ){
- new_conds.push_back( n );
- n = NodeManager::currentNM()->mkNode( OR, new_conds );
- }
- }else if( computeOption==COMPUTE_COND_SPLIT ){
- n = computeCondSplit( n, ipl );
- }else if( computeOption==COMPUTE_PRENEX ){
- n = computePrenex( n, args, true );
- }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- n = computeVarElimination( n, args, ipl );
- //}else if( computeOption==COMPUTE_CNF ){
- //n = computeCNF( n, args, defs, false );
- //ipl = Node::null();
- }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
- std::vector< Node > conj;
- computePurifyExpand( n, conj, args, ipl );
- if( !conj.empty() ){
- return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
- }else{
- return f;
- }
+Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
+ Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+ std::vector< Node > args;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ args.push_back( f[0][i] );
+ }
+ Node n = f[1];
+ if( computeOption==COMPUTE_ELIM_SYMBOLS ){
+ n = computeElimSymbols( n );
+ }else if( computeOption==COMPUTE_MINISCOPING ){
+ //return directly
+ return computeMiniscoping( f, args, n, qa );
+ }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
+ return computeAggressiveMiniscoping( args, n );
+ }else if( computeOption==COMPUTE_NNF ){
+ n = computeNNF( n );
+ }else if( computeOption==COMPUTE_PROCESS_TERMS ){
+ std::vector< Node > new_conds;
+ n = computeProcessTerms( n, args, new_conds, f, qa );
+ if( !new_conds.empty() ){
+ new_conds.push_back( n );
+ n = NodeManager::currentNM()->mkNode( OR, new_conds );
}
- Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
- if( f[1]==n && args.size()==f[0].getNumChildren() ){
+ }else if( computeOption==COMPUTE_COND_SPLIT ){
+ n = computeCondSplit( n, qa );
+ }else if( computeOption==COMPUTE_PRENEX ){
+ n = computePrenex( n, args, true );
+ }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+ n = computeVarElimination( n, args, qa );
+ //}else if( computeOption==COMPUTE_CNF ){
+ //n = computeCNF( n, args, defs, false );
+ //ipl = Node::null();
+ }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
+ std::vector< Node > conj;
+ computePurifyExpand( n, conj, args, qa );
+ if( !conj.empty() ){
+ return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+ }else{
return f;
+ }
+ }
+ Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
+ if( f[1]==n && args.size()==f[0].getNumChildren() ){
+ return f;
+ }else{
+ if( args.empty() ){
+ return n;
}else{
- if( args.empty() ){
- return n;
- }else{
- std::vector< Node > children;
- children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
- children.push_back( n );
- if( !ipl.isNull() ){
- children.push_back( ipl );
- }
- return NodeManager::currentNM()->mkNode(kind::FORALL, children );
+ std::vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+ children.push_back( n );
+ if( !qa.d_ipl.isNull() ){
+ children.push_back( qa.d_ipl );
}
+ return NodeManager::currentNM()->mkNode(kind::FORALL, children );
}
- }else{
- return f;
}
}
}
}
-void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ) {
+void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ) {
if( body.getKind()==OR ){
Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl;
std::map< int, std::vector< Node > > disj;
namespace theory {
namespace quantifiers {
+class QAttributes;
+
class QuantifiersRewriter {
private:
static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
static int getPurifyIdLit( Node n );
private:
static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
- static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
+ static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
std::map< Node, std::vector< int > >& var_parent );
static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
std::map< Node, std::vector< int > >& var_parent, int parentId );
- static Node computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent );
+ static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent );
private:
static Node computeElimSymbols( Node body );
- static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
+ static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa );
static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
static Node computeNNF( Node body );
//cache is dependent upon currCond, icache is not, new_conds are negated conditions
- static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q );
- static Node computeCondSplit( Node body, Node ipl );
+ static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
+ static Node computeCondSplit( Node body, QAttributes& qa );
static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
static Node computeSplit( Node f, std::vector< Node >& args, Node body );
- static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
+ static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
- static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl );
+ static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa );
private:
enum{
COMPUTE_ELIM_SYMBOLS = 0,
//COMPUTE_CNF,
COMPUTE_LAST
};
- static Node computeOperation( Node f, bool isNested, int computeOption );
+ static Node computeOperation( Node f, int computeOption, QAttributes& qa );
public:
static RewriteResponse preRewrite(TNode in);
static RewriteResponse postRewrite(TNode in);
static inline void shutdown() {}
private:
/** options */
- static bool doOperation( Node f, bool isNested, int computeOption );
+ static bool doOperation( Node f, int computeOption, QAttributes& qa );
private:
static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
public:
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() );
+ }
+ 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() );
+ }
+ 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() );
+ }
+ 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() );
+ }
+}
+
+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_ATTRIBUTE ){
Node avar = q[2][i][0];
if( avar.getAttribute(AxiomAttribute()) ){
Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
- d_qattr_axiom[q] = true;
+ qa.d_axiom = true;
}
if( avar.getAttribute(ConjectureAttribute()) ){
Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
- d_qattr_conjecture[q] = true;
+ qa.d_conjecture = true;
}
if( avar.getAttribute(FunDefAttribute()) ){
Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
- d_qattr_fundef[q] = true;
//get operator directly from pattern
- Node f = q[2][i][0].getOperator();
- if( d_fun_defs.find( f )!=d_fun_defs.end() ){
- Message() << "Cannot define function " << f << " more than once." << std::endl;
- exit( 0 );
- }
- d_fun_defs[f] = true;
- d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+ 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;
- d_qattr_sygus[q] = true;
- if( d_quantEngine->getCegInstantiation()==NULL ){
- Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
- }
- d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+ qa.d_sygus = true;
}
if( avar.getAttribute(SynthesisAttribute()) ){
Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
- d_qattr_synthesis[q] = true;
- if( d_quantEngine->getCegInstantiation()==NULL ){
- Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
- }
- d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+ qa.d_synthesis = true;
}
if( avar.hasAttribute(QuantInstLevelAttribute()) ){
- d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
- Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
+ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
+ Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
}
if( avar.hasAttribute(RrPriorityAttribute()) ){
- d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
- Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
+ 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.getKind()==REWRITE_RULE ){
Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
Assert( i==0 );
- if( d_quantEngine->getRewriteEngine()==NULL ){
- Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
- }
- //set rewrite engine as owner
- d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+ qa.d_rr = avar;
}
}
}
}
bool TermDb::isQAttrConjecture( Node q ) {
- std::map< Node, bool >::iterator it = d_qattr_conjecture.find( q );
- if( it==d_qattr_conjecture.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return false;
}else{
- return it->second;
+ return it->second.d_conjecture;
}
}
bool TermDb::isQAttrAxiom( Node q ) {
- std::map< Node, bool >::iterator it = d_qattr_axiom.find( q );
- if( it==d_qattr_axiom.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return false;
}else{
- return it->second;
+ return it->second.d_axiom;
}
}
bool TermDb::isQAttrFunDef( Node q ) {
- std::map< Node, bool >::iterator it = d_qattr_fundef.find( q );
- if( it==d_qattr_fundef.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return false;
}else{
- return it->second;
+ return it->second.isFunDef();
}
}
bool TermDb::isQAttrSygus( Node q ) {
- std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
- if( it==d_qattr_sygus.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return false;
}else{
- return it->second;
+ return it->second.d_sygus;
}
}
bool TermDb::isQAttrSynthesis( Node q ) {
- std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
- if( it==d_qattr_synthesis.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return false;
}else{
- return it->second;
+ return it->second.d_synthesis;
}
}
int TermDb::getQAttrQuantInstLevel( Node q ) {
- std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
- if( it==d_qattr_qinstLevel.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return -1;
}else{
- return it->second;
+ return it->second.d_qinstLevel;
}
}
int TermDb::getQAttrRewriteRulePriority( Node q ) {
- std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q );
- if( it==d_qattr_rr_priority.end() ){
+ std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+ if( it==d_qattr.end() ){
return -1;
}else{
- return it->second;
+ 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;
+ }
+}
TermDbSygus::TermDbSygus(){
d_true = NodeManager::currentNM()->mkConst( true );
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;
+
class QuantifiersEngine;
namespace inst{
};/* class TermArgTrie */
+class QAttributes{
+public:
+ QAttributes() : 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(){}
+ 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;
+ bool isRewriteRule() { return !d_rr.isNull(); }
+ bool isFunDef() { return !d_fundef_f.isNull(); }
+};
+
namespace fmcheck {
class FullModelChecker;
}
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, bool > d_qattr_conjecture;
- std::map< Node, bool > d_qattr_axiom;
- std::map< Node, bool > d_qattr_fundef;
- std::map< Node, bool > d_qattr_sygus;
- std::map< Node, bool > d_qattr_synthesis;
- std::map< Node, int > d_qattr_rr_priority;
- std::map< Node, int > d_qattr_qinstLevel;
+ std::map< Node, QAttributes > d_qattr;
//record attributes
void computeAttributes( Node q );
public:
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 );
+ /** compute quantifier attributes */
+ static void computeQuantAttributes( Node q, QAttributes& qa );
};/* class TermDb */
class TermDbSygus {
out.handleUserAttribute( "synthesis", this );
out.handleUserAttribute( "quant-inst-max-level", this );
out.handleUserAttribute( "rr-priority", this );
+ out.handleUserAttribute( "quant-elim", this );
+ out.handleUserAttribute( "quant-elim-partial", this );
}
TheoryQuantifiers::~TheoryQuantifiers() {
bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
Assert( f.getKind()==FORALL );
Assert( vars.size()==terms.size() );
- Node body = getInstantiation( f, vars, terms );
- //do virtual term substitution
+ Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution
if( doVts ){
body = Rewriter::rewrite( body );
Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
}
-Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ){
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
Node body;
//process partial instantiation if necessary
if( d_term_db->d_vars[q].size()!=vars.size() ){
}
}
}
+ if( doVts ){
+ //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 );
+ Trace("quant-vts-debug") << " ...result: " << body_r << std::endl;
+ body = body_r;
+ }
return body;
}
-Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m ){
+Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
std::vector< Node > vars;
std::vector< Node > terms;
computeTermVector( q, m, vars, terms );
- return getInstantiation( q, vars, terms );
+ return getInstantiation( q, vars, terms, doVts );
}
-Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms ) {
- return getInstantiation( q, d_term_db->d_vars[q], terms );
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
+ return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
}
/*
void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
if( options::incrementalSolving() ){
for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
- it->second->getInstantiations( insts[it->first], it->first );
+ it->second->getInstantiations( insts[it->first], it->first, this );
}
}else{
for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
- it->second.getInstantiations( insts[it->first], it->first );
+ it->second.getInstantiations( insts[it->first], it->first, this );
}
}
}
void flushLemmas();
public:
/** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms );
+ Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
/** get instantiation */
- Node getInstantiation( Node q, InstMatch& m );
+ Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
/** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& terms );
+ Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
/** do substitution */
Node getSubstitute( Node n, std::vector< Node >& terms );
/** add lemma lem */
}
-void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
+void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value) {
Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
* This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
* via the syntax (! n :attr)
*/
- void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
+ void setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value);
/**
* Handle user attribute.
projects / cvc5.git / commitdiff