std::unordered_set<Node> argsSet;
std::unordered_set<Node> nargsSet;
Node q;
- Node nn =
- QuantifiersRewriter::computePrenex(q, n, argsSet, nargsSet, true, true);
+ QuantifiersRewriter qrew(options());
+ Node nn = qrew.computePrenex(q, n, argsSet, nargsSet, true, true);
Assert(n != nn || argsSet.empty());
Assert(n != nn || nargsSet.empty());
if (n != nn)
return out;
}
+QuantifiersRewriter::QuantifiersRewriter(const Options& opts) : d_opts(opts) {}
+
bool QuantifiersRewriter::isLiteral( Node n ){
switch( n.getKind() ){
case NOT:
return true;
}
-void QuantifiersRewriter::addNodeToOrBuilder(Node n, NodeBuilder& t)
-{
- if( n.getKind()==OR ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- t << n[i];
- }
- }else{
- t << n;
- }
-}
-
void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
std::map<Node, bool>& activeMap,
Node n,
return RewriteResponse( status, ret );
}
-bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){
- if( ( k==OR || k==AND ) && options::elimTautQuant() ){
+bool QuantifiersRewriter::addCheckElimChild(std::vector<Node>& children,
+ Node c,
+ Kind k,
+ std::map<Node, bool>& lit_pol,
+ bool& childrenChanged) const
+{
+ if ((k == OR || k == AND) && d_opts.quantifiers.elimTautQuant)
+ {
Node lit = c.getKind()==NOT ? c[0] : c;
bool pol = c.getKind()!=NOT;
std::map< Node, bool >::iterator it = lit_pol.find( lit );
return false;
}
}
- }else{
+ }
+ else
+ {
children.push_back( c );
}
return true;
}
-// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF
-Node QuantifiersRewriter::computeElimSymbols( Node body ) {
+Node QuantifiersRewriter::computeElimSymbols(Node body) const
+{
Kind ok = body.getKind();
Kind k = ok;
bool negAllCh = false;
}
}
-Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){
+Node QuantifiersRewriter::computeProcessTerms(Node body,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& new_conds,
+ Node q,
+ QAttributes& qa) const
+{
std::map< Node, Node > cache;
if( qa.isFunDef() ){
Node h = QuantAttributes::getFunDefHead( q );
return computeProcessTerms2(body, cache, new_vars, new_conds);
}
-Node QuantifiersRewriter::computeProcessTerms2(Node body,
- std::map<Node, Node>& cache,
- std::vector<Node>& new_vars,
- std::vector<Node>& new_conds)
+Node QuantifiersRewriter::computeProcessTerms2(
+ Node body,
+ std::map<Node, Node>& cache,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& new_conds) const
{
NodeManager* nm = NodeManager::currentNM();
Trace("quantifiers-rewrite-term-debug2")
<< "Returning " << ret << " for " << body << std::endl;
// do context-independent rewriting
if (ret.getKind() == EQUAL
- && options::iteLiftQuant() != options::IteLiftQuantMode::NONE)
+ && d_opts.quantifiers.iteLiftQuant != options::IteLiftQuantMode::NONE)
{
for (size_t i = 0; i < 2; i++)
{
if (no.getKind() != ITE)
{
bool doRewrite =
- options::iteLiftQuant() == options::IteLiftQuantMode::ALL;
+ d_opts.quantifiers.iteLiftQuant == options::IteLiftQuantMode::ALL;
std::vector<Node> childrenIte;
childrenIte.push_back(ret[i][0]);
for (size_t j = 1; j <= 2; j++)
Node QuantifiersRewriter::computeCondSplit(Node body,
const std::vector<Node>& args,
- QAttributes& qa)
+ QAttributes& qa) const
{
NodeManager* nm = NodeManager::currentNM();
Kind bk = body.getKind();
- if (options::iteDtTesterSplitQuant() && bk == ITE
+ if (d_opts.quantifiers.iteDtTesterSplitQuant && bk == ITE
&& body[0].getKind() == APPLY_TESTER)
{
Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
return nm->mkNode(AND, conj);
}
}
- if (!options::condVarSplitQuant())
+ if (!d_opts.quantifiers.condVarSplitQuant)
{
return body;
}
if (bk == ITE
|| (bk == EQUAL && body[0].getType().isBoolean()
- && options::condVarSplitQuantAgg()))
+ && d_opts.quantifiers.condVarSplitQuantAgg))
{
Assert(!qa.isFunDef());
bool do_split = false;
// Figure out if we should split
// Currently we split if the aggressive option is set, or
// if the top-level OR is binary.
- if (options::condVarSplitQuantAgg() || size == 2)
+ if (d_opts.quantifiers.condVarSplitQuantAgg || size == 2)
{
do_split = true;
}
bool pol,
std::vector<Node>& args,
std::vector<Node>& vars,
- std::vector<Node>& subs)
+ std::vector<Node>& subs) const
{
if (lit.getKind() == NOT)
{
Trace("var-elim-quant-debug")
<< "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
if (lit.getKind() == APPLY_TESTER && pol && lit[0].getKind() == BOUND_VARIABLE
- && options::dtVarExpandQuant())
+ && d_opts.quantifiers.dtVarExpandQuant)
{
Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
<< std::endl;
}
}
// all eliminations below guarded by varElimQuant()
- if (!options::varElimQuant())
+ if (!d_opts.quantifiers.varElimQuant)
{
return false;
}
bool QuantifiersRewriter::getVarElim(Node body,
std::vector<Node>& args,
std::vector<Node>& vars,
- std::vector<Node>& subs)
+ std::vector<Node>& subs) const
{
return getVarElimInternal(body, body, false, args, vars, subs);
}
bool pol,
std::vector<Node>& args,
std::vector<Node>& vars,
- std::vector<Node>& subs)
+ std::vector<Node>& subs) const
{
Kind nk = n.getKind();
if (nk == NOT)
return getVarElimLit(body, n, pol, args, vars, subs);
}
-bool QuantifiersRewriter::hasVarElim(Node n, bool pol, std::vector<Node>& args)
+bool QuantifiersRewriter::hasVarElim(Node n,
+ bool pol,
+ std::vector<Node>& args) const
{
std::vector< Node > vars;
std::vector< Node > subs;
return ret;
}
-Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){
- if (!options::varElimQuant() && !options::dtVarExpandQuant()
- && !options::varIneqElimQuant())
+Node QuantifiersRewriter::computeVarElimination(Node body,
+ std::vector<Node>& args,
+ QAttributes& qa) const
+{
+ if (!d_opts.quantifiers.varElimQuant && !d_opts.quantifiers.dtVarExpandQuant
+ && !d_opts.quantifiers.varIneqElimQuant)
{
return body;
}
std::vector<Node> vars;
std::vector<Node> subs;
// standard variable elimination
- if (options::varElimQuant())
+ if (d_opts.quantifiers.varElimQuant)
{
getVarElim(body, args, vars, subs);
}
// variable elimination based on one-direction inequalities
- if (vars.empty() && options::varIneqElimQuant())
+ if (vars.empty() && d_opts.quantifiers.varIneqElimQuant)
{
getVarElimIneq(body, args, vars, subs, qa);
}
std::unordered_set<Node>& args,
std::unordered_set<Node>& nargs,
bool pol,
- bool prenexAgg)
+ bool prenexAgg) const
{
NodeManager* nm = NodeManager::currentNM();
Kind k = body.getKind();
if (k == FORALL)
{
if ((pol || prenexAgg)
- && (options::prenexQuantUser() || !QuantAttributes::hasPattern(body)))
+ && (d_opts.quantifiers.prenexQuantUser
+ || !QuantAttributes::hasPattern(body)))
{
std::vector< Node > terms;
std::vector< Node > subs;
return body;
}
-Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
+Node QuantifiersRewriter::computeSplit(std::vector<Node>& args,
+ Node body,
+ QAttributes& qa) const
+{
Assert(body.getKind() == OR);
size_t var_found_count = 0;
size_t eqc_count = 0;
}
//computes miniscoping, also eliminates variables that do not occur free in body
-Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa)
+Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) const
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> args(q[0].begin(), q[0].end());
}else if( body.getKind()==AND ){
// aggressive miniscoping implies that structural miniscoping should
// be applied first
- if (options::miniscopeQuant() || options::aggressiveMiniscopeQuant())
+ if (d_opts.quantifiers.miniscopeQuant
+ || d_opts.quantifiers.aggressiveMiniscopeQuant)
{
BoundVarManager* bvm = nm->getBoundVarManager();
// Break apart the quantifed formula
return retVal;
}
}else if( body.getKind()==OR ){
- if( options::quantSplit() ){
+ if (d_opts.quantifiers.quantSplit)
+ {
//splitting subsumes free variable miniscoping, apply it with higher priority
return computeSplit( args, body, qa );
}
- else if (options::miniscopeQuantFreeVar()
- || options::aggressiveMiniscopeQuant())
+ else if (d_opts.quantifiers.miniscopeQuantFreeVar
+ || d_opts.quantifiers.aggressiveMiniscopeQuant)
{
// aggressive miniscoping implies that free variable miniscoping should
// be applied first
return mkForAll( activeArgs, body, qa );
}
-Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
+Node QuantifiersRewriter::computeAggressiveMiniscoping(std::vector<Node>& args,
+ Node body) const
+{
std::map<Node, std::vector<Node> > varLits;
std::map<Node, std::vector<Node> > litVars;
if (body.getKind() == OR) {
bool QuantifiersRewriter::doOperation(Node q,
RewriteStep computeOption,
- QAttributes& qa)
+ QAttributes& qa) const
{
bool is_strict_trigger =
qa.d_hasPattern
- && options::userPatternsQuant() == options::UserPatMode::STRICT;
+ && d_opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
bool is_std = qa.isStandard() && !is_strict_trigger;
if (computeOption == COMPUTE_ELIM_SYMBOLS)
{
}
else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
{
- return options::aggressiveMiniscopeQuant() && is_std;
+ return d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
}
else if (computeOption == COMPUTE_EXT_REWRITE)
{
- return options::extRewriteQuant();
+ return d_opts.quantifiers.extRewriteQuant;
}
else if (computeOption == COMPUTE_PROCESS_TERMS)
{
- return is_std && options::iteLiftQuant() != options::IteLiftQuantMode::NONE;
+ return is_std
+ && d_opts.quantifiers.iteLiftQuant
+ != options::IteLiftQuantMode::NONE;
}
else if (computeOption == COMPUTE_COND_SPLIT)
{
- return (options::iteDtTesterSplitQuant() || options::condVarSplitQuant())
+ return (d_opts.quantifiers.iteDtTesterSplitQuant
+ || d_opts.quantifiers.condVarSplitQuant)
&& !is_strict_trigger;
}
else if (computeOption == COMPUTE_PRENEX)
{
- return options::prenexQuant() != options::PrenexQuantMode::NONE
- && !options::aggressiveMiniscopeQuant() && is_std;
+ return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
+ && !d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
}
else if (computeOption == COMPUTE_VAR_ELIMINATION)
{
- return (options::varElimQuant() || options::dtVarExpandQuant()) && is_std;
+ return (d_opts.quantifiers.varElimQuant
+ || d_opts.quantifiers.dtVarExpandQuant)
+ && is_std;
}
else
{
//general method for computing various rewrites
Node QuantifiersRewriter::computeOperation(Node f,
RewriteStep computeOption,
- QAttributes& qa)
+ QAttributes& qa) const
{
Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
if (computeOption == COMPUTE_MINISCOPING)
{
- if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
+ if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
{
if( !qa.d_qid_num.isNull() ){
//already processed this, return self
}
else if (computeOption == COMPUTE_PRENEX)
{
- if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
+ if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
{
//will rewrite at preprocess time
return f;
#include "theory/theory_rewriter.h"
namespace cvc5 {
+
+class Options;
+
namespace theory {
namespace quantifiers {
class QuantifiersRewriter : public TheoryRewriter
{
public:
+ QuantifiersRewriter(const Options& opts);
+ /** Pre-rewrite n */
+ RewriteResponse preRewrite(TNode in) override;
+ /** Post-rewrite n */
+ RewriteResponse postRewrite(TNode in) override;
+
static bool isLiteral( Node n );
//-------------------------------------variable elimination utilities
/** is variable elimination
* then this method removes v from args, adds v to vars, adds s to subs, and
* returns true. Otherwise, it returns false.
*/
- static bool getVarElimLit(Node body,
- Node n,
- bool pol,
- std::vector<Node>& args,
- std::vector<Node>& vars,
- std::vector<Node>& subs);
+ bool getVarElimLit(Node body,
+ Node n,
+ bool pol,
+ std::vector<Node>& args,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs) const;
/**
* Get variable eliminate for an equality based on theory-specific reasoning.
*/
* getVarElimLit, we return true. In this case, we update args/vars/subs
* based on eliminating v.
*/
- static bool getVarElim(Node body,
- std::vector<Node>& args,
- std::vector<Node>& vars,
- std::vector<Node>& subs);
+ bool getVarElim(Node body,
+ std::vector<Node>& args,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs) const;
/** has variable elimination
*
* Returns true if n asserted with polarity pol entails a literal for
* which variable elimination is possible.
*/
- static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
+ bool hasVarElim(Node n, bool pol, std::vector<Node>& args) const;
/** compute variable elimination inequality
*
* This method eliminates variables from the body of quantified formula
std::vector<Node>& subs,
QAttributes& qa);
//-------------------------------------end variable elimination utilities
+ /**
+ * Eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR,
+ * and computes NNF.
+ */
+ Node computeElimSymbols(Node body) const;
+ /**
+ * Compute miniscoping in quantified formula q with attributes in qa.
+ */
+ Node computeMiniscoping(Node q, QAttributes& qa) const;
+ Node computeAggressiveMiniscoping(std::vector<Node>& args, Node body) const;
+ /**
+ * This function removes top-level quantifiers from subformulas of body
+ * appearing with overall polarity pol. It adds quantified variables that
+ * appear in positive polarity positions into args, and those at negative
+ * polarity positions in nargs.
+ *
+ * If prenexAgg is true, we ensure that all top-level quantifiers are
+ * eliminated from subformulas. This means that we must expand ITE and
+ * Boolean equalities to ensure that quantifiers are at fixed polarities.
+ *
+ * For example, calling this function on:
+ * (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
+ * would return:
+ * (or (P x z) (not (Q y z)))
+ * and add {x} to args, and {y} to nargs.
+ */
+ Node computePrenex(Node q,
+ Node body,
+ std::unordered_set<Node>& args,
+ std::unordered_set<Node>& nargs,
+ bool pol,
+ bool prenexAgg) const;
+ Node computeSplit(std::vector<Node>& args, Node body, QAttributes& qa) const;
+
+ static bool isPrenexNormalForm(Node n);
+ static Node mkForAll(const std::vector<Node>& args,
+ Node body,
+ QAttributes& qa);
+ static Node mkForall(const std::vector<Node>& args,
+ Node body,
+ bool marked = false);
+ static Node mkForall(const std::vector<Node>& args,
+ Node body,
+ std::vector<Node>& iplc,
+ bool marked = false);
+
private:
/**
* Helper method for getVarElim, called when n has polarity pol in body.
*/
- static bool getVarElimInternal(Node body,
- Node n,
- bool pol,
- std::vector<Node>& args,
- std::vector<Node>& vars,
- std::vector<Node>& subs);
- static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
- static bool addCheckElimChild(std::vector<Node>& children,
- Node c,
- Kind k,
- std::map<Node, bool>& lit_pol,
- bool& childrenChanged);
- static void addNodeToOrBuilder(Node n, NodeBuilder& t);
+ bool getVarElimInternal(Node body,
+ Node n,
+ bool pol,
+ std::vector<Node>& args,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs) const;
+ bool addCheckElimChild(std::vector<Node>& children,
+ Node c,
+ Kind k,
+ std::map<Node, bool>& lit_pol,
+ bool& childrenChanged) const;
static void computeArgs(const std::vector<Node>& args,
std::map<Node, bool>& activeMap,
Node n,
std::vector<Node>& activeArgs,
Node n,
Node ipl);
- static Node computeProcessTerms2(Node body,
- std::map<Node, Node>& cache,
- std::vector<Node>& new_vars,
- std::vector<Node>& new_conds);
+ Node computeProcessTerms2(Node body,
+ std::map<Node, Node>& cache,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& new_conds) const;
static void computeDtTesterIteSplit(
Node n,
std::map<Node, Node>& pcons,
* (forall args'. body'). An example of a variable elimination rewrite is:
* forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
*/
- static Node computeVarElimination(Node body,
- std::vector<Node>& args,
- QAttributes& qa);
+ Node computeVarElimination(Node body,
+ std::vector<Node>& args,
+ QAttributes& qa) const;
//-------------------------------------end variable elimination
//-------------------------------------conditional splitting
/** compute conditional splitting
* ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
* where in each case, x can be eliminated in the first conjunct.
*/
- static Node computeCondSplit(Node body,
- const std::vector<Node>& args,
- QAttributes& qa);
+ Node computeCondSplit(Node body,
+ const std::vector<Node>& args,
+ QAttributes& qa) const;
//-------------------------------------end conditional splitting
//------------------------------------- process terms
/** compute process terms
* is equivalent to:
* forall X, V. ( C => retBody )
*/
- static Node computeProcessTerms(Node body,
- std::vector<Node>& new_vars,
- std::vector<Node>& new_conds,
- Node q,
- QAttributes& qa);
+ Node computeProcessTerms(Node body,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& new_conds,
+ Node q,
+ QAttributes& qa) const;
//------------------------------------- end process terms
//------------------------------------- extended rewrite
/** compute extended rewrite
*/
static Node computeExtendedRewrite(Node q);
//------------------------------------- end extended rewrite
- public:
- static Node computeElimSymbols( Node body );
/**
- * Compute miniscoping in quantified formula q with attributes in qa.
+ * Return true if we should do operation computeOption on quantified formula
+ * q with attributes qa.
*/
- static Node computeMiniscoping(Node q, QAttributes& qa);
- static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
+ bool doOperation(Node q, RewriteStep computeOption, QAttributes& qa) const;
/**
- * This function removes top-level quantifiers from subformulas of body
- * appearing with overall polarity pol. It adds quantified variables that
- * appear in positive polarity positions into args, and those at negative
- * polarity positions in nargs.
- *
- * If prenexAgg is true, we ensure that all top-level quantifiers are
- * eliminated from subformulas. This means that we must expand ITE and
- * Boolean equalities to ensure that quantifiers are at fixed polarities.
- *
- * For example, calling this function on:
- * (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
- * would return:
- * (or (P x z) (not (Q y z)))
- * and add {x} to args, and {y} to nargs.
+ * Return the rewritten form of q after applying operator computeOption to it.
*/
- static Node computePrenex(Node q,
- Node body,
- std::unordered_set<Node>& args,
- std::unordered_set<Node>& nargs,
- bool pol,
- bool prenexAgg);
- static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
-private:
- static Node computeOperation(Node f,
- RewriteStep computeOption,
- QAttributes& qa);
-
-public:
- RewriteResponse preRewrite(TNode in) override;
- RewriteResponse postRewrite(TNode in) override;
-
-private:
- /** options */
- static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);
-
-public:
- static bool isPrenexNormalForm( Node n );
- static Node mkForAll(const std::vector<Node>& args,
- Node body,
- QAttributes& qa);
- static Node mkForall(const std::vector<Node>& args,
- Node body,
- bool marked = false);
- static Node mkForall(const std::vector<Node>& args,
- Node body,
- std::vector<Node>& iplc,
- bool marked = false);
+ Node computeOperation(Node q,
+ RewriteStep computeOption,
+ QAttributes& qa) const;
+ /** Reference to the options */
+ const Options& d_opts;
}; /* class QuantifiersRewriter */
} // namespace quantifiers
std::vector<Node> varsTmp;
std::vector<Node> subsTmp;
- QuantifiersRewriter::getVarElim(body, args, varsTmp, subsTmp);
+ QuantifiersRewriter qrew(options());
+ qrew.getVarElim(body, args, varsTmp, subsTmp);
// if we eliminated a variable, update body and reprocess
if (!varsTmp.empty())
{
OutputChannel& out,
Valuation valuation)
: Theory(THEORY_QUANTIFIERS, env, out, valuation),
+ d_rewriter(env.getOptions()),
d_qstate(env, valuation, logicInfo()),
d_qreg(env),
d_treg(env, d_qstate, d_qreg),
projects / cvc5.git / commitdiff