This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.
It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).
{
// rewrite, this ensures that e.g. the propositional value of
// quantified formulas can be queried
- n = theory::Rewriter::rewrite(n);
+ n = rewrite(n);
Node vn = m->getValue(n);
Assert(vn.isConst());
if (vn.getConst<bool>() == cpol)
// c->explainForConflict(nb);
// }
// Node ret = safeConstructNary(nb);
-// Node rew = Rewriter::rewrite(ret);
+// Node rew = rewrite(ret);
// if(rew.getNumChildren() < ret.getNumChildren()){
// //Debug("approx::") << "explainSet " << ret << " " << rew << endl;
// }
newn = n;
}else if(n.getNumChildren() > 0){
newn = applyReduceVariablesInItes(n);
- newn = Rewriter::rewrite(newn);
+ newn = rewrite(newn);
Assert(Polynomial::isMember(newn));
}else{
newn = n;
//Node n =
Node n = applySubstitutions(binor);
if(n != binor){
- n = Rewriter::rewrite(n);
+ n = rewrite(n);
if(!(n.getKind() == kind::OR &&
n.getNumChildren() == 2 &&
// Prioritize trying a simple rounding of the real solution first,
// it that fails, fall back on original branch and bound strategy.
- Node ub =
- Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1)));
- Node lb =
- Rewriter::rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1)));
+ Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1)));
+ Node lb = rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1)));
Node right = nm->mkNode(OR, ub, lb);
Node rawEq = nm->mkNode(EQUAL, var, mkRationalNode(nearest));
- Node eq = Rewriter::rewrite(rawEq);
+ Node eq = rewrite(rawEq);
// Also preprocess it before we send it out. This is important since
// arithmetic may prefer eliminating equalities.
TrustNode teq;
}
else
{
- Node ub = Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor)));
+ Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor)));
Node lb = ub.notNode();
if (proofsEnabled())
{
return true;
}
- Node rewritten = Rewriter::rewrite(x);
+ Node rewritten = rewrite(x);
//Need to still propagate this!
if(rewritten.getKind() == kind::CONST_BOOLEAN){
/* This maps the node a theory engine will request on an explain call to
* to its corresponding PropUnit.
* This is node is potentially both the propagation or
- * Rewriter::rewrite(propagation).
+ * rewrite(propagation).
*/
typedef context::CDHashMap<Node, size_t> ExplainMap;
ExplainMap d_explanationMap;
bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
{
- Node rewritten = Rewriter::rewrite(lem);
+ Node rewritten = rewrite(lem);
return TheoryInferenceManager::hasCachedLemma(rewritten, p);
}
bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
{
- Node rewritten = Rewriter::rewrite(lem);
+ Node rewritten = rewrite(lem);
return TheoryInferenceManager::cacheLemma(rewritten, p);
}
if (options().arith.nlExtEntailConflicts)
{
Node ch_lemma = lem.d_node.negate();
- ch_lemma = Rewriter::rewrite(ch_lemma);
+ ch_lemma = rewrite(ch_lemma);
Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
<< ch_lemma << "..." << std::endl;
namespace arith {
namespace nl {
-FactoringCheck::FactoringCheck(ExtState* data) : d_data(data)
+FactoringCheck::FactoringCheck(Env& env, ExtState* data)
+ : EnvObj(env), d_data(data)
{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_one = NodeManager::currentNM()->mkConst(Rational(1));
children.pop_back();
}
children[i] = itm->first[i];
- val = Rewriter::rewrite(val);
+ val = rewrite(val);
factor_to_mono[itm->first[i]].push_back(val);
factor_to_mono_orig[itm->first[i]].push_back(itm->first);
}
continue;
}
Node sum = nm->mkNode(Kind::PLUS, itf->second);
- sum = Rewriter::rewrite(sum);
+ sum = rewrite(sum);
Trace("nl-ext-factor")
<< "* Factored sum for " << x << " : " << sum << std::endl;
Trace("nl-ext-factor")
<< "...factored polynomial : " << polyn << std::endl;
Node conc_lit = nm->mkNode(atom.getKind(), polyn, d_zero);
- conc_lit = Rewriter::rewrite(conc_lit);
+ conc_lit = rewrite(conc_lit);
if (!polarity)
{
conc_lit = conc_lit.negate();
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
struct ExtState;
-class FactoringCheck
+class FactoringCheck : protected EnvObj
{
public:
- FactoringCheck(ExtState* data);
+ FactoringCheck(Env& env, ExtState* data);
/** check factoring
*
}
} // namespace
-MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data)
- : d_data(data), d_cdb(d_data->d_mdb)
+MonomialBoundsCheck::MonomialBoundsCheck(Env& env, ExtState* data)
+ : EnvObj(env), d_data(data), d_cdb(d_data->d_mdb)
{
}
Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
Trace("nl-ext-bound-debug") << " " << infer << std::endl;
- Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer));
+ Node infer_mv =
+ d_data->d_model.computeAbstractModelValue(rewrite(infer));
Trace("nl-ext-bound-debug")
<< " ...infer model value is " << infer_mv << std::endl;
if (infer_mv == d_data->d_false)
mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero),
d_ci_exp[x][coeff][rhs]);
Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer);
- Node iblem_rw = Rewriter::rewrite(iblem);
+ Node iblem_rw = rewrite(iblem);
bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms);
Trace("nl-ext-bound-lemma")
<< "*** Bound inference lemma : " << iblem_rw
{
Node rhs_a = itcar->first;
Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a);
- rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
+ rhs_a_res_base = rewrite(rhs_a_res_base);
if (hasNewMonomials(rhs_a_res_base, d_data->d_ms))
{
continue;
Node rhs_b = itcbr->first;
Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b);
rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
- rhs_b_res = Rewriter::rewrite(rhs_b_res);
+ rhs_b_res = rewrite(rhs_b_res);
if (hasNewMonomials(rhs_b_res, d_data->d_ms))
{
continue;
"(pre-rewrite) "
": "
<< rblem << std::endl;
- rblem = Rewriter::rewrite(rblem);
+ rblem = rewrite(rblem);
Trace("nl-ext-rbound-lemma")
<< "Resolution bound lemma : " << rblem << std::endl;
d_data->d_im.addPendingLemma(
#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/ext/constraint.h"
namespace cvc5 {
struct ExtState;
-class MonomialBoundsCheck
+class MonomialBoundsCheck : protected EnvObj
{
public:
- MonomialBoundsCheck(ExtState* data);
+ MonomialBoundsCheck(Env& env, ExtState* data);
void init();
namespace arith {
namespace nl {
-MonomialCheck::MonomialCheck(ExtState* data) : d_data(data)
+MonomialCheck::MonomialCheck(Env& env, ExtState* data)
+ : EnvObj(env), d_data(data)
{
d_order_points.push_back(d_data->d_neg_one);
d_order_points.push_back(d_data->d_zero);
#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/ext/monomial.h"
#include "theory/theory_inference.h"
struct ExtState;
-class MonomialCheck
+class MonomialCheck : protected EnvObj
{
public:
- MonomialCheck(ExtState* data);
+ MonomialCheck(Env& env, ExtState* data);
void init(const std::vector<Node>& xts);
namespace arith {
namespace nl {
-SplitZeroCheck::SplitZeroCheck(ExtState* data)
- : d_data(data), d_zero_split(d_data->d_env.getUserContext())
+SplitZeroCheck::SplitZeroCheck(Env& env, ExtState* data)
+ : EnvObj(env), d_data(data), d_zero_split(d_data->d_env.getUserContext())
{
}
Node v = d_data->d_ms_vars[i];
if (d_zero_split.insert(v))
{
- Node eq = Rewriter::rewrite(v.eqNode(d_data->d_zero));
+ Node eq = rewrite(v.eqNode(d_data->d_zero));
Node lem = eq.orNode(eq.negate());
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
#ifndef CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
#define CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
-#include "expr/node.h"
#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
struct ExtState;
-class SplitZeroCheck
+class SplitZeroCheck : protected EnvObj
{
public:
- SplitZeroCheck(ExtState* data);
+ SplitZeroCheck(Env& env, ExtState* data);
/** check split zero
*
namespace arith {
namespace nl {
-TangentPlaneCheck::TangentPlaneCheck(ExtState* data) : d_data(data) {}
+TangentPlaneCheck::TangentPlaneCheck(Env& env, ExtState* data)
+ : EnvObj(env), d_data(data)
+{
+}
void TangentPlaneCheck::check(bool asWaitingLemmas)
{
{
Node do_extend = nm->mkNode(
(p == 1 || p == 3) ? Kind::GT : Kind::LT, curr_v, pt_v);
- do_extend = Rewriter::rewrite(do_extend);
+ do_extend = rewrite(do_extend);
if (do_extend == d_data->d_true)
{
for (unsigned q = 0; q < 2; q++)
#include <map>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
struct ExtState;
-class TangentPlaneCheck
+class TangentPlaneCheck : protected EnvObj
{
public:
- TangentPlaneCheck(ExtState* data);
+ TangentPlaneCheck(Env& env, ExtState* data);
/** check tangent planes
*
NodeManager* nm = NodeManager::currentNM();
Node iToBvOp = nm->mkConst(IntToBitVector(k));
Node bn = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvOp, n);
- return Rewriter::rewrite(bn);
+ return rewrite(bn);
}
Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const
NodeManager* nm = NodeManager::currentNM();
Node iAndOp = nm->mkConst(IntAnd(k));
Node ret = nm->mkNode(IAND, iAndOp, x, y);
- ret = Rewriter::rewrite(ret);
+ ret = rewrite(ret);
return ret;
}
Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const
{
Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y)));
- ret = Rewriter::rewrite(ret);
+ ret = rewrite(ret);
return ret;
}
{
NodeManager* nm = NodeManager::currentNM();
Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x);
- ret = Rewriter::rewrite(ret);
+ ret = rewrite(ret);
return ret;
}
NodeManager* nm = NodeManager::currentNM();
Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY);
- valC = Rewriter::rewrite(valC);
+ valC = rewrite(valC);
Node lem = nm->mkNode(
IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC));
}
} // namespace
+ICPSolver::ICPSolver(Env& env, InferenceManager& im)
+ : EnvObj(env), d_im(im), d_state(d_mapper)
+{
+}
+
std::vector<Node> ICPSolver::collectVariables(const Node& n) const
{
std::unordered_set<TNode> tmp;
std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
{
- Node tmp = Rewriter::rewrite(n);
+ Node tmp = rewrite(n);
if (tmp.isConst())
{
return {};
{
Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
Trace("nl-icp") << premise << " => " << c << std::endl;
- Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
+ Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
if (lemma.isConst())
{
Assert(lemma == nm->mkConst<bool>(true));
{
Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
Trace("nl-icp") << premise << " => " << c << std::endl;
- Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
+ Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
if (lemma.isConst())
{
Assert(lemma == nm->mkConst<bool>(true));
#endif /* CVC5_POLY_IMP */
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/bound_inference.h"
#include "theory/arith/nl/icp/candidate.h"
#include "theory/arith/nl/icp/contraction_origins.h"
* These contractions can yield to a conflict (if the interval of some variable
* becomes empty) or shrink the search space for a variable.
*/
-class ICPSolver
+class ICPSolver : protected EnvObj
{
+ public:
+ ICPSolver(Env& env, InferenceManager& im);
+ /** Reset this solver for the next theory call */
+ void reset(const std::vector<Node>& assertions);
+
+ /**
+ * Performs a full ICP check.
+ */
+ void check();
+
+ private:
/**
* This encapsulates the state of the ICP solver that is local to a single
* theory call. It contains the variable bounds and candidates derived from
* is constructed.
*/
std::vector<Node> generateLemmas() const;
-
- public:
- ICPSolver(InferenceManager& im) : d_im(im), d_state(d_mapper) {}
- /** Reset this solver for the next theory call */
- void reset(const std::vector<Node>& assertions);
-
- /**
- * Performs a full ICP check.
- */
- void check();
};
#else /* CVC5_POLY_IMP */
-class ICPSolver
+class ICPSolver : protected EnvObj
{
public:
- ICPSolver(InferenceManager& im) {}
+ ICPSolver(Env& env, InferenceManager& im) : EnvObj(env) {}
void reset(const std::vector<Node>& assertions);
void check();
};
d_extTheoryCb(state.getEqualityEngine()),
d_extTheory(env, d_extTheoryCb, d_im),
d_model(),
- d_trSlv(d_im, d_model, d_env),
+ d_trSlv(d_env, d_im, d_model),
d_extState(d_im, d_model, d_env),
- d_factoringSlv(&d_extState),
- d_monomialBoundsSlv(&d_extState),
- d_monomialSlv(&d_extState),
- d_splitZeroSlv(&d_extState),
- d_tangentPlaneSlv(&d_extState),
+ d_factoringSlv(d_env, &d_extState),
+ d_monomialBoundsSlv(d_env, &d_extState),
+ d_monomialSlv(d_env, &d_extState),
+ d_splitZeroSlv(d_env, &d_extState),
+ d_tangentPlaneSlv(d_env, &d_extState),
d_cadSlv(d_env, d_im, d_model),
- d_icpSlv(d_im),
+ d_icpSlv(d_env, d_im),
d_iandSlv(env, d_im, state, d_model),
d_pow2Slv(env, d_im, state, d_model)
{
{
for (const Node& eq : shared_term_value_splits)
{
- Node req = Rewriter::rewrite(eq);
+ Node req = rewrite(eq);
Node literal = d_containing.getValuation().ensureLiteral(req);
d_containing.getOutputChannel().requirePhase(literal, true);
Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
NodeManager* nm = NodeManager::currentNM();
Node valC = nm->mkNode(POW2, valX);
- valC = Rewriter::rewrite(valC);
+ valC = rewrite(valC);
Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC));
return lem;
namespace nl {
namespace transcendental {
-ExponentialSolver::ExponentialSolver(TranscendentalState* tstate)
- : d_data(tstate)
+ExponentialSolver::ExponentialSolver(Env& env, TranscendentalState* tstate)
+ : EnvObj(env), d_data(tstate)
{
}
nm->mkNode(Kind::GEQ, e, poly_approx));
Trace("nl-ext-exp") << "*** Tangent plane lemma (pre-rewrite): " << lem
<< std::endl;
- lem = Rewriter::rewrite(lem);
+ lem = rewrite(lem);
Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl;
Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
// Figure 3 : line 9
if (bounds.first.isNull())
{
// pick c-1
- bounds.first = Rewriter::rewrite(
+ bounds.first = rewrite(
NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
}
if (bounds.second.isNull())
{
// pick c+1
- bounds.second = Rewriter::rewrite(
+ bounds.second = rewrite(
NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one));
}
return bounds;
#include <map>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* It's main functionality are methods that implement lemma schemas below,
* which return a set of lemmas that should be sent on the output channel.
*/
-class ExponentialSolver
+class ExponentialSolver : protected EnvObj
{
public:
- ExponentialSolver(TranscendentalState* tstate);
+ ExponentialSolver(Env& env, TranscendentalState* tstate);
~ExponentialSolver();
/**
}
} // namespace
-SineSolver::SineSolver(TranscendentalState* tstate) : d_data(tstate) {}
+SineSolver::SineSolver(Env& env, TranscendentalState* tstate)
+ : EnvObj(env), d_data(tstate)
+{
+}
SineSolver::~SineSolver() {}
d_tf_initial_refine[t] = true;
Node symn = nm->mkNode(Kind::SINE,
nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0]));
- symn = Rewriter::rewrite(symn);
+ symn = rewrite(symn);
// Can assume it is its own master since phase is split over 0,
// hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
d_data->d_trMaster[symn] = symn;
Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem
<< std::endl;
- lem = Rewriter::rewrite(lem);
+ lem = rewrite(lem);
Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
// Figure 3 : line 9
#include <map>
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/transcendental/transcendental_state.h"
namespace cvc5 {
* It's main functionality are methods that implement lemma schemas below,
* which return a set of lemmas that should be sent on the output channel.
*/
-class SineSolver
+class SineSolver : protected EnvObj
{
public:
- SineSolver(TranscendentalState* tstate);
+ SineSolver(Env& env, TranscendentalState* tstate);
~SineSolver();
/**
namespace nl {
namespace transcendental {
-TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
- NlModel& m,
- Env& env)
- : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
+TranscendentalSolver::TranscendentalSolver(Env& env,
+ InferenceManager& im,
+ NlModel& m)
+ : EnvObj(env),
+ d_tstate(im, m, env),
+ d_expSlv(env, &d_tstate),
+ d_sineSlv(env, &d_tstate)
{
d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
}
if (!subs.empty())
{
pa = arithSubstitute(pa, subs);
- pa = Rewriter::rewrite(pa);
+ pa = rewrite(pa);
}
if (!pa.isConst() || !pa.getConst<bool>())
{
Assert(v_pab.isConst());
Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
Trace("nl-trans") << "...compare : " << comp << std::endl;
- Node compr = Rewriter::rewrite(comp);
+ Node compr = rewrite(comp);
Trace("nl-trans") << "...got : " << compr << std::endl;
if (compr == d_tstate.d_true)
{
- poly_approx_c = Rewriter::rewrite(v_pab);
+ poly_approx_c = rewrite(v_pab);
// beyond the bounds
if (r == 0)
{
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/transcendental/exponential_solver.h"
#include "theory/arith/nl/transcendental/sine_solver.h"
#include "theory/arith/nl/transcendental/transcendental_state.h"
* It's main functionality are methods that implement lemma schemas below,
* which return a set of lemmas that should be sent on the output channel.
*/
-class TranscendentalSolver
+class TranscendentalSolver : protected EnvObj
{
public:
- TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env);
+ TranscendentalSolver(Env& env, InferenceManager& im, NlModel& m);
~TranscendentalSolver();
/** init last call
case COTANGENT:
{
// these are eliminated by rewriting
- return Rewriter::rewrite(node);
+ return rewrite(node);
break;
}
case TO_INTEGER:
// not eliminating total operators
return node;
}
- Node den = Rewriter::rewrite(node[1]);
- Node num = Rewriter::rewrite(node[0]);
+ Node den = rewrite(node[1]);
+ Node num = rewrite(node[0]);
Node rw = nm->mkNode(k, num, den);
Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
Node lem;
if (num.isConst() || rat == 0)
{
// just rewrite
- return Rewriter::rewrite(node);
+ return rewrite(node);
}
if (rat > 0)
{
// not eliminating total operators
return node;
}
- Node num = Rewriter::rewrite(node[0]);
- Node den = Rewriter::rewrite(node[1]);
+ Node num = rewrite(node[0]);
+ Node den = rewrite(node[1]);
if (den.isConst())
{
// No need to eliminate here, can eliminate via rewriting later.
}
case DIVISION:
{
- Node num = Rewriter::rewrite(node[0]);
- Node den = Rewriter::rewrite(node[1]);
+ Node num = rewrite(node[0]);
+ Node den = rewrite(node[1]);
Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
case INTS_DIVISION:
{
// partial function: integer div
- Node num = Rewriter::rewrite(node[0]);
- Node den = Rewriter::rewrite(node[1]);
+ Node num = rewrite(node[0]);
+ Node den = rewrite(node[1]);
Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
case INTS_MODULUS:
{
// partial function: mod
- Node num = Rewriter::rewrite(node[0]);
- Node den = Rewriter::rewrite(node[1]);
+ Node num = rewrite(node[0]);
+ Node den = rewrite(node[1]);
Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
Assert(atom[0].getType().isReal());
Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
- Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+ Node rewritten = rewrite(leq.andNode(geq));
Debug("arith::preprocess")
<< "arith::preprocess() : returning " << rewritten << std::endl;
// don't need to rewrite terms since rewritten is not a non-standard op
{
return d_internal->getEqualityStatus(a,b);
}
- Node aval = Rewriter::rewrite(a.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
- Node bval = Rewriter::rewrite(b.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
+ Node aval =
+ rewrite(a.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
+ Node bval =
+ rewrite(b.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
if (aval == bval)
{
return EQUALITY_TRUE_IN_MODEL;
// ax + p = c -> (ax + p) -ax - c = -ax
// x = (p - ax - c) * -1/a
// Add the substitution if not recursive
- Assert(elim == Rewriter::rewrite(elim));
+ Assert(elim == rewrite(elim));
if (right.size() > options().arith.ppAssertMaxSubSize)
{
Comparison leq = Comparison::mkComparison(LEQ, p, c);
Comparison geq = Comparison::mkComparison(GEQ, p, c);
Node lemma = NodeManager::currentNM()->mkNode(OR, leq.getNode(), geq.getNode());
- Node rewrittenLemma = Rewriter::rewrite(lemma);
+ Node rewrittenLemma = rewrite(lemma);
Debug("arith::dio::ex") << "dioCutting found the plane: " << plane.getNode() << endl;
Debug("arith::dio::ex") << "resulting in the cut: " << lemma << endl;
Debug("arith::dio::ex") << "rewritten " << rewrittenLemma << endl;
bool isDistinct = simpleKind == DISTINCT;
Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
Assert(!isSetup(eq));
- Node reEq = Rewriter::rewrite(eq);
+ Node reEq = rewrite(eq);
Debug("arith::distinct::const") << "Assertion: " << assertion << std::endl;
Debug("arith::distinct::const") << "Eq : " << eq << std::endl;
Debug("arith::distinct::const") << "reEq : " << reEq << std::endl;
Assert(k == kind::LEQ || k == kind::GEQ);
Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs));
- Node rewritten = Rewriter::rewrite(comparison);
+ Node rewritten = rewrite(comparison);
if(!(Comparison::isNormalAtom(rewritten))){
return make_pair(NullConstraint, added);
}
return replayGetConstraint(lhs, k, rhs, ci.getKlass() == BranchCutKlass);
}
-// Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv, Kind k){
+// Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv,
+// Kind k){
// NodeManager* nm = NodeManager::currentNM();
// Node sumLhs = toSumNode(vars, dv.lhs);
// Node ineq = nm->mkNode(k, sumLhs, mkRationalNode(dv.rhs) );
-// Node lit = Rewriter::rewrite(ineq);
+// Node lit = rewrite(ineq);
// return lit;
// }
Rational fl(maybe_value.value().floor());
NodeManager* nm = NodeManager::currentNM();
Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl));
- Node norm = Rewriter::rewrite(leq);
+ Node norm = rewrite(leq);
return norm;
}
}
NodeManager* nm = NodeManager::currentNM();
Node ineq = nm->mkNode(k, sum, rhs);
- return Rewriter::rewrite(ineq);
+ return rewrite(ineq);
}
return Node::null();
}
const ConstraintCPVec& exp = cut->getExplanation();
Node asLemma = Constraint::externalExplainByAssertions(exp);
- Node implied = Rewriter::rewrite(cutConstraint);
+ Node implied = rewrite(cutConstraint);
anythingnew = anythingnew || !isSatLiteral(implied);
Node implication = asLemma.impNode(implied);
++d_statistics.d_panicBranches;
TrustNode branch = branchIntegerVariable(canBranch);
Assert(branch.getNode().getKind() == kind::OR);
- Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
+ Node rwbranch = rewrite(branch.getNode()[0]);
if (!isSatLiteral(rwbranch))
{
d_approxCuts.push_back(branch);
TrustNode lemma = front->split();
++(d_statistics.d_statDisequalitySplits);
- Debug("arith::lemma")
- << "Now " << Rewriter::rewrite(lemma.getNode()) << endl;
+ Debug("arith::lemma") << "Now " << rewrite(lemma.getNode()) << endl;
outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ);
- //cout << "Now " << Rewriter::rewrite(lemma) << endl;
+ // cout << "Now " << rewrite(lemma) << endl;
splitSomething = true;
}else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
Debug("arith::eq") << "can drop as less than lb" << front << endl;
//Currently if the flag is set this came from an equality detected by the
//equality engine in the the difference manager.
- Node normalized = Rewriter::rewrite(toProp);
+ Node normalized = rewrite(toProp);
ConstraintP constraint = d_constraintDatabase.lookup(normalized);
if(constraint == NullConstraint){
if(!successful) { return make_pair(false, Node::null()); }
if(dp.getKind() == CONST_RATIONAL){
- Node eval = Rewriter::rewrite(lit);
+ Node eval = rewrite(lit);
Assert(eval.getKind() == kind::CONST_BOOLEAN);
// if true, true is an acceptable explaination
// if false, the node is uninterpreted and eval can be forgotten
Node lit = mkLiteral(d_literals.size());
if (!lit.isNull())
{
- lit = Rewriter::rewrite(lit);
+ lit = rewrite(lit);
}
d_literals.push_back(lit);
}
if (checkCache)
{
// check if it is unique up to rewriting
- Node lemr = Rewriter::rewrite(lem);
+ Node lemr = rewrite(lem);
if (hasCachedLemma(lemr, p))
{
return false;
}else{
rsg = lhs.eqNode( rhs );
}
- rsg = Rewriter::rewrite( rsg );
+ rsg = rewrite(rsg);
d_conjectures.push_back( rsg );
d_eq_conjectures[lhs].push_back( rhs );
d_eq_conjectures[rhs].push_back( lhs );
Result ExprMiner::doCheck(Node query)
{
- Node queryr = Rewriter::rewrite(query);
+ Node queryr = rewrite(query);
if (queryr.isConst())
{
if (!queryr.getConst<bool>())
}
}
Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
- curr = Rewriter::rewrite(curr);
+ curr = rewrite(curr);
return nm->mkNode(LAMBDA, boundVarList, curr);
}
Node FunDefEvaluator::evaluateDefinitions(Node n) const
{
// should do standard rewrite before this call
- Assert(Rewriter::rewrite(n) == n);
+ Assert(rewrite(n) == n);
Trace("fd-eval") << "FunDefEvaluator: evaluateDefinitions " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
std::unordered_map<TNode, unsigned> funDefCount;
if (childChanged)
{
ret = nm->mkNode(cur.getKind(), children);
- ret = Rewriter::rewrite(ret);
+ ret = rewrite(ret);
}
Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
visited[cur] = ret;
std::map<Node, Node>::iterator itpe = d_hoPurifyToEq.find(pp.first);
if (itpe == d_hoPurifyToEq.end())
{
- eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
+ eq = rewrite(pp.first.eqNode(pp.second));
d_hoPurifyToEq[pp.first] = eq;
}
else
}
Trace("sygus-ccore-init") << " body : " << body << std::endl;
- TransitionInference ti;
+ TransitionInference ti(d_env);
ti.process(body, conj[0][0]);
if (!ti.isComplete())
sc = sc[1];
}
Node scb = TermUtil::simpleNegate(sc);
- TransitionInference tisc;
+ TransitionInference tisc(d_env);
tisc.process(scb, conj[0][0]);
Node scTrans = ti.getTransitionRelation();
Trace("sygus-ccore-init")
namespace theory {
namespace quantifiers {
-SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
+SygusEvalUnfold::SygusEvalUnfold(Env& env, TermDbSygus* tds)
+ : EnvObj(env), d_tds(tds)
+{
+}
void SygusEvalUnfold::registerEvalTerm(Node n)
{
TNode at = a;
TNode vt = v;
Node vn = n.substitute(at, vt);
- vn = Rewriter::rewrite(vn);
+ vn = rewrite(vn);
unsigned start = d_node_mv_args_proc[n][vn];
// get explanation in terms of testers
std::vector<Node> antec_exp;
Trace("sygus-eval-unfold-debug")
<< "Applied sygus args : " << ret << std::endl;
// rewrite
- ret = Rewriter::rewrite(ret);
+ ret = rewrite(ret);
Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
return ret;
}
#define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
#include <map>
+
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/sygus_invariance.h"
namespace cvc5 {
* unfold" applications of eval based on the model values of evaluation heads
* in refinement lemmas.
*/
-class SygusEvalUnfold
+class SygusEvalUnfold : protected EnvObj
{
public:
- SygusEvalUnfold(TermDbSygus* tds);
+ SygusEvalUnfold(Env& env, TermDbSygus* tds);
~SygusEvalUnfold() {}
/** register evaluation term
*
{
continue;
}
- Node builtin = Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz));
+ Node builtin = rewrite(datatypes::utils::sygusToBuiltin(sz));
// if enumerated term does not contain free variables, then its
// corresponding obligation can be solved immediately
if (sz.isConst())
matches.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
// try to match the builtin term with the pattern sz
- if (expr::match(
- Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)), t, matches))
+ if (expr::match(rewrite(datatypes::utils::sygusToBuiltin(sz)), t, matches))
{
// the bound variables z generated by the enumerators are reused across
// enumerated terms, so we need to replace them with our own skolems
for (const Node& sygusTerm : pair.second)
{
- Trace("sygus-rcons") << " "
- << Rewriter::rewrite(
- datatypes::utils::sygusToBuiltin(sygusTerm))
- .toString()
- << std::endl;
+ Trace("sygus-rcons")
+ << " "
+ << rewrite(datatypes::utils::sygusToBuiltin(sygusTerm)).toString()
+ << std::endl;
}
Trace("sygus-rcons") << " ]" << std::endl;
d_treg(tr),
d_stats(s),
d_tds(tr.getTermDatabaseSygus()),
- d_verify(options(), logicInfo(), d_tds),
+ d_verify(env, d_tds),
d_hasSolution(false),
d_ceg_si(new CegSingleInv(env, tr, s)),
- d_templInfer(new SygusTemplateInfer),
+ d_templInfer(new SygusTemplateInfer(env)),
d_ceg_proc(new SynthConjectureProcess),
d_ceg_gc(new CegGrammarConstructor(env, d_tds, this)),
d_sygus_rconst(new SygusRepairConst(env, d_tds)),
namespace theory {
namespace quantifiers {
-SynthVerify::SynthVerify(const Options& opts,
- const LogicInfo& logicInfo,
- TermDbSygus* tds)
- : d_tds(tds), d_subLogicInfo(logicInfo)
+SynthVerify::SynthVerify(Env& env, TermDbSygus* tds)
+ : EnvObj(env), d_tds(tds), d_subLogicInfo(logicInfo())
{
// determine the options to use for the verification subsolvers we spawn
// we start with the provided options
- d_subOptions.copyValues(opts);
+ d_subOptions.copyValues(options());
// limit the number of instantiation rounds on subcalls
d_subOptions.quantifiers.instMaxRounds =
d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
Node squery =
query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end());
Trace("cegqi-debug") << "...squery : " << squery << std::endl;
- squery = Rewriter::rewrite(squery);
+ squery = rewrite(squery);
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
Assert(options::sygusRecFun()
|| (squery.isConst() && squery.getConst<bool>()));
#include <memory>
#include "options/options.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "util/result.h"
/**
* Class for verifying queries corresponding to synthesis conjectures
*/
-class SynthVerify
+class SynthVerify : protected EnvObj
{
public:
- SynthVerify(const Options& opts,
- const LogicInfo& logicInfo,
- TermDbSygus* tds);
+ SynthVerify(Env& env, TermDbSygus* tds);
~SynthVerify();
/**
* Verification call, which takes into account specific aspects of the
namespace theory {
namespace quantifiers {
+SygusTemplateInfer::SygusTemplateInfer(Env& env) : EnvObj(env), d_ti(env) {}
+
void SygusTemplateInfer::initialize(Node q)
{
Assert(d_quant.isNull());
#include <map>
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/transition_inference.h"
namespace cvc5 {
* This class infers templates for an invariant-to-synthesize based on the
* template mode. It uses the transition inference to choose a template.
*/
-class SygusTemplateInfer
+class SygusTemplateInfer : protected EnvObj
{
public:
- SygusTemplateInfer() {}
+ SygusTemplateInfer(Env& env);
~SygusTemplateInfer() {}
/**
* Initialize this class for synthesis conjecture q. If applicable, the
d_qstate(qs),
d_syexp(new SygusExplain(this)),
d_funDefEval(new FunDefEvaluator(env)),
- d_eval_unfold(new SygusEvalUnfold(this))
+ d_eval_unfold(new SygusEvalUnfold(env, this))
{
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
{
if (args.empty())
{
- return Rewriter::rewrite( bn );
+ return rewrite(bn);
}
Assert(isRegistered(tn));
SygusTypeInfo& ti = getTypeInfo(tn);
const_var.end(),
const_subs.begin(),
const_subs.end());
- sn = Rewriter::rewrite(sn);
+ sn = rewrite(sn);
}
else
{
TNode ts = s;
for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
{
- const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts));
+ const_subs[k] = rewrite(const_subs[k].substitute(v, ts));
}
Trace("cegqi-inv-debug2")
<< "...substitution : " << v << " -> " << s << std::endl;
for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
{
Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
- disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+ disjuncts[j] = rewrite(disjuncts[j].substitute(
vars.begin(), vars.end(), svars.begin(), svars.end()));
Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
}
// transition
Assert(terms.find(true) != terms.end());
Node next = terms[true];
- next = Rewriter::rewrite(next.substitute(
+ next = rewrite(next.substitute(
vars.begin(), vars.end(), svars.begin(), svars.end()));
Trace("cegqi-inv-debug")
<< "transition next predicate : " << next << std::endl;
for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
{
Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
- disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+ disjuncts[j] = rewrite(disjuncts[j].substitute(
rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
}
// check if it satisfies the pre/post condition
Node cc = fwd ? getPostCondition() : getPreCondition();
Assert(!cc.isNull());
- Node ccr = Rewriter::rewrite(cc.substitute(
+ Node ccr = rewrite(cc.substitute(
d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
if (ccr.isConst())
{
Assert(!c.isNull());
Assert(d_vars.size() == dt.d_curr.size());
- Node cr = Rewriter::rewrite(c.substitute(
+ Node cr = rewrite(c.substitute(
d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
if (cr.isConst())
{
Assert(it->second.find(pv) != it->second.end());
Node pvs = it->second[pv];
Assert(d_vars.size() == dt.d_curr.size());
- Node pvsr = Rewriter::rewrite(pvs.substitute(
+ Node pvsr = rewrite(pvs.substitute(
d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
next.push_back(pvsr);
}
#include <vector>
#include "expr/node.h"
-
+#include "smt/env_obj.h"
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/single_inv_partition.h"
* The invariant-to-synthesize can either be explicitly given, via a call
* to initialize( f, vars ), or otherwise inferred if this method is not called.
*/
-class TransitionInference
+class TransitionInference : protected EnvObj
{
public:
- TransitionInference() : d_complete(false) {}
+ TransitionInference(Env& env) : EnvObj(env), d_complete(false) {}
/** Process the conjecture n
*
* This initializes this class with information related to viewing it as a
}
Assert(d_currentSet.isConst());
- Assert(d_currentSet == Rewriter::rewrite(d_currentSet));
Trace("set-type-enum") << "SetEnumerator::operator++ d_elementsSoFar = "
<< d_elementsSoFar << std::endl;
std::map<Node, Node> var_bound;
TypeNode tnn;
Node ret = simplifyNode(n, var_bound, tnn, model_replace_f, visited);
- ret = theory::Rewriter::rewrite(ret);
+ ret = rewrite(ret);
return ret;
}
.eqNode(nm->mkNode(kind::APPLY_UF, f, v2))
.negate(),
v1.eqNode(v2)));
- ret = theory::Rewriter::rewrite( ret );
+ ret = rewrite(ret);
return ret;
}
{
// if constant, compare
Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need)));
- cmp = Rewriter::rewrite(cmp);
+ cmp = rewrite(cmp);
needsSplit = !cmp.getConst<bool>();
}
else
}
Node len = nm->mkNode(STRING_LENGTH, cols[i][0]);
Node cons = nm->mkNode(GEQ, len, k_node);
- cons = Rewriter::rewrite(cons);
+ cons = rewrite(cons);
ei->d_cardinalityLemK.set(int_k + 1);
if (!cons.isConst() || !cons.getConst<bool>())
{
<< "Reduction_" << effort << " lemma : " << nnlem << std::endl;
Trace("strings-red-lemma") << "...from " << n << std::endl;
Trace("strings-red-lemma")
- << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
+ << "Reduction_" << effort << " rewritten : " << rewrite(nnlem)
+ << std::endl;
d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on reduction." << std::endl;
<< ", exp " << exp << std::endl;
einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
// inference is rewriting the substituted node
- Node nrc = Rewriter::rewrite(sn);
+ Node nrc = rewrite(sn);
// if rewrites to a constant, then do the inference and mark as reduced
if (nrc.isConst())
{
{
Trace("strings-extf-debug")
<< " rewrite " << nrs << "..." << std::endl;
- Node nrsr = Rewriter::rewrite(nrs);
+ Node nrsr = rewrite(nrs);
// ensure the symbolic form is not rewritable
if (nrsr != nrs)
{
{
children[index] = nrc;
Node conc = nm->mkNode(STRING_CONTAINS, children);
- conc = Rewriter::rewrite(pol ? conc : conc.negate());
+ conc = rewrite(pol ? conc : conc.negate());
// check if it already (does not) hold
if (d_state.hasTerm(conc))
{
Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
Node concOrig =
nm->mkNode(STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
- Node conc = Rewriter::rewrite(concOrig);
+ Node conc = rewrite(concOrig);
// For termination concerns, we only do the inference if the contains
// does not rewrite (and thus does not introduce new terms).
if (conc == concOrig)
// If it's not a predicate, see if we can solve the equality n = c, where c
// is the constant that extended term n is equal to.
Node inferEq = nr.eqNode(in.d_const);
- Node inferEqr = Rewriter::rewrite(inferEq);
+ Node inferEqr = rewrite(inferEq);
Node inferEqrr = inferEqr;
if (inferEqr.getKind() == EQUAL)
{
}
if (inferEqrr != inferEqr)
{
- inferEqrr = Rewriter::rewrite(inferEqrr);
+ inferEqrr = rewrite(inferEqrr);
Trace("strings-extf-infer")
<< "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
<< " with explanation " << in.d_exp << std::endl;
{
eq = d_false;
}
- else if (Rewriter::rewrite(eq) == d_true)
+ else if (rewrite(eq) == d_true)
{
// if trivial, return
return false;
bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
{
Node eq = a.eqNode(b);
- eq = Rewriter::rewrite(eq);
+ eq = rewrite(eq);
if (eq.isConst())
{
return false;
InferInfo iiSplit(infer);
iiSplit.d_sim = this;
iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
- eq = Rewriter::rewrite(eq);
+ eq = rewrite(eq);
addPendingPhaseRequirement(eq, preq);
addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
return true;
{
exp.push_back(te.eqNode(lengthTerm));
}
- return Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
+ return rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
}
Node SolverState::getLength(Node t, std::vector<Node>& exp)
if (n.getKind() != STRING_CONCAT && !n.isConst())
{
Node lsumb = nm->mkNode(STRING_LENGTH, n);
- lsum = Rewriter::rewrite(lsumb);
+ lsum = rewrite(lsumb);
// can register length term if it does not rewrite
if (lsum == lsumb)
{
}
}
Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
- Node eq = Rewriter::rewrite(sk.eqNode(n));
+ Node eq = rewrite(sk.eqNode(n));
d_proxyVar[n] = sk;
// If we are introducing a proxy for a constant or concat term, we do not
// need to send lemmas about its length, since its length is already
}
}
lsum = nm->mkNode(PLUS, nodeVec);
- lsum = Rewriter::rewrite(lsum);
+ lsum = rewrite(lsum);
}
else if (n.isConst())
{
}
Assert(!lsum.isNull());
d_proxyVarToLength[sk] = lsum;
- Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
+ Node ceq = rewrite(skl.eqNode(lsum));
Node ret = nm->mkNode(AND, eq, ceq);
Node n_len_eq_z = n_len.eqNode(d_zero);
Node n_len_eq_z_2 = n.eqNode(emp);
Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
- Node case_emptyr = Rewriter::rewrite(case_empty);
+ Node case_emptyr = rewrite(case_empty);
if (!case_emptyr.isConst())
{
// prefer trying the empty case first
// notice that requirePhase must only be called on rewritten literals that
// occur in the CNF stream.
- n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
+ n_len_eq_z = rewrite(n_len_eq_z);
Assert(!n_len_eq_z.isConst());
reqPhase[n_len_eq_z] = true;
- n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
+ n_len_eq_z_2 = rewrite(n_len_eq_z_2);
Assert(!n_len_eq_z_2.isConst());
reqPhase[n_len_eq_z_2] = true;
}
return Node::null();
}
Node eq = n.eqNode(pn);
- eq = Rewriter::rewrite(eq);
+ eq = rewrite(eq);
if (std::find(exp.begin(), exp.end(), eq) == exp.end())
{
exp.push_back(eq);
return;
}
Trace("strings-subs-proxy") << "Input : " << n << std::endl;
- Node ns = Rewriter::rewrite(n);
+ Node ns = rewrite(n);
if (ns.getKind() == EQUAL)
{
for (size_t i = 0; i < 2; i++)
<< conflict[i] << endl;
return false;
}
- if (conflict[i] != Rewriter::rewrite(conflict[i])) {
- Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
- << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
+ if (conflict[i] != rewrite(conflict[i]))
+ {
+ Debug("properConflict")
+ << "Bad conflict is due to atom not in normal form: " << conflict[i]
+ << " vs " << rewrite(conflict[i]) << endl;
return false;
}
}
<< conflict << endl;
return false;
}
- if (conflict != Rewriter::rewrite(conflict)) {
- Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
- << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
+ if (conflict != rewrite(conflict))
+ {
+ Debug("properConflict")
+ << "Bad conflict is due to atom not in normal form: " << conflict
+ << " vs " << rewrite(conflict) << endl;
return false;
}
}
&& assertion[0].getKind() == kind::EQUAL));
// Normalize
- Node normalizedLiteral = Rewriter::rewrite(assertion);
+ Node normalizedLiteral = rewrite(assertion);
// See if it rewrites false directly -> conflict
if (normalizedLiteral.isConst()) {
}
// Rewrite the equality
- Node eqNormalized = Rewriter::rewrite(atoms[i]);
+ Node eqNormalized = rewrite(atoms[i]);
Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
<< " with nf " << eqNormalized << endl;
continue;
}
// otherwise should hold by rewriting
- Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp));
+ Assert(rewrite(tConc) == rewrite(tExp));
// tExp
// ---- MACRO_SR_PRED_TRANSFORM
// tConc
resourceManager()->spendResource(id);
Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
// shouldn't send trivially true or false lemmas
- Assert(!Rewriter::rewrite(tlem.getProven()).isConst());
+ Assert(!rewrite(tlem.getProven()).isConst());
d_numCurrentLemmas++;
d_out.trustedLemma(tlem, p);
return true;
bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
{
- Node rewritten = Rewriter::rewrite(lem);
+ Node rewritten = rewrite(lem);
return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
}
bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
{
- Node rewritten = Rewriter::rewrite(lem);
+ Node rewritten = rewrite(lem);
if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
{
return false;
retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
if (childrenConst)
{
- retNode = Rewriter::rewrite(retNode);
+ retNode = rewrite(retNode);
}
}
d_normalizedCache[r] = retNode;
<< " returned " << hni << std::endl;
Assert(hni.isConst());
Assert(hni.getType().isSubtypeOf(args[0].getType()));
- hni = Rewriter::rewrite(args[0].eqNode(hni));
+ hni = rewrite(args[0].eqNode(hni));
Node hnv = m->getRepresentative(hn);
Trace("model-builder-debug2") << " get rep val : " << hn
<< " returned " << hnv << std::endl;
Assert(largs.size() == apply_args.size());
hnv = hnv[1].substitute(
largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
- hnv = Rewriter::rewrite(hnv);
+ hnv = rewrite(hnv);
}
Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
.isNull());
if (tid != THEORY_BOOL)
{
Node ppRewritten = ppTheoryRewrite(current, newLemmas);
- Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
+ Assert(rewrite(ppRewritten) == ppRewritten);
if (isProofEnabled() && ppRewritten != current)
{
TrustNode trn =
return preprocessWithProof(term, lems);
}
// should be in rewritten form here
- Assert(term == Rewriter::rewrite(term));
+ Assert(term == rewrite(term));
Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
// do not rewrite inside quantifiers
Node newTerm = term;
TConvProofGenerator* pg,
bool isPre)
{
- Node termr = Rewriter::rewrite(term);
+ Node termr = rewrite(term);
// store rewrite step if tracking proofs and it rewrites
if (isProofEnabled())
{
// recorded in d_tpg are functional. In other words, there should not
// be steps from the same term to multiple rewritten forms, which would be
// the case if we registered a preprocessing step for a non-rewritten term.
- Assert(term == Rewriter::rewrite(term));
+ Assert(term == rewrite(term));
Trace("tpp-debug2") << "preprocessWithProof " << term
<< ", #lems = " << lems.size() << std::endl;
// We never call ppRewrite on equalities here, since equalities have a
for( unsigned j=0; j<itel->second.size(); j++ ){
Node b = itel->second[j];
if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
- Node eq = Rewriter::rewrite( a.eqNode( b ) );
+ Node eq = rewrite(a.eqNode(b));
Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
d_im.lemma(lem, InferenceId::UF_CARD_SPLIT);
// witness via assertions.
if (!d_state.areDisequal(itf->second[j], itf->second[k]))
{
- Node deq =
- Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
+ Node deq = rewrite(itf->second[j].eqNode(itf->second[k]).negate());
// either add to model, or add lemma
if (isCollectModel)
{
d_reps.clear();
}
-SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
- : ContextNotifyObj(context),
- d_assertionsToRerun(context),
+SymmetryBreaker::SymmetryBreaker(Env& env, std::string name)
+ : EnvObj(env),
+ ContextNotifyObj(userContext()),
+ d_assertionsToRerun(userContext()),
d_rerunningAssertions(false),
d_phi(),
d_phiSet(),
}
Node SymmetryBreaker::norm(TNode phi) {
- Node n = Rewriter::rewrite(phi);
+ Node n = rewrite(phi);
return normInternal(n, 0);
}
namespace theory {
namespace uf {
-class SymmetryBreaker : public context::ContextNotifyObj {
-
+class SymmetryBreaker : protected EnvObj, public context::ContextNotifyObj
+{
class Template {
Node d_template;
NodeBuilder d_assertions;
}
public:
- SymmetryBreaker(context::Context* context, std::string name = "");
+ SymmetryBreaker(Env& env, std::string name = "");
void assertFormula(TNode phi);
void apply(std::vector<Node>& newClauses);
-};/* class SymmetryBreaker */
+}; /* class SymmetryBreaker */
} // namespace uf
} // namespace theory
d_thss(nullptr),
d_ho(nullptr),
d_functionsTerms(context()),
- d_symb(userContext(), instanceName),
+ d_symb(env, instanceName),
d_rewriter(logicInfo().isHigherOrder()),
d_state(env, valuation),
d_im(env, *this, d_state, "theory::uf::" + instanceName, false),
projects / cvc5.git / commitdiff