This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
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
#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 {
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();
#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"
// process eassertions
std::vector<Node> processed_assertions;
+ quantifiers::QuantifiersPreprocess qp(d_env);
for (const Node& as : eassertions)
{
// substitution for this assertion
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();
// 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
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);
}
* 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;
#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"
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);
}
}
-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;
}
}
-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;
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);
};
}
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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 */
namespace theory {
namespace quantifiers {
-QuantifiersRegistry::QuantifiersRegistry()
+QuantifiersRegistry::QuantifiersRegistry(Env& env)
: d_quantAttr(),
d_quantBoundInf(options::fmfTypeCompletionThresh(),
- options::finiteModelFind())
+ options::finiteModelFind()),
+ d_quantPreproc(env)
{
}
{
return d_quantBoundInf;
}
+QuantifiersPreprocess& QuantifiersRegistry::getPreprocess()
+{
+ return d_quantPreproc;
+}
Node QuantifiersRegistry::getNameForQuant(Node q) const
{
#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 {
friend class Instantiate;
public:
- QuantifiersRegistry();
+ QuantifiersRegistry(Env& env);
~QuantifiersRegistry() {}
/**
* Register quantifier, which allocates the instantiation constants for q.
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.
QuantAttributes d_quantAttr;
/** The quantifiers bound inference class */
QuantifiersBoundInference d_quantBoundInf;
+ /** The quantifiers preprocessor utility */
+ QuantifiersPreprocess d_quantPreproc;
};
} // namespace quantifiers
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;
}
}
-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
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,
/** 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);
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
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())
* 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
*/
static Node mkSkolemizedBody(Node q,
Node n,
- std::vector<TypeNode>& fvTypes,
std::vector<TNode>& fvs,
std::vector<Node>& sk,
Node& sub,
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)
projects / cvc5.git / commitdiff