summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp17
-rw-r--r--src/theory/quantifiers/options16
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp368
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h12
-rw-r--r--src/theory/quantifiers/term_database.cpp22
-rw-r--r--src/theory/quantifiers/term_database.h8
6 files changed, 197 insertions, 246 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 0bc5bb008..44b353ae5 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -598,19 +598,10 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
void CegInstantiation::preregisterAssertion( Node n ) {
//check if it sygus conjecture
- if( n.getKind()==FORALL ){
- if( n.getNumChildren()==3 ){
- for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
- if( n[2][i].getKind()==INST_ATTRIBUTE ){
- Node avar = n[2][i][0];
- if( avar.getAttribute(SygusAttribute()) ){
- //this is a sygus conjecture
- Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
- d_conj->preregisterConjecture( n );
- }
- }
- }
- }
+ if( TermDb::isSygusConjecture( n ) ){
+ //this is a sygus conjecture
+ Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
+ d_conj->preregisterConjecture( n );
}
}
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ec71e5348..74ce3cc6c 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -11,21 +11,21 @@ module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
option miniscopeQuant --miniscope-quant bool :default true :read-write
- disable miniscope quantifiers
+ miniscope quantifiers
# Whether to mini-scope quantifiers based on formulas with no free variables.
# For example, forall x. ( P( x ) V Q ) will be rewritten to
# ( forall x. P( x ) ) V Q
option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
- disable miniscope quantifiers for ground subformulas
-option clauseSplit --clause-split bool :default true
- apply clause splitting to quantified formulas
+ miniscope quantifiers for ground subformulas
+option quantSplit --quant-split bool :default true
+ apply splitting to quantified formulas based on variable disjoint disjuncts
option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
prenex mode for quantified formulas
# Whether to variable-eliminate quantifiers.
# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
# forall y. P( c, y )
option varElimQuant --var-elim-quant bool :default true
- disable simple variable elimination for quantified formulas
+ enable simple variable elimination for quantified formulas
option dtVarExpandQuant --dt-var-exp-quant bool :default true
expand datatype variables bound to one constructor in quantifiers
#ite lift mode for quantified formulas
@@ -65,7 +65,7 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
consider ground terms within bodies of quantified formulas for matching
option smartTriggers --smart-triggers bool :default true
- disable smart triggers
+ enable smart triggers
option relevantTriggers --relevant-triggers bool :default false
prefer triggers that are more relevant based on SInE style analysis
option relationalTriggers --relational-triggers bool :default false
@@ -135,13 +135,13 @@ option fmfInstEngine --fmf-inst-engine bool :default false
option fmfFullSaturate --fmf-full-saturate bool :default false
instantiate with all known ground terms for infinite domain quantifiers when finite model finding
option fmfInstGen --fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+ enable Inst-Gen instantiation techniques for finite model finding
option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
only perform Inst-Gen instantiation techniques on one quantifier per round
option fmfFreshDistConst --fmf-fresh-dc bool :default false
use fresh distinguished representative when applying Inst-Gen techniques
option fmfFmcSimple --fmf-fmc-simple bool :default true
- disable simple models in full model check for finite model finding
+ simple models in full model check for finite model finding
option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
finite model finding on bounded integer quantification
option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c32aeeb78..0fbf7e6a3 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -92,14 +92,17 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
}
}
-void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ){
- if( n.getKind()==BOUND_VARIABLE ){
- if( std::find( args.begin(), args.end(), n )!=args.end() ){
- activeMap[ n ] = true;
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- computeArgs( args, activeMap, n[i] );
+void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getKind()==BOUND_VARIABLE ){
+ if( std::find( args.begin(), args.end(), n )!=args.end() ){
+ activeMap[ n ] = true;
+ }
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ computeArgs( args, activeMap, n[i], visited );
+ }
}
}
}
@@ -107,10 +110,13 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node
void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
Assert( activeArgs.empty() );
std::map< Node, bool > activeMap;
- computeArgs( args, activeMap, n );
- for( unsigned i=0; i<args.size(); i++ ){
- if( activeMap.find( args[i] )!=activeMap.end() ){
- activeArgs.push_back( args[i] );
+ std::map< Node, bool > visited;
+ computeArgs( args, activeMap, n, visited );
+ if( !activeMap.empty() ){
+ for( unsigned i=0; i<args.size(); i++ ){
+ if( activeMap.find( args[i] )!=activeMap.end() ){
+ activeArgs.push_back( args[i] );
+ }
}
}
}
@@ -118,10 +124,11 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector<
void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) {
Assert( activeArgs.empty() );
std::map< Node, bool > activeMap;
- computeArgs( args, activeMap, n );
+ std::map< Node, bool > visited;
+ computeArgs( args, activeMap, n, visited );
if( !activeMap.empty() ){
//collect variables in inst pattern list only if we cannot eliminate quantifier
- computeArgs( args, activeMap, ipl );
+ computeArgs( args, activeMap, ipl, visited );
for( unsigned i=0; i<args.size(); i++ ){
if( activeMap.find( args[i] )!=activeMap.end() ){
activeArgs.push_back( args[i] );
@@ -130,32 +137,6 @@ void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector
}
}
-bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
- if( std::find( args.begin(), args.end(), n )!=args.end() ){
- return true;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( hasArg( args, n[i] ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-bool QuantifiersRewriter::hasArg1( Node a, Node n ) {
- if( n==a ){
- return true;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( hasArg1( a, n[i] ) ){
- return true;
- }
- }
- return false;
- }
-}
-
RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
@@ -258,21 +239,41 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
return body;
}else{
bool childrenChanged = false;
+ Kind k = body.getKind();
+ if( body.getKind()==IMPLIES ){
+ k = OR;
+ childrenChanged = true;
+ }else if( body.getKind()==XOR ){
+ k = IFF;
+ childrenChanged = true;
+ }
std::vector< Node > children;
+ std::map< Node, bool > lit_pol;
for( unsigned i=0; i<body.getNumChildren(); i++ ){
Node c = computeElimSymbols( body[i] );
if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){
c = c.negate();
}
- children.push_back( c );
+ if( ( k==OR || k==AND ) && options::elimTautQuant() ){
+ Node lit = c.getKind()==NOT ? c[0] : c;
+ bool pol = c.getKind()!=NOT;
+ std::map< Node, bool >::iterator it = lit_pol.find( lit );
+ if( it==lit_pol.end() ){
+ lit_pol[lit] = pol;
+ children.push_back( c );
+ }else{
+ childrenChanged = true;
+ if( it->second!=pol ){
+ return NodeManager::currentNM()->mkConst( k==OR );
+ }
+ }
+ }else{
+ children.push_back( c );
+ }
childrenChanged = childrenChanged || c!=body[i];
}
- if( body.getKind()==IMPLIES ){
- return NodeManager::currentNM()->mkNode( OR, children );
- }else if( body.getKind()==XOR ){
- return NodeManager::currentNM()->mkNode( IFF, children );
- }else if( childrenChanged ){
- return NodeManager::currentNM()->mkNode( body.getKind(), children );
+ if( childrenChanged ){
+ return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
}else{
return body;
}
@@ -456,7 +457,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, s
for( unsigned i=0; i<2; i++ ){
if( it->first[i].getKind()==BOUND_VARIABLE ){
unsigned j = i==0 ? 1 : 0;
- if( !hasArg1( it->first[i], it->first[j] ) ){
+ if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
vars.push_back( it->first[i] );
subs.push_back( it->first[j] );
break;
@@ -551,7 +552,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
int j = i==0 ? 1 : 0;
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
if( ita!=args.end() ){
- if( !hasArg1( it->first[i], it->first[j] ) ){
+ if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
vars.push_back( it->first[i] );
subs.push_back( it->first[j] );
args.erase( ita );
@@ -793,131 +794,103 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
}
}
-Node QuantifiersRewriter::computeElimTaut( Node body ) {
- if( body.getKind()==OR ){
- std::vector< Node > children;
- std::map< Node, bool > lit_pol;
- for( unsigned i=0; i<body.getNumChildren(); i++ ){
- Node lit = body[i].getKind()==NOT ? body[i][0] : body[i];
- bool pol = body[i].getKind()!=NOT;
- std::map< Node, bool >::iterator it = lit_pol.find( lit );
- if( it==lit_pol.end() ){
- lit_pol[lit] = pol;
- children.push_back( body[i] );
- }else{
- if( it->second!=pol ){
- return NodeManager::currentNM()->mkConst( true );
- }
- }
- }
- if( children.size()!=body.getNumChildren() ){
- return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
- }
- }
- return body;
-}
-
-Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
- if( body.getKind()==OR ){
- size_t var_found_count = 0;
- size_t eqc_count = 0;
- size_t eqc_active = 0;
- std::map< Node, int > var_to_eqc;
- std::map< int, std::vector< Node > > eqc_to_var;
- std::map< int, std::vector< Node > > eqc_to_lit;
+Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node body ) {
+ Assert( body.getKind()==OR );
+ size_t var_found_count = 0;
+ size_t eqc_count = 0;
+ size_t eqc_active = 0;
+ std::map< Node, int > var_to_eqc;
+ std::map< int, std::vector< Node > > eqc_to_var;
+ std::map< int, std::vector< Node > > eqc_to_lit;
- std::vector<Node> lits;
+ std::vector<Node> lits;
- for( size_t i=0; i<body.getNumChildren(); i++ ){
- //get variables contained in the literal
- Node n = body[i];
- std::vector<Node> lit_vars;
- computeArgVec( vars, lit_vars, n);
- //collectVars( n, vars, lit_vars );
- if (lit_vars.empty()) {
- lits.push_back(n);
- }else {
- std::vector<int> eqcs;
- std::vector<Node> lit_new_vars;
- //for each variable in literal
- for( size_t j=0; j<lit_vars.size(); j++) {
- //see if the variable has already been found
- if (var_to_eqc.find(lit_vars[j])!=var_to_eqc.end()) {
- int eqc = var_to_eqc[lit_vars[j]];
- if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
- eqcs.push_back(eqc);
- }
- }
- else {
- var_found_count++;
- lit_new_vars.push_back(lit_vars[j]);
+ for( unsigned i=0; i<body.getNumChildren(); i++ ){
+ //get variables contained in the literal
+ Node n = body[i];
+ std::vector< Node > lit_args;
+ computeArgVec( args, lit_args, n );
+ if (lit_args.empty()) {
+ lits.push_back(n);
+ }else {
+ //collect the equivalence classes this literal belongs to, and the new variables it contributes
+ std::vector< int > eqcs;
+ std::vector< Node > lit_new_args;
+ //for each variable in literal
+ for( unsigned j=0; j<lit_args.size(); j++) {
+ //see if the variable has already been found
+ if (var_to_eqc.find(lit_args[j])!=var_to_eqc.end()) {
+ int eqc = var_to_eqc[lit_args[j]];
+ if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
+ eqcs.push_back(eqc);
}
+ }else{
+ var_found_count++;
+ lit_new_args.push_back(lit_args[j]);
}
- if (eqcs.empty()) {
- eqcs.push_back(eqc_count);
- eqc_count++;
- eqc_active++;
- }
+ }
+ if (eqcs.empty()) {
+ eqcs.push_back(eqc_count);
+ eqc_count++;
+ eqc_active++;
+ }
- int eqcz = eqcs[0];
- //merge equivalence classes with eqcz
- for (unsigned j=1; j<eqcs.size(); j++) {
- int eqc = eqcs[j];
- //move all variables from equivalence class
- for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
- Node v = eqc_to_var[eqc][k];
- var_to_eqc[v] = eqcz;
- eqc_to_var[eqcz].push_back(v);
- }
- eqc_to_var.erase(eqc);
- //move all literals from equivalence class
- for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
- Node l = eqc_to_lit[eqc][k];
- eqc_to_lit[eqcz].push_back(l);
- }
- eqc_to_lit.erase(eqc);
- eqc_active--;
+ int eqcz = eqcs[0];
+ //merge equivalence classes with eqcz
+ for (unsigned j=1; j<eqcs.size(); j++) {
+ int eqc = eqcs[j];
+ //move all variables from equivalence class
+ for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
+ Node v = eqc_to_var[eqc][k];
+ var_to_eqc[v] = eqcz;
+ eqc_to_var[eqcz].push_back(v);
}
- if (eqc_active==1 && var_found_count==vars.size()) {
- return f;
+ eqc_to_var.erase(eqc);
+ //move all literals from equivalence class
+ for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
+ Node l = eqc_to_lit[eqc][k];
+ eqc_to_lit[eqcz].push_back(l);
}
- //add variables to equivalence class
- for (size_t j=0; j<lit_new_vars.size(); j++) {
- var_to_eqc[lit_new_vars[j]] = eqcz;
- eqc_to_var[eqcz].push_back(lit_new_vars[j]);
- }
- //add literal to equivalence class
- eqc_to_lit[eqcz].push_back(n);
+ eqc_to_lit.erase(eqc);
+ eqc_active--;
+ }
+ //add variables to equivalence class
+ for (unsigned j=0; j<lit_new_args.size(); j++) {
+ var_to_eqc[lit_new_args[j]] = eqcz;
+ eqc_to_var[eqcz].push_back(lit_new_args[j]);
}
+ //add literal to equivalence class
+ eqc_to_lit[eqcz].push_back(n);
}
- if (eqc_active>1) {
- Trace("clause-split-debug") << "Split clause " << f << std::endl;
- Trace("clause-split-debug") << " Ground literals: " << std::endl;
- for( size_t i=0; i<lits.size(); i++) {
- Trace("clause-split-debug") << " " << lits[i] << std::endl;
+ }
+ if ( eqc_active>1 || !lits.empty() ){
+ Trace("clause-split-debug") << "Split clause " << f << std::endl;
+ Trace("clause-split-debug") << " Ground literals: " << std::endl;
+ for( size_t i=0; i<lits.size(); i++) {
+ Trace("clause-split-debug") << " " << lits[i] << std::endl;
+ }
+ Trace("clause-split-debug") << std::endl;
+ Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
+ for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
+ Trace("clause-split-debug") << " Literals: " << std::endl;
+ for (size_t i=0; i<it->second.size(); i++) {
+ Trace("clause-split-debug") << " " << it->second[i] << std::endl;
}
- Trace("clause-split-debug") << std::endl;
- Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
- for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
- Trace("clause-split-debug") << " Literals: " << std::endl;
- for (size_t i=0; i<it->second.size(); i++) {
- Trace("clause-split-debug") << " " << it->second[i] << std::endl;
- }
- int eqc = it->first;
- Trace("clause-split-debug") << " Variables: " << std::endl;
- for (size_t i=0; i<eqc_to_var[eqc].size(); i++) {
- Trace("clause-split-debug") << " " << eqc_to_var[eqc][i] << std::endl;
- }
- Trace("clause-split-debug") << std::endl;
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]);
- Node body = it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode(OR,it->second);
- Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
- lits.push_back(fa);
+ int eqc = it->first;
+ Trace("clause-split-debug") << " Variables: " << std::endl;
+ for (size_t i=0; i<eqc_to_var[eqc].size(); i++) {
+ Trace("clause-split-debug") << " " << eqc_to_var[eqc][i] << std::endl;
}
- Node nf = NodeManager::currentNM()->mkNode(OR,lits);
- Trace("clause-split-debug") << "Made node : " << nf << std::endl;
- return nf;
+ Trace("clause-split-debug") << std::endl;
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]);
+ Node body = it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( OR, it->second );
+ Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
+ lits.push_back(fa);
}
+ Assert( lits.size()>1 );
+ Node nf = NodeManager::currentNM()->mkNode(OR,lits);
+ Trace("clause-split-debug") << "Made node : " << nf << std::endl;
+ return nf;
}
return f;
}
@@ -925,18 +898,9 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
std::vector< Node > activeArgs;
//if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
- if( options::ceGuidedInst() && !ipl.isNull() ){
- for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
- Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
- if( ipl[i].getKind()==INST_ATTRIBUTE ){
- Node avar = ipl[i][0];
- if( avar.getAttribute(SygusAttribute()) ){
- activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
- }
- }
- }
- }
- if( activeArgs.empty() ){
+ if( options::ceGuidedInst() && TermDb::isSygusConjectureAnnotation( ipl ) ){
+ activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
+ }else{
computeArgVec2( args, activeArgs, body, ipl );
}
if( activeArgs.empty() ){
@@ -953,7 +917,6 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i
}
Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){
- //Notice() << "rewrite quant " << body << std::endl;
if( body.getKind()==FORALL ){
//combine arguments
std::vector< Node > newArgs;
@@ -968,7 +931,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
if( body[0].getKind()==NOT ){
return computeMiniscoping( f, args, body[0][0], ipl );
}else if( body[0].getKind()==AND ){
- if( doMiniscopingNoFreeVar() ){
+ 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() );
@@ -976,7 +939,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
return computeMiniscoping( f, args, t.constructNode(), ipl );
}
}else if( body[0].getKind()==OR ){
- if( doMiniscopingAnd() ){
+ if( options::miniscopeQuant() ){
NodeBuilder<> t(kind::AND);
for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
Node trm = body[0][i].negate();
@@ -986,23 +949,29 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
}
}
}else if( body.getKind()==AND ){
- if( doMiniscopingAnd() ){
+ if( options::miniscopeQuant() ){
//break apart
NodeBuilder<> t(kind::AND);
- for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ for( unsigned i=0; i<body.getNumChildren(); i++ ){
t << computeMiniscoping( f, args, body[i], ipl );
}
Node retVal = t;
return retVal;
}
}else if( body.getKind()==OR ){
- if( doMiniscopingNoFreeVar() ){
+ if( options::quantSplit() ){
+ //splitting subsumes free variable miniscoping, apply it with higher priority
+ Node nf = computeSplit( f, args, body );
+ if( nf!=f ){
+ return nf;
+ }
+ }else if( options::miniscopeQuantFreeVar() ){
Node newBody = body;
NodeBuilder<> body_split(kind::OR);
NodeBuilder<> tb(kind::OR);
- for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ for( unsigned i=0; i<body.getNumChildren(); i++ ){
Node trm = body[i];
- if( hasArg( args, body[i] ) ){
+ if( TermDb::containsTerms( body[i], args ) ){
tb << trm;
}else{
body_split << trm;
@@ -1130,22 +1099,6 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
return mkForAll( args, body, Node::null() );
}
-bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
- return options::miniscopeQuantFreeVar();
-}
-
-bool QuantifiersRewriter::doMiniscopingAnd(){
- if( options::miniscopeQuant() ){
- return true;
- }else{
- if( options::cbqi() ){
- return true;
- }else{
- return false;
- }
- }
-}
-
bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
if( computeOption==COMPUTE_ELIM_SYMBOLS ){
return true;
@@ -1163,14 +1116,10 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
return options::iteDtTesterSplitQuant();
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
- }else if( computeOption==COMPUTE_ELIM_TAUT ){
- return options::elimTautQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
return options::varElimQuant() || options::dtVarExpandQuant();
- }else if( computeOption==COMPUTE_CNF ){
- return false;//return options::cnfQuant() ; FIXME
- }else if( computeOption==COMPUTE_SPLIT ){
- return options::clauseSplit();
+ //}else if( computeOption==COMPUTE_CNF ){
+ // return options::cnfQuant();
}else{
return false;
}
@@ -1206,20 +1155,15 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
n = computeProcessIte2( n );
}else if( computeOption==COMPUTE_PRENEX ){
n = computePrenex( n, args, true );
- }else if( computeOption==COMPUTE_ELIM_TAUT ){
- n = computeElimTaut( n );
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
Node prev;
do{
prev = n;
n = computeVarElimination( n, args, ipl );
}while( prev!=n && !args.empty() );
- }else if( computeOption==COMPUTE_CNF ){
- //n = computeNNF( n );
- n = computeCNF( n, args, defs, false );
- ipl = Node::null();
- }else if( computeOption==COMPUTE_SPLIT ) {
- return computeSplit(f, n, args );
+ //}else if( computeOption==COMPUTE_CNF ){
+ //n = computeCNF( n, args, defs, false );
+ //ipl = Node::null();
}
Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
if( f[1]==n && args.size()==f[0].getNumChildren() ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7db80c84b..0f477b828 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -34,11 +34,9 @@ public:
private:
static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
- static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n );
+ 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 );
- static bool hasArg( std::vector< Node >& args, Node n );
- static bool hasArg1( Node a, Node n );
static Node computeClause( Node n );
static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
private:
@@ -51,8 +49,7 @@ private:
static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
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 computeElimTaut( Node body );
- static Node computeSplit( Node f, Node body, std::vector< Node >& args );
+ static Node computeSplit( Node f, std::vector< Node >& args, Node body );
private:
enum{
COMPUTE_ELIM_SYMBOLS = 0,
@@ -62,10 +59,9 @@ private:
COMPUTE_PROCESS_ITE,
COMPUTE_PROCESS_ITE_2,
COMPUTE_PRENEX,
- COMPUTE_ELIM_TAUT,
COMPUTE_VAR_ELIMINATION,
//COMPUTE_FLATTEN_ARGS_UF,
- COMPUTE_CNF,
+ //COMPUTE_CNF,
COMPUTE_SPLIT,
COMPUTE_LAST
};
@@ -77,8 +73,6 @@ public:
static inline void shutdown() {}
private:
/** options */
- static bool doMiniscopingNoFreeVar();
- static bool doMiniscopingAnd();
static bool doOperation( Node f, bool isNested, int computeOption );
public:
static Node rewriteRewriteRule( Node r );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 52aee392b..9985d3cdb 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1023,7 +1023,7 @@ void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node,
void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
std::vector< Node > vars;
- computeVarContains( n, vars );
+ computeVarContains( n, vars );
for( unsigned j=0; j<vars.size(); j++ ){
Node v = vars[j];
if( v.getAttribute(InstConstantAttribute())==f ){
@@ -1119,7 +1119,7 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){
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] ){
@@ -1624,6 +1624,24 @@ Node TermDb::getFunDefBody( Node q ) {
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;
+}
+
void TermDb::computeAttributes( Node q ) {
Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
if( q.getNumChildren()==3 ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9c5a7cc56..136d77268 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -370,7 +370,7 @@ public:
bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
/** simple check for contains term */
bool containsVtsInfinity( Node n, bool isFree = false );
-
+
private:
//helper for contains term
static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
@@ -379,7 +379,7 @@ private:
public:
/** simple check for contains term */
static bool containsTerm( Node n, Node t );
- /** simple check for contains term */
+ /** simple check for contains term, true if contains at least one term in t */
static bool containsTerms( Node n, std::vector< Node >& t );
/** simple negate */
static Node simpleNegate( Node n );
@@ -403,6 +403,10 @@ public: //general queries concerning quantified formulas wrt modules
static Node getRewriteRule( Node q );
/** is fun def */
static bool isFunDef( Node q );
+ /** 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback