summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp88
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h9
-rw-r--r--src/theory/quantifiers/term_database.cpp15
-rw-r--r--src/theory/quantifiers/term_database.h4
-rw-r--r--src/theory/quantifiers/trigger.cpp4
5 files changed, 69 insertions, 51 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d25e516fe..dabaa2188 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -185,51 +185,55 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+ 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 body
- Node body = in[1];
- if( in.getKind()==EXISTS ){
- body = body.getKind()==NOT ? body[0] : body.notNode();
- }
//get the instantiation pattern list
Node ipl;
if( in.getNumChildren()==3 ){
ipl = in[2];
}
- bool isNested = in.hasAttribute(NestedQuantAttribute());
- //compute miniscoping first
- Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities)
- if( body!=n ){
- Notice() << "NNF " << body << " -> " << n << std::endl;
- }
- n = computeMiniscoping( args, n, ipl, isNested );
- if( in.getKind()==kind::EXISTS ){
- n = n.getKind()==NOT ? n[0] : n.notNode();
+ //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{
+ bool isNested = in.hasAttribute(NestedQuantAttribute());
+ for( int op=0; op<COMPUTE_LAST; op++ ){
+ if( doOperation( in, isNested, op ) ){
+ ret = computeOperation( in, op );
+ if( ret!=in ){
+ status = REWRITE_AGAIN_FULL;
+ break;
+ }
+ }
+ }
}
- //compute other rewrite options for each produced quantifier
- n = rewriteQuants( n, isNested, true );
//print if changed
- if( in!=n ){
+ if( in!=ret ){
if( in.hasAttribute(NestedQuantAttribute()) ){
- setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+ setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
}
- Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
- Trace("quantifiers-rewrite") << " to " << std::endl;
- Trace("quantifiers-rewrite") << n << std::endl;
if( in.hasAttribute(InstConstantAttribute()) ){
InstConstantAttribute ica;
- n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
+ ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
}
-
- // This is required if substitute in computePrenex() is used.
- return RewriteResponse(REWRITE_AGAIN_FULL, n );
- }else{
- return RewriteResponse(REWRITE_DONE, n );
+ 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);
}
@@ -542,7 +546,10 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
if( f.getNumChildren()==3 ){
ipl = f[2];
}
- if( computeOption==COMPUTE_NNF ){
+ if( computeOption==COMPUTE_MINISCOPING ){
+ //return directly
+ return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
+ }else if( computeOption==COMPUTE_NNF ){
n = computeNNF( n );
}else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
@@ -663,25 +670,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
}
return mkForAll( args, body, ipl );
}
-
-Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){
+/*
+Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){
if( n.getKind()==FORALL ){
- return rewriteQuant( n, isNested, duringRewrite );
+ return rewriteQuant( n, isNested );
}else if( isLiteral( n ) ){
return n;
}else{
NodeBuilder<> tt(n.getKind());
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- tt << rewriteQuants( n[i], isNested, duringRewrite );
+ tt << rewriteQuants( n[i], isNested );
}
return tt.constructNode();
}
}
-Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){
+Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){
Node prev = n;
for( int op=0; op<COMPUTE_LAST; op++ ){
- if( doOperation( n, isNested, op, duringRewrite ) ){
+ if( doOperation( n, isNested, op ) ){
Node prev2 = n;
n = computeOperation( n, op );
if( prev2!=n ){
@@ -695,9 +702,10 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit
return n;
}else{
//rewrite again until fix point is reached
- return rewriteQuant( n, isNested, duringRewrite );
+ return rewriteQuant( n, isNested );
}
}
+*/
bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
return options::miniscopeQuantFreeVar();
@@ -715,17 +723,19 @@ bool QuantifiersRewriter::doMiniscopingAnd(){
}
}
-bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){
- if( computeOption==COMPUTE_NNF ){
+bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
+ if( computeOption==COMPUTE_MINISCOPING ){
+ return true;
+ }else if( computeOption==COMPUTE_NNF ){
return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
}else if( computeOption==COMPUTE_PRE_SKOLEM ){
- return false;//options::preSkolemQuant() && !duringRewrite;
+ return false;//options::preSkolemQuant();
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
return options::varElimQuant();
}else if( computeOption==COMPUTE_CNF ){
- return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind();
+ return false;//return options::cnfQuant() ;
}else{
return false;
}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 636e00774..00301c610 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -51,7 +51,8 @@ private:
static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq );
private:
enum{
- COMPUTE_NNF = 0,
+ COMPUTE_MINISCOPING = 0,
+ COMPUTE_NNF,
COMPUTE_PRE_SKOLEM,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
@@ -69,10 +70,10 @@ private:
/** options */
static bool doMiniscopingNoFreeVar();
static bool doMiniscopingAnd();
- static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true );
+ static bool doOperation( Node f, bool isNested, int computeOption );
public:
- static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true );
- static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true );
+ //static Node rewriteQuants( Node n, bool isNested = false );
+ //static Node rewriteQuant( Node n, bool isNested = false );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 591270ab0..b55e8abdf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,7 +14,7 @@
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/options.h"
@@ -80,7 +80,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
d_op_map[op].push_back( n );
added.insert( n );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
addTerm( n[i], added, withinQuant );
if( options::efficientEMatching() ){
EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher();
@@ -100,10 +100,9 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
}
if( options::eagerInstQuant() ){
if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
int addedLemmas = 0;
- for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){
- addedLemmas += ith->d_op_triggers[op][i]->addTerm( n );
+ for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
+ addedLemmas += d_op_triggers[op][i]->addTerm( n );
}
//Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
@@ -468,3 +467,9 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain
}
}
}
+
+void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
+ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
+ d_op_triggers[op].push_back( tr );
+ }
+}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5060ac1a7..2bae5a043 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -205,6 +205,8 @@ private:
void computeVarContains2( Node n, Node parent );
/** var contains */
std::map< TNode, std::vector< TNode > > d_var_contains;
+ /** triggers for each operator */
+ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
public:
/** compute var contains */
void computeVarContains( Node n );
@@ -214,6 +216,8 @@ public:
void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+ /** register trigger (for eager quantifier instantiation) */
+ void registerTrigger( inst::Trigger* tr, Node op );
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index ae08fe863..67b2e6bd8 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -67,10 +67,8 @@ d_quantEngine( qe ), d_f( f ){
}
//Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
if( options::eagerInstQuant() ){
- Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF );
- uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
for( int i=0; i<(int)d_nodes.size(); i++ ){
- ith->registerTrigger( this, d_nodes[i].getOperator() );
+ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback