This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.
Construction of Evaluator utilities is now discouraged.
The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.
This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
#include "proof/conv_proof_generator.h"
#include "smt/dump_manager.h"
#include "smt/smt_engine_stats.h"
+#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/trust_substitutions.h"
#include "util/resource_manager.h"
d_nodeManager(nm),
d_proofNodeManager(nullptr),
d_rewriter(new theory::Rewriter()),
+ d_evalRew(new theory::Evaluator(d_rewriter.get())),
+ d_eval(new theory::Evaluator(nullptr)),
d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
d_dumpManager(new DumpManager(d_userContext.get())),
d_logic(),
std::ostream& Env::getDumpOut() { return *d_options.base.out; }
+Node Env::evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ bool useRewriter) const
+{
+ std::unordered_map<Node, Node> visited;
+ return evaluate(n, args, vals, visited, useRewriter);
+}
+
+Node Env::evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ const std::unordered_map<Node, Node>& visited,
+ bool useRewriter) const
+{
+ if (useRewriter)
+ {
+ return d_evalRew->eval(n, args, vals, visited);
+ }
+ return d_eval->eval(n, args, vals, visited);
+}
+
+Node Env::rewriteViaMethod(TNode n, MethodId idr)
+{
+ if (idr == MethodId::RW_REWRITE)
+ {
+ return d_rewriter->rewrite(n);
+ }
+ if (idr == MethodId::RW_EXT_REWRITE)
+ {
+ return d_rewriter->extendedRewrite(n);
+ }
+ if (idr == MethodId::RW_REWRITE_EQ_EXT)
+ {
+ return d_rewriter->rewriteEqualityExt(n);
+ }
+ if (idr == MethodId::RW_EVALUATE)
+ {
+ return evaluate(n, {}, {}, false);
+ }
+ if (idr == MethodId::RW_IDENTITY)
+ {
+ // does nothing
+ return n;
+ }
+ // unknown rewriter
+ Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr
+ << std::endl;
+ return n;
+}
+
} // namespace cvc5
#include <memory>
#include "options/options.h"
+#include "proof/method_id.h"
#include "theory/logic_info.h"
#include "util/statistics_registry.h"
}
namespace theory {
+class Evaluator;
class Rewriter;
class TrustSubstitutionMap;
}
*/
std::ostream& getDumpOut();
+ /* Rewrite helpers--------------------------------------------------------- */
+ /**
+ * Evaluate node n under the substitution args -> vals. For details, see
+ * theory/evaluator.h.
+ *
+ * @param n The node to evaluate
+ * @param args The domain of the substitution
+ * @param vals The range of the substitution
+ * @param useRewriter if true, we use this rewriter to rewrite subterms of
+ * n that cannot be evaluated to a constant.
+ * @return the rewritten, evaluated form of n under the given substitution.
+ */
+ Node evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ bool useRewriter) const;
+ /** Same as above, with a visited cache. */
+ Node evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ const std::unordered_map<Node, Node>& visited,
+ bool useRewriter = true) const;
+ /**
+ * Apply rewrite on n via the rewrite method identifier idr (see method_id.h).
+ * This encapsulates the exact behavior of a REWRITE step in a proof.
+ *
+ * @param n The node to rewrite,
+ * @param idr The method identifier of the rewriter, by default RW_REWRITE
+ * specifying a call to rewrite.
+ * @return The rewritten form of n.
+ */
+ Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE);
+
private:
/* Private initialization ------------------------------------------------- */
* specific to an SmtEngine/TheoryEngine instance.
*/
std::unique_ptr<theory::Rewriter> d_rewriter;
+ /** Evaluator that also invokes the rewriter */
+ std::unique_ptr<theory::Evaluator> d_evalRew;
+ /** Evaluator that does not invoke the rewriter */
+ std::unique_ptr<theory::Evaluator> d_eval;
/** The top level substitutions */
std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
/** The dump manager */
{
return d_env.getRewriter()->extendedRewrite(node, aggr);
}
+Node EnvObj::evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ bool useRewriter) const
+{
+ return d_env.evaluate(n, args, vals, useRewriter);
+}
+Node EnvObj::evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ const std::unordered_map<Node, Node>& visited,
+ bool useRewriter) const
+{
+ return d_env.evaluate(n, args, vals, visited, useRewriter);
+}
const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
* This is a wrapper around theory::Rewriter::extendedRewrite via Env.
*/
Node extendedRewrite(TNode node, bool aggr = true) const;
+ /**
+ * Evaluate node n under the substitution args -> vals.
+ * This is a wrapper about theory::Rewriter::evaluate via Env.
+ */
+ Node evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ bool useRewriter = true) const;
+ /** Same as above, with a visited cache. */
+ Node evaluate(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ const std::unordered_map<Node, Node>& visited,
+ bool useRewriter = true) const;
/** Get the current logic information. */
const LogicInfo& logicInfo() const;
rargs.push_back(args[3]);
}
}
- Rewriter* rr = d_env.getRewriter();
- Node tr = rr->rewriteViaMethod(ts, idr);
+ Node tr = d_env.rewriteViaMethod(ts, idr);
Trace("smt-proof-pp-debug")
<< "...eq intro rewrite equality is " << ts << " == " << tr << ", from "
<< idr << std::endl;
getMethodId(args[1], idr);
}
Rewriter* rr = d_env.getRewriter();
- Node ret = rr->rewriteViaMethod(args[0], idr);
+ Node ret = d_env.rewriteViaMethod(args[0], idr);
Node eq = args[0].eqNode(ret);
if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
{
#include "expr/skolem_manager.h"
#include "smt/env.h"
#include "smt/term_formula_removal.h"
-#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
#include "theory/theory.h"
+#include "util/rational.h"
using namespace cvc5::kind;
MethodId idr)
{
Node nks = applySubstitution(n, exp, ids, ida);
- return d_env.getRewriter()->rewriteViaMethod(nks, idr);
+ return d_env.rewriteViaMethod(nks, idr);
}
bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
{
return Node::null();
}
- Node res = d_env.getRewriter()->rewriteViaMethod(args[0], idr);
+ Node res = d_env.rewriteViaMethod(args[0], idr);
if (res.isNull())
{
return Node::null();
{
Assert(children.empty());
Assert(args.size() == 1);
- Node res = d_env.getRewriter()->rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
+ Node res = d_env.rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
if (res.isNull())
{
return Node::null();
<< SkolemManager::getOriginalForm(res) << std::endl;
// **** NOTE: can rewrite the witness form here. This enables certain lemmas
// to be provable, e.g. (= k t) where k is a purification Skolem for t.
- res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
+ res = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res));
if (!res.isConst() || !res.getConst<bool>())
{
Trace("builtin-pfcheck")
if (res1 != res2)
{
// can rewrite the witness forms
- res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
- res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
+ res1 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res1));
+ res2 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res2));
if (res1.isNull() || res1 != res2)
{
Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
{
NodeManager* nm = NodeManager::currentNM();
- Evaluator eval;
+ Evaluator eval(nullptr);
// constant arguments?
bool constArgs = true;
for (const Node& a : args)
#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include "theory/theory_state.h"
+#include "util/rational.h"
using namespace cvc5;
using namespace cvc5::kind;
if (bv != bvr)
{
// add to the sampler database object
- std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
- d_sampler[a].find(tn);
- if (its == d_sampler[a].end())
+ std::map<TypeNode, std::unique_ptr<quantifiers::SygusSampler>>& smap =
+ d_sampler[a];
+ std::map<TypeNode,
+ std::unique_ptr<quantifiers::SygusSampler>>::iterator its =
+ smap.find(tn);
+ if (its == smap.end())
{
- d_sampler[a][tn].initializeSygus(
+ smap[tn].reset(new quantifiers::SygusSampler(d_env));
+ smap[tn]->initializeSygus(
d_tds, nv, options::sygusSamples(), false);
its = d_sampler[a].find(tn);
}
// check equivalent
- its->second.checkEquivalent(bv, bvr, *options().base.out);
+ its->second->checkEquivalent(bv, bvr, *options().base.out);
}
}
* This is used for the sygusRewVerify() option to verify the correctness of
* the rewriter.
*/
- std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler;
+ std::map<Node, std::map<TypeNode, std::unique_ptr<quantifiers::SygusSampler>>>
+ d_sampler;
/** Assert tester internal
*
* This function is called when the tester with index tindex is asserted for
#include "expr/dtype_cons.h"
#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
using namespace std;
using namespace cvc5::kind;
#include "expr/dtype_cons.h"
#include "expr/kind.h"
#include "expr/skolem_manager.h"
+#include "expr/uninterpreted_constant.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "theory/theory_state.h"
#include "theory/type_enumerator.h"
#include "theory/valuation.h"
+#include "util/rational.h"
using namespace std;
using namespace cvc5::kind;
}
}
+Evaluator::Evaluator(Rewriter* rr)
+ : d_rr(rr), d_alphaCard(strings::utils::getAlphabetCardinality())
+{
+}
+
Node Evaluator::eval(TNode n,
const std::vector<Node>& args,
- const std::vector<Node>& vals,
- bool useRewriter) const
+ const std::vector<Node>& vals) const
{
std::unordered_map<Node, Node> visited;
- return eval(n, args, vals, visited, useRewriter);
+ return eval(n, args, vals, visited);
}
Node Evaluator::eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
- const std::unordered_map<Node, Node>& visited,
- bool useRewriter) const
+ const std::unordered_map<Node, Node>& visited) const
{
Trace("evaluator") << "Evaluating " << n << " under substitution " << args
<< " " << vals << " with visited size = " << visited.size()
for (const std::pair<const Node, Node>& p : visited)
{
Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
- results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results, useRewriter);
+ results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results);
if (results[p.first].d_tag == EvalResult::INVALID)
{
// could not evaluate, use the evalAsNode map
std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(p.second);
Assert(itn != evalAsNode.end());
Node val = itn->second;
- if (useRewriter)
+ if (d_rr != nullptr)
{
- val = Rewriter::rewrite(val);
+ val = d_rr->rewrite(val);
}
evalAsNode[p.first] = val;
}
}
Trace("evaluator") << "Run eval internal..." << std::endl;
- Node ret = evalInternal(n, args, vals, evalAsNode, results, useRewriter).toNode();
+ Node ret = evalInternal(n, args, vals, evalAsNode, results).toNode();
// if we failed to evaluate
- if (ret.isNull() && useRewriter)
+ if (ret.isNull() && d_rr != nullptr)
{
// should be stored in the evaluation-as-node map
std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
Assert(itn != evalAsNode.end());
- ret = Rewriter::rewrite(itn->second);
+ ret = d_rr->rewrite(itn->second);
}
// should be the same as substitution + rewriting, or possibly null if
- // useRewriter is false
- Assert((ret.isNull() && !useRewriter)
+ // d_rr is nullptr
+ Assert((ret.isNull() && d_rr == nullptr)
|| ret
- == Rewriter::rewrite(n.substitute(
- args.begin(), args.end(), vals.begin(), vals.end())));
+ == d_rr->rewrite(n.substitute(
+ args.begin(), args.end(), vals.begin(), vals.end())));
return ret;
}
const std::vector<Node>& args,
const std::vector<Node>& vals,
std::unordered_map<TNode, Node>& evalAsNode,
- std::unordered_map<TNode, EvalResult>& results,
- bool useRewriter) const
+ std::unordered_map<TNode, EvalResult>& results) const
{
std::vector<TNode> queue;
queue.emplace_back(n);
// successfully evaluated, and the children that did not.
Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
- if (useRewriter)
+ if (d_rr != nullptr)
{
// Rewrite the result now, if we use the rewriter. We will see below
// if we are able to turn it into a valid EvalResult.
- currNodeVal = Rewriter::rewrite(currNodeVal);
+ currNodeVal = d_rr->rewrite(currNodeVal);
}
}
needsReconstruct = false;
// evalAsNodeC but favor avoiding this copy for performance reasons.
std::unordered_map<TNode, Node> evalAsNodeC;
std::unordered_map<TNode, EvalResult> resultsC;
- results[currNode] = evalInternal(op[1],
- lambdaArgs,
- lambdaVals,
- evalAsNodeC,
- resultsC,
- useRewriter);
+ results[currNode] = evalInternal(
+ op[1], lambdaArgs, lambdaVals, evalAsNodeC, resultsC);
Trace("evaluator") << "Evaluated via arguments to "
<< results[currNode].d_tag << std::endl;
if (results[currNode].d_tag == EvalResult::INVALID)
case kind::STRING_FROM_CODE:
{
Integer i = results[currNode[0]].d_rat.getNumerator();
- if (i >= 0 && i < strings::utils::getAlphabetCardinality())
+ if (i >= 0 && i < d_alphaCard)
{
std::vector<unsigned> svec = {i.toUnsignedInt()};
results[currNode] = EvalResult(String(svec));
Node toNode() const;
};
+class Rewriter;
+
/**
* The class that performs the actual evaluation of a term under a
* substitution. Right now, the class does not cache anything between different
class Evaluator
{
public:
+ Evaluator(Rewriter* rr);
/**
* Evaluates node `n` under the substitution described by the variable names
* `args` and the corresponding values `vals`. This method uses evaluation
* The result of this call is either equivalent to:
* (1) Rewriter::rewrite(n.substitute(args,vars))
* (2) Node::null().
- * If useRewriter is true, then we are always in the first case. If
- * useRewriter is false, then we may be in case (2) if computing the
+ * If d_rr is non-null, then we are always in the first case. If
+ * useRewriter is null, then we may be in case (2) if computing the
* rewritten, substituted form of n could not be determined by evaluation.
*/
Node eval(TNode n,
const std::vector<Node>& args,
- const std::vector<Node>& vals,
- bool useRewriter = true) const;
+ const std::vector<Node>& vals) const;
/**
* Same as above, but with a precomputed visited map.
*/
Node eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
- const std::unordered_map<Node, Node>& visited,
- bool useRewriter = true) const;
+ const std::unordered_map<Node, Node>& visited) const;
private:
/**
const std::vector<Node>& args,
const std::vector<Node>& vals,
std::unordered_map<TNode, Node>& evalAsNode,
- std::unordered_map<TNode, EvalResult>& results,
- bool useRewriter) const;
+ std::unordered_map<TNode, EvalResult>& results) const;
/** reconstruct
*
* This function reconstructs the result of evaluating n using a combination
Node reconstruct(TNode n,
std::unordered_map<TNode, EvalResult>& eresults,
std::unordered_map<TNode, Node>& evalAsNode) const;
+ /** The (optional) rewriter to be used */
+ Rewriter* d_rr;
+ /** The cardinality of the alphabet of strings */
+ uint32_t d_alphaCard;
};
} // namespace theory
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
-#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
-#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
-#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
-
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace std;
using namespace cvc5::kind;
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace std;
using namespace cvc5::kind;
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#include "theory/quantifiers/expr_miner_manager.h"
#include "options/quantifiers_options.h"
+#include "smt/env.h"
namespace cvc5 {
namespace theory {
options::sygusRewSynthAccel(),
false),
d_qg(env),
- d_sols(env)
+ d_sols(env),
+ d_sampler(env)
{
}
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5;
using namespace std;
namespace theory {
namespace quantifiers {
-FunDefEvaluator::FunDefEvaluator() {}
+FunDefEvaluator::FunDefEvaluator(Env& env) : EnvObj(env) {}
void FunDefEvaluator::assertDefinition(Node q)
{
<< fdi.d_args << " / " << fdi.d_body << std::endl;
}
-Node FunDefEvaluator::evaluate(Node n) const
+Node FunDefEvaluator::evaluateDefinitions(Node n) const
{
// should do standard rewrite before this call
Assert(Rewriter::rewrite(n) == n);
- Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
+ Trace("fd-eval") << "FunDefEvaluator: evaluateDefinitions " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
std::unordered_map<TNode, unsigned> funDefCount;
std::unordered_map<TNode, unsigned>::iterator itCount;
if (!args.empty())
{
// invoke it on arguments using the evaluator
- sbody = d_eval.eval(sbody, args, children);
+ sbody = evaluate(sbody, args, children);
if (Trace.isOn("fd-eval-debug2"))
{
Trace("fd-eval-debug2")
#include <map>
#include <vector>
+
#include "expr/node.h"
-#include "theory/evaluator.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
/**
* Techniques for evaluating recursively defined functions.
*/
-class FunDefEvaluator
+class FunDefEvaluator : protected EnvObj
{
public:
- FunDefEvaluator();
+ FunDefEvaluator(Env& env);
~FunDefEvaluator() {}
/**
* Assert definition of a (recursive) function definition given by quantified
* class. If n cannot be simplified to a constant, then this method returns
* null.
*/
- Node evaluate(Node n) const;
+ Node evaluateDefinitions(Node n) const;
/**
* Has a call to assertDefinition been made? If this returns false, then
* the evaluate method is the same as calling the rewriter, and returning
std::map<Node, FunDefInfo> d_funDefMap;
/** list of all definitions */
std::vector<Node> d_funDefs;
- /** evaluator utility */
- Evaluator d_eval;
};
} // namespace quantifiers
#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
using namespace std;
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
+#include "util/string.h"
using namespace std;
using namespace cvc5::kind;
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#include "options/base_options.h"
#include "options/quantifiers_options.h"
+#include "smt/env.h"
#include "util/random.h"
using namespace cvc5::kind;
SynthConjecture* p)
: SygusModule(env, qs, qim, tds, p),
d_eval_unfold(tds->getEvalUnfold()),
+ d_cegis_sampler(env),
d_usingSymCons(false)
{
}
}
}
- Evaluator* eval = d_tds->getEvaluator();
for (unsigned r = 0; r < 2; r++)
{
std::unordered_set<Node>& rlemmas =
{
// We may have computed the evaluation of some function applications
// via example-based symmetry breaking, stored in evalVisited.
- Node lemcsu = eval->eval(lem, vs, ms, evalVisited);
+ Node lemcsu = evaluate(lem, vs, ms, evalVisited);
if (lemcsu.isConst() && !lemcsu.getConst<bool>())
{
return true;
namespace theory {
namespace quantifiers {
+class SygusEvalUnfold;
+
/** Cegis
*
* The default sygus module for synthesis, counterexample-guided inductive
Assert(candidates.size() == 1 && candidates[0] == d_candidate);
TNode cval = candidate_values[0];
Node ets = d_eterm.substitute(d_candidate, cval);
- Node etsr = Rewriter::rewrite(ets);
+ Node etsr = rewrite(ets);
Trace("sygus-ccore-debug") << "...predicate is: " << etsr << std::endl;
NodeManager* nm = NodeManager::currentNM();
for (unsigned d = 0; d < 2; d++)
visited.insert(id);
Trace("sygus-ccore-ref") << "...eval " << std::endl;
// check if it is true
- Node en = p->evaluate(n, id, ctx);
+ Node en = p->evaluatePt(n, id, ctx);
if (en.isConst() && en.getConst<bool>())
{
ss = ctx;
for (unsigned i = currIndex, psize = passerts.size(); i < psize; i++)
{
Node cn = passerts[i];
- Node cne = p->evaluate(cn, mvId, mvs);
+ Node cne = p->evaluatePt(cn, mvId, mvs);
if (cne.isConst() && !cne.getConst<bool>())
{
n = cn;
return r;
}
-Node CegisCoreConnective::evaluate(Node n,
- Node id,
- const std::vector<Node>& mvs)
+Node CegisCoreConnective::evaluatePt(Node n,
+ Node id,
+ const std::vector<Node>& mvs)
{
Kind nk = n.getKind();
if (nk == AND || nk == OR)
// split AND/OR
for (const Node& nc : n)
{
- Node enc = evaluate(nc, id, mvs);
+ Node enc = evaluatePt(nc, id, mvs);
Assert(enc.isConst());
if (enc.getConst<bool>() == expRes)
{
}
}
// use evaluator
- Node cn = d_eval.eval(n, d_vars, mvs);
- if (cn.isNull())
- {
- cn = n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end());
- cn = Rewriter::rewrite(cn);
- }
+ Node cn = evaluate(n, d_vars, mvs);
+ Assert(!cn.isNull());
if (!id.isNull())
{
ec[id] = cn;
mvs.clear();
getModel(*checkSol, mvs);
// should evaluate to true
- Node ean = evaluate(an, Node::null(), mvs);
+ Node ean = evaluatePt(an, Node::null(), mvs);
Assert(ean.isConst() && ean.getConst<bool>());
Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl;
// In terms of Variant #2, this is the line:
#include "expr/node.h"
#include "expr/node_trie.h"
#include "smt/env_obj.h"
-#include "theory/evaluator.h"
#include "theory/quantifiers/sygus/cegis.h"
#include "util/result.h"
* If id is non-null, then id is a unique identifier for mvs, and we cache
* the result of n for this point.
*/
- Node evaluate(Node n, Node id, const std::vector<Node>& mvs);
+ Node evaluatePt(Node n, Node id, const std::vector<Node>& mvs);
/** A cache of the above function */
std::unordered_map<Node, std::unordered_map<Node, Node>> d_eval_cache;
- /** The evaluator utility used for the above function */
- Evaluator d_eval;
//-----------------------------------end for evaluation
/** Construct solution from pool
#include "theory/quantifiers/sygus/sygus_unif_rl.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "util/rational.h"
using namespace cvc5::kind;
std::ostream* out = nullptr;
if (options::sygusRewVerify())
{
- d_samplerRrV.reset(new SygusSampler);
+ d_samplerRrV.reset(new SygusSampler(d_env));
d_samplerRrV->initializeSygus(
d_tds, e, options::sygusSamples(), false);
// use the default output for the output of sygusRewVerify
#include "theory/quantifiers/sygus/rcons_type_info.h"
#include "expr/skolem_manager.h"
+#include "smt/env.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/rcons_obligation.h"
+#include "theory/quantifiers/sygus_sampler.h"
namespace cvc5 {
namespace theory {
d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false));
// since initial samples are not always useful for equivalence checks, set
// their number to 0
- d_sygusSampler.initialize(stn, builtinVars, 0);
- d_crd->initialize(builtinVars, &d_sygusSampler);
+ d_sygusSampler.reset(new SygusSampler(env));
+ d_sygusSampler->initialize(stn, builtinVars, 0);
+ d_crd->initialize(builtinVars, d_sygusSampler.get());
}
Node RConsTypeInfo::nextEnum()
#include "theory/quantifiers/candidate_rewrite_database.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
-#include "theory/quantifiers/sygus_sampler.h"
namespace cvc5 {
namespace theory {
class RConsObligation;
class CandidateRewriteDatabase;
+class SygusSampler;
/**
* A utility class for Sygus Reconstruct datatype types (grammar non-terminals).
/** Candidate rewrite database for this class' sygus datatype type */
std::unique_ptr<CandidateRewriteDatabase> d_crd;
/** Sygus sampler needed for initializing the candidate rewrite database */
- SygusSampler d_sygusSampler;
+ std::unique_ptr<SygusSampler> d_sygusSampler;
/** A map from a builtin term to its obligation.
*
* Each sygus datatype type has its own version of this map because it is
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/sygus/type_node_id_trie.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#include "theory/rewriter.h"
#include "theory/strings/word.h"
#include "util/floatingpoint.h"
+#include "util/string.h"
using namespace cvc5::kind;
#include "options/quantifiers_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
-#include "theory/evaluator.h"
#include "theory/quantifiers/sygus/example_infer.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
: EnvObj(env),
d_qstate(qs),
d_syexp(new SygusExplain(this)),
- d_eval(new Evaluator),
- d_funDefEval(new FunDefEvaluator),
+ d_funDefEval(new FunDefEvaluator(env)),
d_eval_unfold(new SygusEvalUnfold(this))
{
d_true = NodeManager::currentNM()->mkConst( true );
{
// If recursive functions are enabled, then we use the recursive function
// evaluation utility.
- Node fres = d_funDefEval->evaluate(res);
+ Node fres = d_funDefEval->evaluateDefinitions(res);
if (!fres.isNull())
{
return fres;
// This may fail if there is a subterm of bn under the
// substitution that is not constant, or if an operator in bn is not
// supported by the evaluator
- res = d_eval->eval(bn, varlist, args);
+ res = evaluate(bn, varlist, args);
}
if (res.isNull())
{
#include "expr/dtype.h"
#include "smt/env_obj.h"
-#include "theory/evaluator.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers/fun_def_evaluator.h"
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
//------------------------------utilities
/** get the explanation utility */
SygusExplain* getExplain() { return d_syexp.get(); }
- /** get the evaluator */
- Evaluator* getEvaluator() { return d_eval.get(); }
/** (recursive) function evaluator utility */
FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); }
/** evaluation unfolding utility */
//------------------------------utilities
/** sygus explanation */
std::unique_ptr<SygusExplain> d_syexp;
- /** evaluator */
- std::unique_ptr<Evaluator> d_eval;
/** (recursive) function evaluator utility */
std::unique_ptr<FunDefEvaluator> d_funDefEval;
/** evaluation function unfolding utility */
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "theory/quantifiers/lazy_trie.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/rewriter.h"
#include "util/bitvector.h"
#include "util/random.h"
+#include "util/rational.h"
#include "util/sampler.h"
+#include "util/string.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
-SygusSampler::SygusSampler()
- : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
+SygusSampler::SygusSampler(Env& env)
+ : d_env(env), d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
{
}
{
Assert(index < d_samples.size());
// do beta-reductions in n first
- n = Rewriter::rewrite(n);
+ n = d_env.getRewriter()->rewrite(n);
// use efficient rewrite for substitution + rewrite
- Node ev = d_eval.eval(n, d_vars, d_samples[index]);
+ Node ev = d_env.evaluate(n, d_vars, d_samples[index], true);
+ Assert(!ev.isNull());
Trace("sygus-sample-ev") << "Evaluate ( " << n << ", " << index << " ) -> ";
- if (!ev.isNull())
- {
- Trace("sygus-sample-ev") << ev << std::endl;
- return ev;
- }
- Trace("sygus-sample-ev") << "null" << std::endl;
- Trace("sygus-sample-ev") << "Rewrite -> ";
- // substitution + rewrite
- std::vector<Node>& pt = d_samples[index];
- ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
- ev = Rewriter::rewrite(ev);
Trace("sygus-sample-ev") << ev << std::endl;
return ev;
}
// negative
ret = nm->mkNode(kind::UMINUS, ret);
}
- ret = Rewriter::rewrite(ret);
+ ret = d_env.getRewriter()->rewrite(ret);
Assert(ret.isConst());
return ret;
}
Trace("sygus-sample-grammar") << "mkGeneric" << std::endl;
Node ret = d_tds->mkGeneric(dt, cindex, pre);
Trace("sygus-sample-grammar") << "...returned " << ret << std::endl;
- ret = Rewriter::rewrite(ret);
+ ret = d_env.getRewriter()->rewrite(ret);
Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl;
// A rare case where we generate a non-constant value from constant
// leaves is (/ n 0).
#define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
#include <map>
-#include "theory/evaluator.h"
#include "theory/quantifiers/lazy_trie.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_enumeration.h"
namespace cvc5 {
+
+class Env;
+
namespace theory {
namespace quantifiers {
+class TermDbSygus;
+
/** SygusSampler
*
* This class can be used to test whether two expressions are equivalent
class SygusSampler : public LazyTrieEvaluator
{
public:
- SygusSampler();
+ SygusSampler(Env& env);
~SygusSampler() override {}
/** initialize
void checkEquivalent(Node bv, Node bvr, std::ostream& out);
protected:
+ /** The environment we are using to evaluate terms and samples */
+ Env& d_env;
/** sygus term database of d_qe */
TermDbSygus* d_tds;
/** term enumerator object (used for random sampling) */
TermEnumeration d_tenum;
/** samples */
std::vector<std::vector<Node> > d_samples;
- /** evaluator class */
- Evaluator d_eval;
/** data structure to check duplication of sample points */
class PtTrie
{
clearCachesInternal();
}
-Node Rewriter::rewriteViaMethod(TNode n, MethodId idr)
-{
- if (idr == MethodId::RW_REWRITE)
- {
- return rewrite(n);
- }
- if (idr == MethodId::RW_EXT_REWRITE)
- {
- return extendedRewrite(n);
- }
- if (idr == MethodId::RW_REWRITE_EQ_EXT)
- {
- return rewriteEqualityExt(n);
- }
- if (idr == MethodId::RW_EVALUATE)
- {
- Evaluator eval;
- return eval.eval(n, {}, {}, false);
- }
- if (idr == MethodId::RW_IDENTITY)
- {
- // does nothing
- return n;
- }
- // unknown rewriter
- Unhandled() << "Rewriter::rewriteViaMethod: no rewriter for " << idr
- << std::endl;
- return n;
-}
-
} // namespace theory
} // namespace cvc5
#pragma once
#include "expr/node.h"
-#include "proof/method_id.h"
#include "theory/theory_rewriter.h"
namespace cvc5 {
+class Env;
class TConvProofGenerator;
class ProofNodeManager;
class TrustNode;
namespace theory {
+class Evaluator;
+
/**
* The main rewriter class.
*/
class Rewriter {
-
+ friend class cvc5::Env; // to initialize the evaluators of this class
public:
Rewriter();
Node rewriteEqualityExt(TNode node);
/**
+ * !!! Temporary until static access to rewriter is eliminated. This method
+ * should be moved to same place as evaluate (currently in Env).
+ *
* Extended rewrite of the given node. This method is implemented by a
* custom ExtendRewriter class that wraps this class to perform custom
* rewrites (usually those that are not useful for solving, but e.g. useful
/** Get the theory rewriter for the given id */
TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
- /**
- * Apply rewrite on n via the rewrite method identifier idr (see method_id.h).
- * This encapsulates the exact behavior of a REWRITE step in a proof.
- *
- * @param n The node to rewrite,
- * @param idr The method identifier of the rewriter, by default RW_REWRITE
- * specifying a call to rewrite.
- * @return The rewritten form of n.
- */
- Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE);
-
private:
/**
* Get the rewriter associated with the SmtEngine in scope.
}
}
-Rewriter::Rewriter() : d_tpg(nullptr)
-{
-
-}
+Rewriter::Rewriter() : d_tpg(nullptr) {}
void Rewriter::clearCachesInternal()
{
std::vector<Node> args = {w, x, y, z};
std::vector<Node> vals = {c1, zero, one, c1};
- Evaluator eval;
+ Rewriter* rr = d_smtEngine->getRewriter();
+ Evaluator eval(rr);
Node r = eval.eval(t, args, vals);
ASSERT_EQ(r,
- Rewriter::rewrite(t.substitute(
+ rr->rewrite(t.substitute(
args.begin(), args.end(), vals.begin(), vals.end())));
}
std::vector<Node> args = {x};
std::vector<Node> vals = {c};
- Evaluator eval;
+ Rewriter* rr = d_smtEngine->getRewriter();
+ Evaluator eval(rr);
Node r = eval.eval(t, args, vals);
ASSERT_EQ(r,
- Rewriter::rewrite(t.substitute(
+ rr->rewrite(t.substitute(
args.begin(), args.end(), vals.begin(), vals.end())));
}
std::vector<Node> args;
std::vector<Node> vals;
- Evaluator eval;
+ Rewriter* rr = d_smtEngine->getRewriter();
+ Evaluator eval(rr);
{
Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, one);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, Rewriter::rewrite(n));
+ ASSERT_EQ(r, rr->rewrite(n));
}
{
Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, one);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, Rewriter::rewrite(n));
+ ASSERT_EQ(r, rr->rewrite(n));
}
{
Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, two);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, Rewriter::rewrite(n));
+ ASSERT_EQ(r, rr->rewrite(n));
}
{
Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, Rewriter::rewrite(n));
+ ASSERT_EQ(r, rr->rewrite(n));
}
}
std::vector<Node> args;
std::vector<Node> vals;
- Evaluator eval;
+ Rewriter* rr = d_smtEngine->getRewriter();
+ Evaluator eval(rr);
// (str.code "A") ---> 65
{
projects / cvc5.git / commitdiff