diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/quantifiers_preprocess.cpp | 5 | ||||
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 5 | ||||
| -rw-r--r-- | src/proof/proof_rule.h | 2 | ||||
| -rw-r--r-- | src/smt/env_obj.cpp | 7 | ||||
| -rw-r--r-- | src/smt/env_obj.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 31 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_preprocess.cpp | 267 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_preprocess.h | 78 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_registry.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_registry.h | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 192 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 21 | ||||
| -rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/skolemize.h | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 |
18 files changed, 422 insertions, 239 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ba88080b8..5c898b654 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -855,6 +855,8 @@ libcvc5_add_sources( theory/quantifiers/quantifiers_macros.h theory/quantifiers/quantifiers_modules.cpp theory/quantifiers/quantifiers_modules.h + theory/quantifiers/quantifiers_preprocess.cpp + theory/quantifiers/quantifiers_preprocess.h theory/quantifiers/quantifiers_registry.cpp theory/quantifiers/quantifiers_registry.h theory/quantifiers/quantifiers_rewriter.cpp diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index a9363c549..c0bb0ea7f 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -20,7 +20,7 @@ #include "base/output.h" #include "preprocessing/assertion_pipeline.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/rewriter.h" namespace cvc5 { @@ -37,10 +37,11 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( AssertionPipeline* assertionsToPreprocess) { size_t size = assertionsToPreprocess->size(); + quantifiers::QuantifiersPreprocess qp(d_env); for (size_t i = 0; i < size; ++i) { Node prev = (*assertionsToPreprocess)[i]; - TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev); + TrustNode trn = qp.preprocess(prev); if (!trn.isNull()) { Node next = trn.getNode(); diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d105c436a..8194f9f52 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -21,7 +21,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/rewriter.h" @@ -118,6 +118,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, // process eassertions std::vector<Node> processed_assertions; + quantifiers::QuantifiersPreprocess qp(d_env); for (const Node& as : eassertions) { // substitution for this assertion @@ -131,7 +132,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, if (pas.getKind() == FORALL) { // preprocess the quantified formula - TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = qp.preprocess(pas); if (!trn.isNull()) { pas = trn.getNode(); diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index bc2b6437b..7b93e3a55 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -840,7 +840,7 @@ enum class PfRule : uint32_t // Arguments: (F) // --------------------------------------------------------------- // Conclusion: F - // where F is an equality of the form t = QuantifiersRewriter::preprocess(t) + // where F is an equality of the form t = QuantifiersPreprocess::preprocess(t) QUANTIFIERS_PREPROCESS, //================================================= String rules diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index fc50a359b..32c6e4b02 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -24,9 +24,12 @@ namespace cvc5 { EnvObj::EnvObj(Env& env) : d_env(env) {} -Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); } +Node EnvObj::rewrite(TNode node) const +{ + return d_env.getRewriter()->rewrite(node); +} -Node EnvObj::extendedRewrite(TNode node, bool aggr) +Node EnvObj::extendedRewrite(TNode node, bool aggr) const { return d_env.getRewriter()->extendedRewrite(node, aggr); } diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index ebe304dcf..4b907c27b 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -48,12 +48,12 @@ class EnvObj * Rewrite a node. * This is a wrapper around theory::Rewriter::rewrite via Env. */ - Node rewrite(TNode node); + Node rewrite(TNode node) const; /** * Extended rewrite a node. * This is a wrapper around theory::Rewriter::extendedRewrite via Env. */ - Node extendedRewrite(TNode node, bool aggr = true); + Node extendedRewrite(TNode node, bool aggr = true) const; /** Get the current logic information. */ const LogicInfo& logicInfo() const; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 0daf53d2d..9010d4fe1 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -28,7 +28,7 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" @@ -252,7 +252,7 @@ bool Instantiate::addInstantiation(Node q, q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite - TrustNode tpBody = QuantifiersRewriter::preprocess(body, true); + TrustNode tpBody = d_qreg.getPreprocess().preprocess(body, true); if (!tpBody.isNull()) { Assert(tpBody.getKind() == TrustNodeKind::REWRITE); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 34235a193..64a816975 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -93,7 +93,9 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } } -void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { +void QuantPhaseReq::getPolarity( + Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) +{ if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol; newPol = pol; @@ -115,7 +117,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } } -void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { +void QuantPhaseReq::getEntailPolarity( + Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) +{ if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol && pol!=( n.getKind()==OR ); newPol = pol; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 5f91a9488..7ca17b6ad 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -78,8 +78,35 @@ public: std::map< Node, bool > d_phase_reqs_equality; std::map< Node, Node > d_phase_reqs_equality_term; - static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); - static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); + /** + * Get the polarity of the child^th child of n, assuming its polarity + * is given by (hasPol, pol). A term has polarity if it is only relevant + * if asserted with one polarity. Its polarity is (typically) the number + * of negations it is beneath. + */ + static void getPolarity(Node n, + size_t child, + bool hasPol, + bool pol, + bool& newHasPol, + bool& newPol); + + /** + * Get the entailed polarity of the child^th child of n, assuming its + * entailed polarity is given by (hasPol, pol). A term has entailed polarity + * if it must be asserted with a polarity. Its polarity is (typically) the + * number of negations it is beneath. + * + * Entailed polarity and polarity above differ, e.g.: + * (and A B): A and B have true polarity and true entailed polarity + * (or A B): A and B have true polarity and no entailed polarity + */ + static void getEntailPolarity(Node n, + size_t child, + bool hasPol, + bool pol, + bool& newHasPol, + bool& newPol); }; } diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp new file mode 100644 index 000000000..19487bc8d --- /dev/null +++ b/src/theory/quantifiers/quantifiers_preprocess.cpp @@ -0,0 +1,267 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Preprocessor for the theory of quantifiers. + */ + +#include "theory/quantifiers/quantifiers_preprocess.h" + +#include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/skolemize.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +QuantifiersPreprocess::QuantifiersPreprocess(Env& env) : EnvObj(env) {} + +Node QuantifiersPreprocess::computePrenexAgg( + Node n, std::map<Node, Node>& visited) const +{ + std::map<Node, Node>::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + if (!expr::hasClosure(n)) + { + // trivial + return n; + } + NodeManager* nm = NodeManager::currentNM(); + Node ret = n; + if (n.getKind() == NOT) + { + ret = computePrenexAgg(n[0], visited).negate(); + } + else if (n.getKind() == FORALL) + { + std::vector<Node> children; + children.push_back(computePrenexAgg(n[1], visited)); + std::vector<Node> args; + args.insert(args.end(), n[0].begin(), n[0].end()); + // for each child, strip top level quant + for (unsigned i = 0; i < children.size(); i++) + { + if (children[i].getKind() == FORALL) + { + args.insert(args.end(), children[i][0].begin(), children[i][0].end()); + children[i] = children[i][1]; + } + } + // keep the pattern + std::vector<Node> iplc; + if (n.getNumChildren() == 3) + { + iplc.insert(iplc.end(), n[2].begin(), n[2].end()); + } + Node nb = nm->mkOr(children); + ret = QuantifiersRewriter::mkForall(args, nb, iplc, true); + } + else + { + std::unordered_set<Node> argsSet; + std::unordered_set<Node> nargsSet; + Node q; + Node nn = + QuantifiersRewriter::computePrenex(q, n, argsSet, nargsSet, true, true); + Assert(n != nn || argsSet.empty()); + Assert(n != nn || nargsSet.empty()); + if (n != nn) + { + Node nnn = computePrenexAgg(nn, visited); + // merge prenex + if (nnn.getKind() == FORALL) + { + argsSet.insert(nnn[0].begin(), nnn[0].end()); + nnn = nnn[1]; + // pos polarity variables are inner + if (!argsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {argsSet.begin(), argsSet.end()}, nnn, true); + } + argsSet.clear(); + } + else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) + { + nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); + nnn = nnn[0][1].negate(); + } + if (!nargsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) + .negate(); + } + if (!argsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {argsSet.begin(), argsSet.end()}, nnn, true); + } + ret = nnn; + } + } + visited[n] = ret; + return ret; +} + +Node QuantifiersPreprocess::preSkolemizeQuantifiers( + Node n, + bool polarity, + std::vector<TNode>& fvs, + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>& + visited) const +{ + std::pair<Node, bool> key(n, polarity); + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>:: + iterator it = visited.find(key); + if (it != visited.end()) + { + return it->second; + } + NodeManager* nm = NodeManager::currentNM(); + Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() + << std::endl; + if (n.getKind() == FORALL) + { + Node ret = n; + if (n.getNumChildren() == 3) + { + // Do not pre-skolemize quantified formulas with three children. + // This includes non-standard quantified formulas + // like recursive function definitions, or sygus conjectures, and + // quantified formulas with triggers. + } + else if (polarity) + { + if (options().quantifiers.preSkolemQuant + && options().quantifiers.preSkolemQuantNested) + { + std::vector<Node> children; + children.push_back(n[0]); + // add children to current scope + std::vector<TNode> fvss; + fvss.insert(fvss.end(), fvs.begin(), fvs.end()); + fvss.insert(fvss.end(), n[0].begin(), n[0].end()); + // process body in a new context + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction> + visitedSub; + Node pbody = preSkolemizeQuantifiers(n[1], polarity, fvss, visitedSub); + children.push_back(pbody); + // return processed quantifier + ret = nm->mkNode(FORALL, children); + } + } + else + { + // will skolemize current, process body + Node nn = preSkolemizeQuantifiers(n[1], polarity, fvs, visited); + std::vector<Node> sk; + Node sub; + std::vector<unsigned> sub_vars; + // return skolemized body + ret = Skolemize::mkSkolemizedBody(n, nn, fvs, sk, sub, sub_vars); + } + visited[key] = ret; + return ret; + } + // check if it contains a quantifier as a subterm + // if so, we may preprocess this node + if (!expr::hasClosure(n)) + { + visited[key] = n; + return n; + } + Kind k = n.getKind(); + Node ret = n; + Assert(n.getType().isBoolean()); + if (k == ITE || (k == EQUAL && n[0].getType().isBoolean())) + { + if (options().quantifiers.preSkolemQuantAgg) + { + Node nn; + // must remove structure + if (k == ITE) + { + nn = nm->mkNode(AND, + nm->mkNode(OR, n[0].notNode(), n[1]), + nm->mkNode(OR, n[0], n[2])); + } + else if (k == EQUAL) + { + nn = nm->mkNode(AND, + nm->mkNode(OR, n[0].notNode(), n[1]), + nm->mkNode(OR, n[0], n[1].notNode())); + } + ret = preSkolemizeQuantifiers(nn, polarity, fvs, visited); + } + } + else if (k == AND || k == OR || k == NOT || k == IMPLIES) + { + std::vector<Node> children; + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity(n, i, true, polarity, newHasPol, newPol); + Assert(newHasPol); + children.push_back(preSkolemizeQuantifiers(n[i], newPol, fvs, visited)); + } + ret = nm->mkNode(k, children); + } + visited[key] = ret; + return ret; +} + +TrustNode QuantifiersPreprocess::preprocess(Node n, bool isInst) const +{ + Node prev = n; + if (options().quantifiers.preSkolemQuant) + { + if (!isInst || !options().quantifiers.preSkolemQuantNested) + { + Trace("quantifiers-preprocess-debug") + << "Pre-skolemize " << n << "..." << std::endl; + // apply pre-skolemization to existential quantifiers + std::vector<TNode> fvs; + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction> + visited; + n = preSkolemizeQuantifiers(prev, true, fvs, visited); + } + } + // pull all quantifiers globally + if (options().quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL) + { + Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; + std::map<Node, Node> visited; + n = computePrenexAgg(n, visited); + n = rewrite(n); + Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; + } + if (n != prev) + { + Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; + Trace("quantifiers-preprocess") << "..returned " << n << std::endl; + return TrustNode::mkTrustRewrite(prev, n, nullptr); + } + return TrustNode::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_preprocess.h b/src/theory/quantifiers/quantifiers_preprocess.h new file mode 100644 index 000000000..45b7ad07a --- /dev/null +++ b/src/theory/quantifiers/quantifiers_preprocess.h @@ -0,0 +1,78 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Preprocessor for the theory of quantifiers. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H + +#include "proof/trust_node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * Module for doing preprocessing that is pertinent to quantifiers. These + * operations cannot be done in the rewriter since e.g. preskolemization + * depends on knowing the polarity of the position in which quantifiers occur. + */ +class QuantifiersPreprocess : protected EnvObj +{ + public: + QuantifiersPreprocess(Env& env); + /** preprocess + * + * This returns the result of applying simple quantifiers-specific + * pre-processing to n, including but not limited to: + * - pre-skolemization, + * - aggressive prenexing. + * The argument isInst is set to true if n is an instance of a previously + * registered quantified formula. If this flag is true, we do not apply + * certain steps like pre-skolemization since we know they will have no + * effect. + * + * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. + */ + TrustNode preprocess(Node n, bool isInst = false) const; + + private: + using NodePolPairHashFunction = PairHashFunction<Node, bool, std::hash<Node>>; + /** + * Pre-skolemize quantifiers. Return the pre-skolemized form of n. + * + * @param n The formula to preskolemize. + * @param polarity The polarity of n in the input. + * @param fvs The free variables + * @param visited Cache of visited (node, polarity) pairs. + */ + Node preSkolemizeQuantifiers( + Node n, + bool polarity, + std::vector<TNode>& fvs, + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>& + visited) const; + /** + * Apply prenexing aggressively. Returns the prenex normal form of n. + */ + Node computePrenexAgg(Node n, std::map<Node, Node>& visited) const; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 7e3aebbb8..4dc329d8e 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -23,10 +23,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantifiersRegistry::QuantifiersRegistry() +QuantifiersRegistry::QuantifiersRegistry(Env& env) : d_quantAttr(), d_quantBoundInf(options::fmfTypeCompletionThresh(), - options::finiteModelFind()) + options::finiteModelFind()), + d_quantPreproc(env) { } @@ -189,6 +190,10 @@ QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference() { return d_quantBoundInf; } +QuantifiersPreprocess& QuantifiersRegistry::getPreprocess() +{ + return d_quantPreproc; +} Node QuantifiersRegistry::getNameForQuant(Node q) const { diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index ee99a284a..559939bbe 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -22,6 +22,7 @@ #include "theory/quantifiers/quant_bound_inference.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_preprocess.h" namespace cvc5 { namespace theory { @@ -42,7 +43,7 @@ class QuantifiersRegistry : public QuantifiersUtil friend class Instantiate; public: - QuantifiersRegistry(); + QuantifiersRegistry(Env& env); ~QuantifiersRegistry() {} /** * Register quantifier, which allocates the instantiation constants for q. @@ -91,6 +92,8 @@ class QuantifiersRegistry : public QuantifiersUtil QuantAttributes& getQuantAttributes(); /** Get quantifiers bound inference utility */ QuantifiersBoundInference& getQuantifiersBoundInference(); + /** Get the preprocess utility */ + QuantifiersPreprocess& getPreprocess(); /** * Get quantifiers name, which returns a variable corresponding to the name of * quantified formula q if q has a name, or otherwise returns q itself. @@ -126,6 +129,8 @@ class QuantifiersRegistry : public QuantifiersUtil QuantAttributes d_quantAttr; /** The quantifiers bound inference class */ QuantifiersBoundInference d_quantBoundInf; + /** The quantifiers preprocessor utility */ + QuantifiersPreprocess d_quantPreproc; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e5662cdc6..c66324445 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1406,92 +1406,6 @@ Node QuantifiersRewriter::computePrenex(Node q, return body; } -Node QuantifiersRewriter::computePrenexAgg(Node n, - std::map<Node, Node>& visited) -{ - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv!=visited.end() ){ - return itv->second; - } - if (!expr::hasClosure(n)) - { - // trivial - return n; - } - NodeManager* nm = NodeManager::currentNM(); - Node ret = n; - if (n.getKind() == NOT) - { - ret = computePrenexAgg(n[0], visited).negate(); - } - else if (n.getKind() == FORALL) - { - std::vector<Node> children; - children.push_back(computePrenexAgg(n[1], visited)); - std::vector<Node> args; - args.insert(args.end(), n[0].begin(), n[0].end()); - // for each child, strip top level quant - for (unsigned i = 0; i < children.size(); i++) - { - if (children[i].getKind() == FORALL) - { - args.insert(args.end(), children[i][0].begin(), children[i][0].end()); - children[i] = children[i][1]; - } - } - // keep the pattern - std::vector<Node> iplc; - if (n.getNumChildren() == 3) - { - iplc.insert(iplc.end(), n[2].begin(), n[2].end()); - } - Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children); - ret = mkForall(args, nb, iplc, true); - } - else - { - std::unordered_set<Node> argsSet; - std::unordered_set<Node> nargsSet; - Node q; - Node nn = computePrenex(q, n, argsSet, nargsSet, true, true); - Assert(n != nn || argsSet.empty()); - Assert(n != nn || nargsSet.empty()); - if (n != nn) - { - Node nnn = computePrenexAgg(nn, visited); - // merge prenex - if (nnn.getKind() == FORALL) - { - argsSet.insert(nnn[0].begin(), nnn[0].end()); - nnn = nnn[1]; - // pos polarity variables are inner - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - argsSet.clear(); - } - else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) - { - nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); - nnn = nnn[0][1].negate(); - } - if (!nargsSet.empty()) - { - nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) - .negate(); - } - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - ret = nnn; - } - } - visited[n] = ret; - return ret; -} - Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { Assert(body.getKind() == OR); size_t var_found_count = 0; @@ -1999,112 +1913,6 @@ bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { } } -Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ - Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; - if( n.getKind()==kind::NOT ){ - Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs ); - return nn.negate(); - }else if( n.getKind()==kind::FORALL ){ - if (n.getNumChildren() == 3) - { - // Do not pre-skolemize quantified formulas with three children. - // This includes non-standard quantified formulas - // like recursive function definitions, or sygus conjectures, and - // quantified formulas with triggers. - return n; - } - else if (polarity) - { - if( options::preSkolemQuant() && options::preSkolemQuantNested() ){ - vector< Node > children; - children.push_back( n[0] ); - //add children to current scope - std::vector< TypeNode > fvt; - std::vector< TNode > fvss; - fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() ); - fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - fvt.push_back( n[0][i].getType() ); - fvss.push_back( n[0][i] ); - } - //process body - children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) ); - //return processed quantifier - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); - } - }else{ - //process body - Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs ); - std::vector< Node > sk; - Node sub; - std::vector< unsigned > sub_vars; - //return skolemized body - return Skolemize::mkSkolemizedBody( - n, nn, fvTypes, fvs, sk, sub, sub_vars); - } - }else{ - //check if it contains a quantifier as a subterm - //if so, we will write this node - if (expr::hasClosure(n)) - { - if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ - if( options::preSkolemQuantAgg() ){ - 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::EQUAL ){ - 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() ) ); - } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); - } - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - } - return n; -} - -TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) -{ - Node prev = n; - - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } - } - //pull all quantifiers globally - if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) - { - Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - std::map<Node, Node> visited; - n = computePrenexAgg(n, visited); - n = Rewriter::rewrite( n ); - Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; - //Assert( isPrenexNormalForm( n ) ); - } - if( n!=prev ){ - Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; - Trace("quantifiers-preprocess") << "..returned " << n << std::endl; - return TrustNode::mkTrustRewrite(prev, n, nullptr); - } - return TrustNode::null(); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index a7f107573..de5c0b0a4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -273,10 +273,6 @@ class QuantifiersRewriter : public TheoryRewriter std::unordered_set<Node>& nargs, bool pol, bool prenexAgg); - /** - * Apply prenexing aggressively. Returns the prenex normal form of n. - */ - static Node computePrenexAgg(Node n, std::map<Node, Node>& visited); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: static Node computeOperation(Node f, @@ -291,25 +287,8 @@ private: /** options */ static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa); -private: - static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: static bool isPrenexNormalForm( Node n ); - /** preprocess - * - * This returns the result of applying simple quantifiers-specific - * preprocessing to n, including but not limited to: - * - rewrite rule elimination, - * - pre-skolemization, - * - aggressive prenexing. - * The argument isInst is set to true if n is an instance of a previously - * registered quantified formula. If this flag is true, we do not apply - * certain steps like pre-skolemization since we know they will have no - * effect. - * - * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. - */ - static TrustNode preprocess(Node n, bool isInst = false); static Node mkForAll(const std::vector<Node>& args, Node body, QAttributes& qa); diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index fa91b1782..23b66b1de 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -178,13 +178,18 @@ void Skolemize::getSelfSel(const DType& dt, Node Skolemize::mkSkolemizedBody(Node f, Node n, - std::vector<TypeNode>& argTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, std::vector<unsigned>& sub_vars) { NodeManager* nm = NodeManager::currentNM(); + // compute the argument types from the free variables + std::vector<TypeNode> argTypes; + for (TNode v : fvs) + { + argTypes.push_back(v.getType()); + } SkolemManager* sm = nm->getSkolemManager(); Assert(sk.empty() || sk.size() == f[0].getNumChildren()); // calculate the variables and substitution @@ -329,12 +334,11 @@ Node Skolemize::getSkolemizedBody(Node f) std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f); if (it == d_skolem_body.end()) { - std::vector<TypeNode> fvTypes; std::vector<TNode> fvs; Node sub; std::vector<unsigned> sub_vars; - Node ret = mkSkolemizedBody( - f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars); + Node ret = + mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars); d_skolem_body[f] = ret; // store sub quantifier information if (!sub.isNull()) diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index c8e6ec7dd..fbb79f5d2 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -89,10 +89,10 @@ class Skolemize * The skolem constants/functions we generate by this * skolemization are added to sk. * - * The arguments fvTypes and fvs are used if we are + * The argument fvs are used if we are * performing skolemization within a nested quantified * formula. In this case, skolem constants we introduce - * must be parameterized based on fvTypes and must be + * must be parameterized based on the types of fvs and must be * applied to fvs. * * The last two arguments sub and sub_vars are used for @@ -103,7 +103,6 @@ class Skolemize */ static Node mkSkolemizedBody(Node q, Node n, - std::vector<TypeNode>& fvTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 137e25c89..76696c32f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,7 +35,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), d_qstate(env, valuation, logicInfo()), - d_qreg(), + d_qreg(env), d_treg(env, d_qstate, d_qreg), d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) |