From 9760648304ab71e6af6c479c0c3e941908561bc7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Dec 2021 11:01:05 -0600 Subject: [PATCH] Eliminate more static calls to Rewriter::rewrite (#7755) --- .../quantifiers/sygus/sygus_process_conj.cpp | 8 +++++-- .../quantifiers/sygus/sygus_process_conj.h | 9 ++++---- .../quantifiers/sygus/synth_conjecture.cpp | 2 +- src/theory/theory_model_builder.cpp | 3 ++- src/theory/uf/cardinality_extension.cpp | 10 +++++---- src/theory/uf/cardinality_extension.h | 5 +++-- src/theory/uf/proof_equality_engine.cpp | 5 +++-- src/theory/uf/proof_equality_engine.h | 3 ++- src/theory/uf/theory_uf_model.cpp | 21 ++++++++++++------- src/theory/uf/theory_uf_model.h | 15 ++++++++----- 10 files changed, 52 insertions(+), 29 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index f5cadc607..d51cd9ab1 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -30,6 +30,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { +SynthConjectureProcessFun::SynthConjectureProcessFun(Env& env) : EnvObj(env) {} + void SynthConjectureProcessFun::init(Node f) { d_synth_fun = f; @@ -511,7 +513,7 @@ void SynthConjectureProcessFun::getIrrelevantArgs( } } -SynthConjectureProcess::SynthConjectureProcess() {} +SynthConjectureProcess::SynthConjectureProcess(Env& env) : EnvObj(env) {} SynthConjectureProcess::~SynthConjectureProcess() {} Node SynthConjectureProcess::preSimplify(Node q) { @@ -532,7 +534,9 @@ Node SynthConjectureProcess::postSimplify(Node q) Node f = q[0][i]; if (f.getType().isFunction()) { - d_sf_info[f].init(f); + std::pair::iterator, bool> + it = d_sf_info.emplace(f, d_env); + it.first->second.init(f); } } diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index d751e4c9c..b0b87c65b 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/type_node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -119,10 +120,10 @@ class SynthConjectureProcessArg * It maintains information about each of the function to * synthesize's arguments. */ -struct SynthConjectureProcessFun +struct SynthConjectureProcessFun : protected EnvObj { public: - SynthConjectureProcessFun() {} + SynthConjectureProcessFun(Env& env); ~SynthConjectureProcessFun() {} /** initialize this class for function f */ void init(Node f); @@ -266,10 +267,10 @@ struct SynthConjectureProcessFun * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are * used for pruning search space based on conjecture-specific analysis. */ -class SynthConjectureProcess +class SynthConjectureProcess : protected EnvObj { public: - SynthConjectureProcess(); + SynthConjectureProcess(Env& env); ~SynthConjectureProcess(); /** simplify the synthesis conjecture q * Returns a formula that is equivalent to q. diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e7d0ef58b..a90551a0f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -61,7 +61,7 @@ SynthConjecture::SynthConjecture(Env& env, d_hasSolution(false), d_ceg_si(new CegSingleInv(env, tr, s)), d_templInfer(new SygusTemplateInfer(env)), - d_ceg_proc(new SynthConjectureProcess), + d_ceg_proc(new SynthConjectureProcess(env)), d_ceg_gc(new CegGrammarConstructor(env, d_tds, this)), d_sygus_rconst(new SygusRepairConst(env, d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index bc63aef97..1e56bd6ba 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1278,7 +1278,8 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) } std::stringstream ss; ss << "_arg_"; - Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues); + Rewriter* r = condenseFuncValues ? d_env.getRewriter() : nullptr; + Node val = ufmt.getFunctionValue(ss.str(), r); m->assignFunctionDefinition(f, val); // ufmt.debugPrint( std::cout, m ); } diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index f5f6ff565..6dcc0f72f 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -465,11 +465,13 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const return std::string("uf_card"); } -SortModel::SortModel(TypeNode tn, +SortModel::SortModel(Env& env, + TypeNode tn, TheoryState& state, TheoryInferenceManager& im, CardinalityExtension* thss) - : d_type(tn), + : EnvObj(env), + d_type(tn), d_state(state), d_im(im), d_thss(thss), @@ -1011,7 +1013,7 @@ int SortModel::addSplit(Region* r) if (!s.isNull() ){ //add lemma to output channel Assert(s.getKind() == EQUAL); - Node ss = Rewriter::rewrite( s ); + Node ss = rewrite(s); if( ss.getKind()!=EQUAL ){ Node b_t = NodeManager::currentNM()->mkConst( true ); Node b_f = NodeManager::currentNM()->mkConst( false ); @@ -1620,7 +1622,7 @@ void CardinalityExtension::preRegisterTerm(TNode n) if (tn.isSort()) { Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl; - rm = new SortModel(tn, d_state, d_im, this); + rm = new SortModel(d_env, tn, d_state, d_im, this); } if (rm) { diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 7a6d44ee9..822f13f23 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -48,7 +48,7 @@ class CardinalityExtension : protected EnvObj * Information for incremental conflict/clique finding for a * particular sort. */ - class SortModel + class SortModel : protected EnvObj { private: std::map< Node, std::vector< int > > d_totality_lems; @@ -281,7 +281,8 @@ class CardinalityExtension : protected EnvObj void simpleCheckCardinality(); public: - SortModel(TypeNode tn, + SortModel(Env& env, + TypeNode tn, TheoryState& state, TheoryInferenceManager& im, CardinalityExtension* thss); diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 71688fc15..856dce011 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -31,7 +31,8 @@ namespace theory { namespace eq { ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee) - : EagerProofGenerator(env.getProofNodeManager(), + : EnvObj(env), + EagerProofGenerator(env.getProofNodeManager(), env.getUserContext(), "pfee::" + ee.identify()), d_ee(ee), @@ -180,7 +181,7 @@ TrustNode ProofEqEngine::assertConflict(Node lit) // lit may not be equivalent to false, but should rewrite to false if (lit != d_false) { - Assert(Rewriter::rewrite(lit) == d_false) + Assert(rewrite(lit) == d_false) << "pfee::assertConflict: conflict literal is not rewritable to " "false"; std::vector exp; diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index fc8520dd1..47bb2fe0d 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -27,6 +27,7 @@ #include "proof/buffered_proof_generator.h" #include "proof/eager_proof_generator.h" #include "proof/lazy_proof.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -80,7 +81,7 @@ class EqualityEngine; * - explain, for explaining why a literal is true in the current state. * Details on these methods can be found below. */ -class ProofEqEngine : public EagerProofGenerator +class ProofEqEngine : protected EnvObj, public EagerProofGenerator { typedef context::CDHashSet NodeSet; typedef context::CDHashMap> NodeProofMap; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 861f12d64..6d8d421ba 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -57,7 +57,11 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int } } -Node UfModelTreeNode::getFunctionValue(std::vector& args, int index, Node argDefaultValue, bool simplify) { +Node UfModelTreeNode::getFunctionValue(const std::vector& args, + int index, + Node argDefaultValue, + bool simplify) +{ if(!d_data.empty()) { Node defaultValue = argDefaultValue; if(d_data.find(Node::null()) != d_data.end()) { @@ -222,16 +226,19 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector } } -Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){ - Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify ); - if(simplify) { - body = Rewriter::rewrite( body ); +Node UfModelTree::getFunctionValue(const std::vector& args, Rewriter* r) +{ + Node body = d_tree.getFunctionValue(args, 0, Node::null(), r != nullptr); + if (r != nullptr) + { + body = r->rewrite(body); } Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args); return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body); } -Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){ +Node UfModelTree::getFunctionValue(const std::string& argPrefix, Rewriter* r) +{ TypeNode type = d_op.getType(); std::vector< Node > vars; for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); } - return getFunctionValue( vars, simplify ); + return getFunctionValue(vars, r); } } // namespace uf diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index f386c2f99..e4235623e 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -26,6 +26,7 @@ namespace cvc5 { namespace theory { class TheoryModel; +class Rewriter; namespace uf { @@ -45,7 +46,10 @@ public: /** setValue function */ void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); /** getFunctionValue */ - Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true ); + Node getFunctionValue(const std::vector& args, + int index, + Node argDefaultValue, + bool simplify = true); /** update function */ void update( TheoryModel* m ); /** simplify function */ @@ -92,11 +96,12 @@ public: d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); } /** getFunctionValue - * Returns a representation of this function. - */ - Node getFunctionValue( std::vector< Node >& args, bool simplify = true ); + * Returns a representation of this function. The body of the function is + * rewritten if r is non-null. + */ + Node getFunctionValue(const std::vector& args, Rewriter* r); /** getFunctionValue for args with set prefix */ - Node getFunctionValue( const char* argPrefix, bool simplify = true ); + Node getFunctionValue(const std::string& argPrefix, Rewriter* r); /** update * This will update all values in the tree to be representatives in m. */ -- 2.30.2