if( !options::rewriteDivk.wasSetByUser()) {
options::rewriteDivk.set( true );
}
+ //do not do macros
+ if( !options::macrosQuant.wasSetByUser()) {
+ options::macrosQuant.set( false );
+ }
}
//cbqi options
dumpAssertions("post-skolem-quant", d_assertions);
if( options::macrosQuant() ){
//quantifiers macro expansion
- quantifiers::QuantifierMacros qm;
+ quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
bool success;
do{
success = qm.simplify( d_assertions.ref(), true );
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/modes.h"
#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
using namespace CVC4;
using namespace std;
bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
- unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2;
+ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
for( unsigned r=0; r<rmax; r++ ){
d_ground_macros = (r==0);
Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
//first, collect macro definitions
- std::map< unsigned, Node > simp_assertions;
- int last_macro = -1;
for( int i=0; i<(int)assertions.size(); i++ ){
Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
- Node curr = assertions[i];
- //do simplification before process
- if( doRewrite && !d_macro_defs_new.empty() ){
- curr = simplify( assertions[i] );
- curr = Rewriter::rewrite( curr );
- if( curr!=assertions[i] ){
- simp_assertions[i] = curr;
- }
- }
- if( processAssertion( curr ) ){
- last_macro = i;
+ if( processAssertion( assertions[i] ) ){
//process this assertion again
i--;
}
Trace("macros") << "Do simplifications..." << std::endl;
//now, rewrite based on macro definitions
for( unsigned i=0; i<assertions.size(); i++ ){
- Node curr = assertions[i];
- std::map< unsigned, Node >::iterator it = simp_assertions.find( i );
- if( it!=simp_assertions.end() ){
- curr = it->second;
- }
- //simplify again if before last macro
- if( (int)i<last_macro ){
- curr = simplify( curr );
- }
+ Node curr = simplify( assertions[i] );
if( curr!=assertions[i] ){
curr = Rewriter::rewrite( curr );
Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
}
}
}
- for( int i=0; i<(int)assertions.size(); i++ ){
- if( Trace.isOn("macros-warn") ){
+ if( Trace.isOn("macros-warn") ){
+ for( int i=0; i<(int)assertions.size(); i++ ){
debugMacroDefinition( assertions[i], assertions[i] );
}
}
return true;
}
}
- return false;
- }else if( n.getKind()==FORALL ){
+ }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
std::vector< Node > args;
for( size_t j=0; j<n[0].getNumChildren(); j++ ){
args.push_back( n[0][j] );
}
+ Node nproc = n[1];
+ if( !d_macro_defs_new.empty() ){
+ nproc = simplify( nproc );
+ if( nproc!=n[1] ){
+ nproc = Rewriter::rewrite( nproc );
+ }
+ }
//look at the body of the quantifier for macro definition
- return process( n[1], true, args, n );
- }else{
- return false;
+ if( process( nproc, true, args, n ) ){
+ d_quant_macros[n] = true;
+ return true;
+ }
}
+ return false;
}
-bool QuantifierMacros::contains( Node n, Node n_s ){
- if( n==n_s ){
- return true;
- }else{
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( contains( n[i], n_s ) ){
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==APPLY_UF ){
+ Node nop = n.getOperator();
+ if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){
return true;
}
- }
- return false;
- }
-}
-
-bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){
- if( n.getKind()==APPLY_UF ){
- Node nop = n.getOperator();
- if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){
+ if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+ opc.push_back( nop );
+ }
+ }else if( d_ground_macros && n.getKind()==FORALL ){
return true;
}
- if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
- opc.push_back( nop );
- }
- }else if( d_ground_macros && n.getKind()==FORALL ){
- return true;
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( containsBadOp( n[i], op, opc ) ){
- return true;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ if( containsBadOp( n[i], op, opc, visited ) ){
+ return true;
+ }
}
}
return false;
return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
}
+bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+ Node icn = d_qe->getTermDatabase()->getInstConstantNode( n, f );
+ Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
+ std::vector< Node > var;
+ d_qe->getTermDatabase()->getVarContainsNode( f, icn, var );
+ Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
+ std::vector< Node > trigger_var;
+ inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var );
+ Trace("macros-debug2") << "Done." << std::endl;
+ //only if all variables are also trigger variables
+ return trigger_var.size()>=var.size();
+}
+
bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
Assert( n.getKind()==APPLY_UF );
TypeNode tn = n.getOperator().getType();
return true;
}
-void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
- if( n.getKind()==APPLY_UF ){
- if( isBoundVarApplyUf( n ) ){
- candidates.push_back( n );
- }
- }else if( n.getKind()==PLUS ){
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- getMacroCandidates( n[i], candidates );
- }
- }else if( n.getKind()==MULT ){
- //if the LHS is a constant
- if( n.getNumChildren()==2 && n[0].isConst() ){
- getMacroCandidates( n[1], candidates );
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==APPLY_UF ){
+ if( isBoundVarApplyUf( n ) ){
+ candidates.push_back( n );
+ }
+ }else if( n.getKind()==PLUS ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ getMacroCandidates( n[i], candidates, visited );
+ }
+ }else if( n.getKind()==MULT ){
+ //if the LHS is a constant
+ if( n.getNumChildren()==2 && n[0].isConst() ){
+ getMacroCandidates( n[1], candidates, visited );
+ }
+ }else if( n.getKind()==NOT ){
+ getMacroCandidates( n[0], candidates, visited );
}
- }else if( n.getKind()==NOT ){
- getMacroCandidates( n[0], candidates );
}
}
return Node::null();
}
-bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){
- if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
- if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
- if( retOnly ){
- return true;
- }else{
- vars.push_back( n );
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
+ if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+ if( retOnly ){
+ return true;
+ }else{
+ vars.push_back( n );
+ }
}
}
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){
- return true;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
+ return true;
+ }
}
}
return false;
}else{
//literal case
if( isMacroLiteral( n, pol ) ){
+ std::map< Node, bool > visited;
std::vector< Node > candidates;
for( size_t i=0; i<n.getNumChildren(); i++ ){
- getMacroCandidates( n[i], candidates );
+ getMacroCandidates( n[i], candidates, visited );
}
for( size_t i=0; i<candidates.size(); i++ ){
Node m = candidates[i];
Node op = m.getOperator();
if( d_macro_defs.find( op )==d_macro_defs.end() ){
std::vector< Node > fvs;
- getFreeVariables( m, args, fvs, false );
+ visited.clear();
+ getFreeVariables( m, args, fvs, false, visited );
//get definition and condition
Node n_def = solveInEquality( m, n ); //definition for the macro
- //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains
- std::vector< Node > opc;
- if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op, opc ) ){
- Node n_cond; //condition when this definition holds
- //conditional must not contain any free variables apart from fvs
- if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
- Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
- //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
- // x1 ... xn are distinct variables
- if( d_macro_basis[op].empty() ){
- for( size_t a=0; a<m.getNumChildren(); a++ ){
- std::stringstream ss;
- ss << "mda_" << op << "";
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
- d_macro_basis[op].push_back( v );
+ if( !n_def.isNull() ){
+ Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
+ Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl;
+ visited.clear();
+ //definition must exist and not contain any free variables apart from fvs
+ if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
+ Trace("macros-debug") << "...free variables are contained." << std::endl;
+ visited.clear();
+ //cannot contain a defined operator, opc is list of functions it contains
+ std::vector< Node > opc;
+ if( !containsBadOp( n_def, op, opc, visited ) ){
+ Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
+ //must be ground UF term if mode is GROUND_UF
+ if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
+ Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
+ //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
+ // x1 ... xn are distinct variables
+ if( d_macro_basis[op].empty() ){
+ for( size_t a=0; a<m.getNumChildren(); a++ ){
+ std::stringstream ss;
+ ss << "mda_" << op << "";
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+ d_macro_basis[op].push_back( v );
+ }
+ }
+ std::map< Node, Node > solved;
+ for( size_t a=0; a<m.getNumChildren(); a++ ){
+ solved[m[a]] = d_macro_basis[op][a];
+ }
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ if( getSubstitution( fvs, solved, vars, subs, true ) ){
+ n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ addMacro( op, n_def, opc );
+ return true;
+ }
}
}
- std::map< Node, Node > solved;
- for( size_t a=0; a<m.getNumChildren(); a++ ){
- solved[m[a]] = d_macro_basis[op][a];
- }
- std::vector< Node > vars;
- std::vector< Node > subs;
- if( getSubstitution( fvs, solved, vars, subs, true ) ){
- n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- addMacro( op, n_def, opc );
- return true;
- }
}
}
}
}
void QuantifierMacros::finalizeDefinitions() {
- if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){
+ bool doDefs = false;
+ if( Trace.isOn("macros-warn") ){
+ doDefs = true;
+ }
+ if( options::incrementalSolving() || options::produceModels() || doDefs ){
Trace("macros") << "Store as defined functions..." << std::endl;
//also store as defined functions
for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
#include <map>
#include "expr/node.h"
#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class QuantifierMacros{
+private:
+ QuantifiersEngine * d_qe;
private:
bool d_ground_macros;
bool processAssertion( Node n );
bool isBoundVarApplyUf( Node n );
bool process( Node n, bool pol, std::vector< Node >& args, Node f );
- bool contains( Node n, Node n_s );
- bool containsBadOp( Node n, Node op, std::vector< Node >& opc );
+ bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited );
bool isMacroLiteral( Node n, bool pol );
- void getMacroCandidates( Node n, std::vector< Node >& candidates );
+ bool isGroundUfTerm( Node f, Node n );
+ void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited );
Node solveInEquality( Node n, Node lit );
- bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );
+ bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited );
bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
//map from operators to macro basis terms
std::map< Node, Node > d_macro_defs_new;
//operators to macro ops that contain them
std::map< Node, std::vector< Node > > d_macro_def_contains;
- //simplify cache
+ //simplify caches
std::map< Node, Node > d_simplify_cache;
+ std::map< Node, bool > d_quant_macros;
private:
Node simplify( Node n );
void addMacro( Node op, Node n, std::vector< Node >& opc );
void debugMacroDefinition( Node oo, Node n );
public:
- QuantifierMacros(){}
+ QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){}
~QuantifierMacros(){}
bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
MACROS_QUANT_MODE_ALL,
/** infer ground definitions */
MACROS_QUANT_MODE_GROUND,
+ /** infer ground uf definitions */
+ MACROS_QUANT_MODE_GROUND_UF,
} MacrosQuantMode;
}/* CVC4::theory::quantifiers namespace */
option quantAlphaEquiv --quant-alpha-equiv bool :default true
infer alpha equivalence between quantified formulas
-option macrosQuant --macros-quant bool :default false
+option macrosQuant --macros-quant bool :read-write :default false
perform quantifiers macro expansion
-option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
mode for quantifiers macro expansion
### recursive function options
ground (default) \n\
+ Only infer ground definitions for functions.\n\
\n\
+ground-uf \n\
++ Only infer ground definitions for functions that result in triggers for all free variables.\n\
+\n\
";
inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
return MACROS_QUANT_MODE_ALL;
} else if(optarg == "ground") {
return MACROS_QUANT_MODE_GROUND;
+ } else if(optarg == "ground-uf") {
+ return MACROS_QUANT_MODE_GROUND_UF;
} else if(optarg == "help") {
puts(macrosQuantHelp.c_str());
exit(1);
Node TermDb::getInstConstantBody( Node f ){
std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
if( it==d_inst_const_body.end() ){
- makeInstantiationConstantsFor( f );
Node n = getInstConstantNode( f[1], f );
d_inst_const_body[ f ] = n;
return n;
}
Node TermDb::getInstConstantNode( Node n, Node f ){
- Assert( d_inst_constants.find( f )!=d_inst_constants.end() );
- return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
-}
-
-Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
- const std::vector<Node> & inst_constants){
- Node n2 = n.substitute( vars.begin(), vars.end(),
- inst_constants.begin(),
- inst_constants.end() );
+ makeInstantiationConstantsFor( f );
+ Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(),
+ d_inst_constants[f].begin(), d_inst_constants[f].end() );
return n2;
}
return d_free_vars[tn];
}
-void TermDb::computeVarContains( Node n ) {
- if( d_var_contains.find( n )==d_var_contains.end() ){
- d_var_contains[n].clear();
- computeVarContains2( n, n );
- }
+void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
+ std::map< Node, bool > visited;
+ computeVarContains2( n, varContains, visited );
}
-void TermDb::computeVarContains2( Node n, Node parent ){
- if( n.getKind()==INST_CONSTANT ){
- if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
- d_var_contains[parent].push_back( n );
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- computeVarContains2( n[i], parent );
- }
- }
-}
-
-bool TermDb::isVariableSubsume( Node n1, Node n2 ){
- if( n1==n2 ){
- return true;
- }else{
- //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
- computeVarContains( n1 );
- computeVarContains( n2 );
- for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){
- if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){
- //Notice() << "no" << std::endl;
- return false;
+void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==INST_CONSTANT ){
+ 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], varContains, visited );
}
}
- //Notice() << "yes" << std::endl;
- return true;
}
}
void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
- for( int i=0; i<(int)pats.size(); i++ ){
- computeVarContains( pats[i] );
+ for( unsigned i=0; i<pats.size(); i++ ){
varContains[ pats[i] ].clear();
- for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){
- if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){
- varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] );
- }
- }
+ getVarContainsNode( f, pats[i], varContains[ pats[i] ] );
}
}
void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
- computeVarContains( n );
- for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
- if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
- varContains.push_back( d_var_contains[n][j] );
+ 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 );
+ }
}
}
}
-/** is n1 an instance of n2 or vice versa? */
-int TermDb::isInstanceOf( Node n1, Node n2 ){
+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() ){
int result = 0;
for( int i=0; i<(int)n1.getNumChildren(); i++ ){
if( n1[i]!=n2[i] ){
- int cResult = isInstanceOf( n1[i], n2[i] );
+ int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 );
if( cResult==0 ){
return 0;
}else if( cResult!=result ){
}
return 0;
}else if( n2.getKind()==INST_CONSTANT ){
- computeVarContains( n1 );
//if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
// return 1;
//}
- if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){
+ if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){
return 1;
}
}else if( n1.getKind()==INST_CONSTANT ){
- computeVarContains( n2 );
//if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
// return -1;
//}
- if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){
+ 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;
void TermDb::filterInstances( std::vector< Node >& nodes ){
std::vector< bool > active;
active.resize( nodes.size(), true );
- for( int i=0; i<(int)nodes.size(); i++ ){
- for( int j=i+1; j<(int)nodes.size(); j++ ){
+ 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 = isInstanceOf( nodes[i], nodes[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;
}
}
std::vector< Node > temp;
- for( int i=0; i<(int)nodes.size(); i++ ){
+ for( unsigned i=0; i<nodes.size(); i++ ){
if( active[i] ){
temp.push_back( nodes[i] );
}
instantiation.
*/
Node getInstConstantNode( Node n, Node f );
- /** same as before but node f is just linked to the new pattern by the
- applied attribute
- vars the bind variable
- nvars the same variable but with an attribute
- */
- Node convertNodeToPattern( Node n, Node f,
- const std::vector<Node> & vars,
- const std::vector<Node> & nvars);
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
//for triggers
private:
/** helper function for compute var contains */
- void computeVarContains2( Node n, Node parent );
- /** var contains */
- std::map< TNode, std::vector< TNode > > d_var_contains;
+ void computeVarContains2( Node n, 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 */
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 */
+ int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
public:
/** compute var contains */
- void computeVarContains( Node n );
- /** variables subsume, return true if n1 contains all free variables in n2 */
- bool isVariableSubsume( Node n1, Node n2 );
+ void computeVarContains( Node n, std::vector< Node >& varContains );
/** get var contains for each of the patterns in pats */
void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
std::map< Node, bool > vars;
std::map< Node, std::vector< Node > > patterns;
size_t varCount = 0;
- for( int i=0; i<(int)temp.size(); i++ ){
+ std::map< Node, std::vector< Node > > varContains;
+ qe->getTermDatabase()->getVarContains( f, temp, varContains );
+ for( unsigned i=0; i<temp.size(); i++ ){
bool foundVar = false;
- qe->getTermDatabase()->computeVarContains( temp[i] );
- for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
- Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
- if( quantifiers::TermDb::getInstConstAttr(v)==f ){
- if( vars.find( v )==vars.end() ){
- varCount++;
- vars[ v ] = true;
- foundVar = true;
- }
+ for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+ Node v = varContains[ temp[i] ][j];
+ Assert( quantifiers::TermDb::getInstConstAttr(v)==f );
+ if( vars.find( v )==vars.end() ){
+ varCount++;
+ vars[ v ] = true;
+ foundVar = true;
}
}
if( foundVar ){
trNodes.push_back( temp[i] );
- for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
- Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
+ for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+ Node v = varContains[ temp[i] ][j];
patterns[ v ].push_back( temp[i] );
}
}
return NULL;
}else{
//now, minimize the trigger
- for( int i=0; i<(int)trNodes.size(); i++ ){
+ for( unsigned i=0; i<trNodes.size(); i++ ){
bool keepPattern = false;
Node n = trNodes[i];
- for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
- Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
+ for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+ Node v = varContains[ n ][j];
if( patterns[v].size()==1 ){
keepPattern = true;
break;
}
if( !keepPattern ){
//remove from pattern vector
- for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
- Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
- for( int k=0; k<(int)patterns[v].size(); k++ ){
+ for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+ Node v = varContains[ n ][j];
+ for( unsigned k=0; k<patterns[v].size(); k++ ){
if( patterns[v][k]==n ){
patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
break;
}
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
+bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
if( patMap.find( n )==patMap.end() ){
patMap[ n ] = false;
bool newHasPol = n.getKind()==IFF ? false : hasPol;
bool retVal = false;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+ if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
retVal = true;
}
}
if( n.getKind()!=FORALL ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+ if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
retVal = true;
}
}
}
}
}
- collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true );
+ collectPatTerms2( f, n, patMap, tstrt, exclude, true, true );
for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
if( it->second ){
patTerms.push_back( it->first );
return Node::null();
}
+void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
+ std::vector< Node > patTerms;
+ //collect all patterns from icn
+ std::vector< Node > exclude;
+ collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude );
+ //collect all variables from all patterns in patTerms, add to t_vars
+ for( unsigned i=0; i<patTerms.size(); i++ ){
+ qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
+ }
+}
+
InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
if( n.getKind()==INST_CONSTANT ){
return NULL;
static bool isUsable( Node n, Node f );
static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
+ static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
public:
//different strategies for choosing trigger terms
enum {
static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
static Node getInversionVariable( Node n );
static Node getInversion( Node n, Node x );
+ /** get all variables that E-matching can possibly handle */
+ static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars );
inline void toStream(std::ostream& out) const {
/*
-; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --macros-quant-mode=ground --no-check-models
(set-logic UFLIA)
(define-fun f ((x Int)) Int x)
projects / cvc5.git / commitdiff