From c6c8ba915748e117821996992fd043e2669b59b4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 1 Oct 2012 19:55:15 +0000 Subject: [PATCH] initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver --- src/smt/smt_engine.cpp | 135 ++++++++++++++++++ .../quantifiers/quantifiers_rewriter.cpp | 30 ++-- src/theory/quantifiers/trigger.cpp | 2 +- src/theory/uf/options | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 2 +- 5 files changed, 154 insertions(+), 19 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b968da2e0..5e8cef250 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -261,6 +261,11 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool simplifyAssertions() throw(TypeCheckingException); + /** + * contains quantifiers + */ + bool containsQuantifiers( Node n ); + public: SmtEnginePrivate(SmtEngine& smt) : @@ -352,6 +357,11 @@ public: Node expandDefinitions(TNode n, hash_map& cache) throw(TypeCheckingException); + /** + * pre-skolemize quantifiers + */ + Node preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ); + };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -999,6 +1009,104 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& fvs ){ + Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl; + if( n.getKind()==kind::NOT ){ + Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs ); + return nn.negate(); + }else if( n.getKind()==kind::FORALL ){ + if( polarity ){ + std::vector< Node > children; + children.push_back( n[0] ); + //add children to current scope + std::vector< Node > fvss; + fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + fvss.push_back( n[0][i] ); + } + //process body + children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) ); + if( n.getNumChildren()==3 ){ + children.push_back( n[2] ); + } + //return processed quantifier + return NodeManager::currentNM()->mkNode( kind::FORALL, children ); + }else{ + //process body + Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs ); + //now, substitute skolems for the variables + std::vector< TypeNode > argTypes; + for( int i=0; i<(int)fvs.size(); i++ ){ + argTypes.push_back( fvs[i].getType() ); + } + //calculate the variables and substitution + std::vector< Node > vars; + std::vector< Node > subs; + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + vars.push_back( n[0][i] ); + } + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + //make the new function symbol + if( argTypes.empty() ){ + Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" ); + subs.push_back( s ); + }else{ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); + Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); + NoMatchAttribute nma; + op.setAttribute(nma,true); + std::vector< Node > funcArgs; + funcArgs.push_back( op ); + funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); + subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) ); + } + } + //apply substitution + nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + return nn; + } + }else{ + //check if it contains a quantifier as a subterm + bool containsQuant = false; + if( n.getType().isBoolean() ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( containsQuantifiers( n[i] ) ){ + containsQuant = true; + break; + } + } + } + //if so, we will write this node + if( containsQuant ){ + if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + } + return preSkolemizeQuantifiers( nn, polarity, fvs ); + }else{ + Assert( n.getKind()==AND || n.getKind()==OR ); + std::vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + }else{ + return n; + } + } +} + void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); @@ -1454,6 +1562,20 @@ bool SmtEnginePrivate::simplifyAssertions() return true; } + +bool SmtEnginePrivate::containsQuantifiers( Node n ){ + if( n.getKind()==kind::FORALL ){ + return true; + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( containsQuantifiers( n[i] ) ){ + return true; + } + } + return false; + } +} + Result SmtEngine::check() { Assert(d_fullyInited); Assert(d_pendingPops == 0); @@ -1556,6 +1678,19 @@ void SmtEnginePrivate::processAssertions() { Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; } + if( options::preSkolemQuant() ){ + //apply pre-skolemization to existential quantifiers + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + Node prev = d_assertionsToPreprocess[i]; + std::vector< Node > fvs; + d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) ); + if( prev!=d_assertionsToPreprocess[i] ){ + Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << std::endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << std::endl; + } + } + } + Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); 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++ ){ -- 2.30.2