diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-01 19:55:15 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-01 19:55:15 +0000 |
commit | c6c8ba915748e117821996992fd043e2669b59b4 (patch) | |
tree | e953453ec5c38f283e46476a8a4c0bc54da079a5 /src/theory | |
parent | f95c6698e5d57b7142b76f29e977168b5bb5ac8c (diff) |
initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/options | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 2 |
4 files changed, 19 insertions, 19 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c6987a85a..17fd3ba41 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -134,7 +134,7 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){ void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){ if( n.getKind()==FORALL || n.getKind()==EXISTS ){ - Debug("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl; + Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl; NestedQuantAttribute nqai; n.setAttribute(nqai,q); } @@ -144,7 +144,7 @@ void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){ } RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { - Debug("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; + Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ if( !in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( in[ 1 ], in ); @@ -174,9 +174,9 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { if( in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); } - Debug("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; - Debug("quantifiers-pre-rewrite") << " to " << std::endl; - Debug("quantifiers-pre-rewrite") << n << std::endl; + Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; + Trace("quantifiers-pre-rewrite") << " to " << std::endl; + Trace("quantifiers-pre-rewrite") << n << std::endl; } return RewriteResponse(REWRITE_DONE, n); } @@ -185,7 +185,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { } RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { - Debug("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; + Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ //get the arguments std::vector< Node > args; @@ -200,7 +200,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { //get the instantiation pattern list Node ipl; if( in.getNumChildren()==3 ){ - ipl = in[2]; + ipl = in[2]; } bool isNested = in.hasAttribute(NestedQuantAttribute()); //compute miniscoping first @@ -219,9 +219,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); } - Debug("quantifiers-rewrite") << "*** rewrite " << in << std::endl; - Debug("quantifiers-rewrite") << " to " << std::endl; - Debug("quantifiers-rewrite") << n << std::endl; + 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()) ); @@ -389,7 +389,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui predArgs.push_back( op ); predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() ); Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs ); - Debug("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl; + Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl; //create the bound var list Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs ); //now, look at the structure of nt @@ -676,9 +676,9 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit Node prev2 = n; n = computeOperation( n, op ); if( prev2!=n ){ - Debug("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl; - Debug("quantifiers-rewrite-op") << " to " << std::endl; - Debug("quantifiers-rewrite-op") << n << std::endl; + Trace("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl; + Trace("quantifiers-rewrite-op") << " to " << std::endl; + Trace("quantifiers-rewrite-op") << n << std::endl; } } } @@ -710,7 +710,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return options::preSkolemQuant() && !duringRewrite; + return false;//options::preSkolemQuant() && !duringRewrite; }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 3bd2945e8..49a1f8332 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -285,7 +285,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ } bool Trigger::isAtomicTrigger( Node n ){ - return n.getKind()==APPLY_UF || n.getKind()==SELECT || n.getKind()==STORE || + return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ diff --git a/src/theory/uf/options b/src/theory/uf/options index 3b6a0818f..f199f6c1b 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -25,7 +25,7 @@ option ufssSmartSplits --uf-ss-smart-split bool :default false use smart splitting heuristic for uf strong solver option ufssModelInference --uf-ss-model-infer bool :default false use model inference method for uf strong solver -option ufssSimpleCliques --uf-ss-simple-cliques bool :default false - add simple clique lemmas for uf strong solver +option ufssExplainedCliques --uf-ss-explained-cliques bool :default false + add explained clique lemmas for uf strong solver endmodule diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 3f82a6948..712d6426b 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1009,7 +1009,7 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } - if( options::ufssSimpleCliques() ){ + if( !options::ufssExplainedCliques() ){ //add as lemma std::vector< Node > eqs; for( int i=0; i<(int)clique.size(); i++ ){ |