diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-30 12:56:17 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-30 12:56:17 -0500 |
commit | 2f4162877ad455c8c80f60a9bedf0b779b44ecaa (patch) | |
tree | c2a17095f6b2a2523676773def22c59061e475de /src | |
parent | 2bce108ebe25f7a4b5996cf3fde5eda77564f52e (diff) |
Add option in quantifiers for clause splitting
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/options | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 111 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
3 files changed, 115 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e12a7d70f..60f5a171d 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -31,6 +31,9 @@ option varElimQuant --var-elim-quant bool :default false option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas +option clauseSplit --clause-split bool :default false + apply clause splitting to quantified formulas + # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to # forall x. P( x ) => f( S( x ) ) = x diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c6379860e..5c71f6e6f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -537,6 +537,111 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } +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; + + 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; + computeArgs( 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]); + } + } + 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--; + } + if (eqc_active==1 && var_found_count==vars.size()) { + return f; + } + //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); + } + } + 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; + } + 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); + } + Node nf = NodeManager::currentNM()->mkNode(OR,lits); + Trace("clause-split-debug") << "Made node : " << nf << std::endl; + return nf; + } + } + return f; +} + //general method for computing various rewrites Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ if( f.getKind()==FORALL ){ @@ -572,6 +677,8 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ //n = computeNNF( n ); n = computeCNF( n, args, defs, false ); ipl = Node::null(); + }else if( computeOption==COMPUTE_SPLIT ) { + return computeSplit(f, n, args ); } Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; if( f[1]==n && args.size()==f[0].getNumChildren() ){ @@ -811,13 +918,15 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - return true; + return !options::finiteModelFind(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ return false;//return options::cnfQuant() ; + }else if( computeOption==COMPUTE_SPLIT ){ + return options::clauseSplit(); }else{ return false; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 712967bd2..be3e333f3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -50,6 +50,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 computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ COMPUTE_MINISCOPING = 0, @@ -60,6 +61,7 @@ private: COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, + COMPUTE_SPLIT, COMPUTE_LAST }; static Node computeOperation( Node f, int computeOption ); |