From: Aina Niemetz Date: Fri, 3 Sep 2021 16:54:41 +0000 (-0700) Subject: sygus: Make CeSingleInv derive from EnvObj. (#7136) X-Git-Tag: cvc5-1.0.0~1276 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=da047b41fa252cf8087d95c91688b9cdc3ba6114;p=cvc5.git sygus: Make CeSingleInv derive from EnvObj. (#7136) This further reorders the header according to the code style guidelines. --- diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 99716806f..d2c616238 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -28,7 +28,6 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace cvc5::kind; @@ -38,10 +37,10 @@ namespace theory { namespace quantifiers { CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s) - : d_env(env), + : EnvObj(env), + d_isSolved(false), d_sip(new SingleInvocationPartition), d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)), - d_isSolved(false), d_single_invocation(false), d_treg(tr) { @@ -277,7 +276,7 @@ bool CegSingleInv::solve() Assert(inst.size() == vars.size()); Node ilem = body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end()); - ilem = Rewriter::rewrite(ilem); + ilem = rewrite(ilem); d_instConds.push_back(ilem); Trace("sygus-si") << " Instantiation Lemma: " << ilem << std::endl; } @@ -512,7 +511,7 @@ bool CegSingleInv::solveTrivial(Node q) // remake with eliminated nodes body = body.substitute( varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); - body = Rewriter::rewrite(body); + body = rewrite(body); // apply to subs // this ensures we behave correctly if we solve x before y in // x = y+1 ^ y = 2. @@ -520,7 +519,7 @@ bool CegSingleInv::solveTrivial(Node q) { subs[i] = subs[i].substitute( varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); - subs[i] = Rewriter::rewrite(subs[i]); + subs[i] = rewrite(subs[i]); } vars.insert(vars.end(), varsTmp.begin(), varsTmp.end()); subs.insert(subs.end(), subsTmp.begin(), subsTmp.end()); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index f7d6e5bb9..a0fac61d3 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -20,6 +20,7 @@ #include "context/cdlist.h" #include "expr/subs.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" @@ -40,63 +41,13 @@ class SygusReconstruct; // (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti). // For these techniques, we may generate a template (d_templ) which specifies a restricted // solution space. We may in turn embed this template as a SyGuS grammar. -class CegSingleInv +class CegSingleInv : protected EnvObj { - private: - //presolve - void collectPresolveEqTerms( Node n, - std::map< Node, std::vector< Node > >& teq ); - void getPresolveEqConjuncts( std::vector< Node >& vars, - std::vector< Node >& terms, - std::map< Node, std::vector< Node > >& teq, - Node n, std::vector< Node >& conj ); - private: - /** Reference to the env */ - Env& d_env; - // single invocation inference utility - SingleInvocationPartition* d_sip; - /** solution reconstruction */ - std::unique_ptr d_srcons; - - // list of skolems for each argument of programs - std::vector d_single_inv_arg_sk; - // program to solution index - std::map d_prog_to_sol_index; - // original conjecture - Node d_orig_conjecture; - - public: - //---------------------------------representation of the solution - /** - * The list of instantiations that suffice to show the first-order equivalent - * of the negated synthesis conjecture is unsatisfiable. - */ - std::vector > d_inst; - /** - * The list of instantiation lemmas, corresponding to instantiations of the - * first order conjecture for the term vectors above. - */ - std::vector d_instConds; - /** The solutions, without reconstruction to syntax */ - std::vector d_solutions; - /** The solutions, after reconstruction to syntax */ - std::vector d_rcSolutions; - /** is solved */ - bool d_isSolved; - //---------------------------------end representation of the solution - - private: - Node d_simp_quant; - // are we single invocation? - bool d_single_invocation; - // single invocation portion of quantified formula - Node d_single_inv; - public: CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s); ~CegSingleInv(); - // get simplified conjecture + /** Get simplified conjecture. */ Node getSimplifiedConjecture() { return d_simp_quant; } /** initialize this class for synthesis conjecture q */ void initialize( Node q ); @@ -146,7 +97,33 @@ class CegSingleInv /** preregister conjecture */ void preregisterConjecture( Node q ); + //---------------------------------representation of the solution + /** + * The list of instantiations that suffice to show the first-order equivalent + * of the negated synthesis conjecture is unsatisfiable. + */ + std::vector > d_inst; + /** + * The list of instantiation lemmas, corresponding to instantiations of the + * first order conjecture for the term vectors above. + */ + std::vector d_instConds; + /** The solutions, without reconstruction to syntax */ + std::vector d_solutions; + /** The solutions, after reconstruction to syntax */ + std::vector d_rcSolutions; + /** is solved */ + bool d_isSolved; + //---------------------------------end representation of the solution + private: + // presolve + void collectPresolveEqTerms(Node n, std::map >& teq); + void getPresolveEqConjuncts(std::vector& vars, + std::vector& terms, + std::map >& teq, + Node n, + std::vector& conj); /** solve trivial * * If this method returns true, it sets d_isSolved to true and adds @@ -165,6 +142,25 @@ class CegSingleInv * calls to the above method getSolutionFromInst. */ void setSolution(); + + // single invocation inference utility + SingleInvocationPartition* d_sip; + /** solution reconstruction */ + std::unique_ptr d_srcons; + + // list of skolems for each argument of programs + std::vector d_single_inv_arg_sk; + // program to solution index + std::map d_prog_to_sol_index; + // original conjecture + Node d_orig_conjecture; + + Node d_simp_quant; + // are we single invocation? + bool d_single_invocation; + // single invocation portion of quantified formula + Node d_single_inv; + /** Reference to the term registry */ TermRegistry& d_treg; /** The conjecture */