From 04dc5b60462dc367fe1b99254c215957006f7b21 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Nov 2020 23:06:13 -0600 Subject: [PATCH] Split sygus template inference to its own file (#5388) This splits techniques for inferring templates for functions-to-synthesize to their own file. This is work towards cleaning up the single invocation utility, which will be undergoing some additions. --- src/CMakeLists.txt | 2 + .../sygus/ce_guided_single_inv.cpp | 173 +-------------- .../quantifiers/sygus/ce_guided_single_inv.h | 43 +--- .../sygus/cegis_core_connective.cpp | 1 + .../quantifiers/sygus/synth_conjecture.cpp | 18 +- .../quantifiers/sygus/synth_conjecture.h | 3 + .../quantifiers/sygus/template_infer.cpp | 205 ++++++++++++++++++ src/theory/quantifiers/sygus/template_infer.h | 76 +++++++ 8 files changed, 301 insertions(+), 220 deletions(-) create mode 100644 src/theory/quantifiers/sygus/template_infer.cpp create mode 100644 src/theory/quantifiers/sygus/template_infer.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e763565ad..c6b41e94a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -761,6 +761,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/synth_conjecture.h theory/quantifiers/sygus/synth_engine.cpp theory/quantifiers/sygus/synth_engine.h + theory/quantifiers/sygus/template_infer.cpp + theory/quantifiers/sygus/template_infer.h theory/quantifiers/sygus/term_database_sygus.cpp theory/quantifiers/sygus/term_database_sygus.h theory/quantifiers/sygus/type_info.cpp diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 4b45072f7..ac7d6efc7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -34,9 +34,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p) +CegSingleInv::CegSingleInv(QuantifiersEngine* qe) : d_qe(qe), - d_parent(p), d_sip(new SingleInvocationPartition), d_sol(new CegSingleInvSol(qe)), d_isSolved(false), @@ -61,20 +60,7 @@ void CegSingleInv::initialize(Node q) // infer single invocation-ness // get the variables - std::vector< Node > progs; - std::map< Node, std::vector< Node > > prog_vars; - for (const Node& sf : q[0]) - { - progs.push_back( sf ); - Node sfvl = CegGrammarConstructor::getSygusVarList(sf); - if (!sfvl.isNull()) - { - for (const Node& sfv : sfvl) - { - prog_vars[sf].push_back(sfv); - } - } - } + std::vector progs(q[0].begin(), q[0].end()); // compute single invocation partition Node qq; if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL) @@ -113,163 +99,8 @@ void CegSingleInv::initialize(Node q) if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE) { d_single_invocation = true; - return; - } - } - // We are processing without single invocation techniques, now check if - // we should fix an invariant template (post-condition strengthening or - // pre-condition weakening). - options::SygusInvTemplMode tmode = options::sygusInvTemplMode(); - if (tmode != options::SygusInvTemplMode::NONE) - { - // currently only works for single predicate synthesis - if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) - { - tmode = options::SygusInvTemplMode::NONE; - } - else if (!options::sygusInvTemplWhenSyntax()) - { - // only use invariant templates if no syntactic restrictions - if (CegGrammarConstructor::hasSyntaxRestrictions(q)) - { - tmode = options::SygusInvTemplMode::NONE; - } - } - } - - if (tmode == options::SygusInvTemplMode::NONE) - { - // not processing invariant templates - return; - } - // if we are doing invariant templates, then construct the template - Trace("sygus-si") << "- Do transition inference..." << std::endl; - d_ti[q].process(qq, q[0][0]); - Trace("cegqi-inv") << std::endl; - Node prog = d_ti[q].getFunction(); - if (!d_ti[q].isComplete()) - { - // the invariant could not be inferred - return; - } - Assert(prog == q[0][0]); - NodeManager* nm = NodeManager::currentNM(); - // map the program back via non-single invocation map - std::vector prog_templ_vars; - d_ti[q].getVariables(prog_templ_vars); - d_trans_pre[prog] = d_ti[q].getPreCondition(); - d_trans_post[prog] = d_ti[q].getPostCondition(); - Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; - Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; - std::vector sivars; - d_sip->getSingleInvocationVariables(sivars); - Node invariant = d_sip->getFunctionInvocationFor(prog); - if (invariant.isNull()) - { - // the conjecture did not have an instance of the invariant - // (e.g. it is trivially true/false). - return; - } - invariant = invariant.substitute(sivars.begin(), - sivars.end(), - prog_templ_vars.begin(), - prog_templ_vars.end()); - Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - - // store simplified version of quantified formula - d_simp_quant = d_sip->getFullSpecification(); - std::vector new_bv; - for( const Node& v : sivars ) - { - new_bv.push_back(nm->mkBoundVar(v.getType())); - } - d_simp_quant = d_simp_quant.substitute( - sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); - Assert(q[1].getKind() == NOT && q[1][0].getKind() == FORALL); - for (const Node& v : q[1][0][0]) - { - new_bv.push_back(v); - } - d_simp_quant = - nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, new_bv), d_simp_quant) - .negate(); - d_simp_quant = Rewriter::rewrite(d_simp_quant); - d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]); - Trace("sygus-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; - - // construct template argument - d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType()); - - // construct template - Node templ; - if (options::sygusInvAutoUnfold()) - { - if (d_ti[q].isComplete()) - { - Trace("cegqi-inv-auto-unfold") - << "Automatic deterministic unfolding... " << std::endl; - // auto-unfold - DetTrace dt; - int init_dt = d_ti[q].initializeTrace(dt); - if (init_dt == 0) - { - Trace("cegqi-inv-auto-unfold") << " Init : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << std::endl; - unsigned counter = 0; - unsigned status = 0; - while (counter < 100 && status == 0) - { - status = d_ti[q].incrementTrace(dt); - counter++; - Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") - << "...status = " << status << std::endl; - } - if (status == 1) - { - // we have a trivial invariant - templ = d_ti[q].constructFormulaTrace(dt); - Trace("cegqi-inv") << "By finite deterministic terminating trace, a " - "solution invariant is : " - << std::endl; - Trace("cegqi-inv") << " " << templ << std::endl; - // this should be unnecessary - templ = nm->mkNode(AND, templ, d_templ_arg[prog]); - } - } - else - { - Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; - } - } - } - Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ - << std::endl; - if (templ.isNull()) - { - if (tmode == options::SygusInvTemplMode::PRE) - { - templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]); - } - else - { - Assert(tmode == options::SygusInvTemplMode::POST); - templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]); } } - Trace("cegqi-inv") << " template (pre-substitution) : " << templ - << std::endl; - Assert(!templ.isNull()); - // subsitute the template arguments - Assert(prog_templ_vars.size() == prog_vars[prog].size()); - templ = templ.substitute(prog_templ_vars.begin(), - prog_templ_vars.end(), - prog_vars[prog].begin(), - prog_vars[prog].end()); - Trace("cegqi-inv") << " template : " << templ << std::endl; - d_templ[prog] = templ; } void CegSingleInv::finishInit(bool syntaxRestricted) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 642415935..0e1ddba1f 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -22,7 +22,6 @@ #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" -#include "theory/quantifiers/sygus/transition_inference.h" namespace CVC4 { namespace theory { @@ -52,12 +51,8 @@ class CegSingleInv private: /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; - /** the parent of this class */ - SynthConjecture* d_parent; // single invocation inference utility SingleInvocationPartition* d_sip; - // transition inference module for each function to synthesize - std::map< Node, TransitionInference > d_ti; // solution reconstruction CegSingleInvSol* d_sol; @@ -100,16 +95,9 @@ class CegSingleInv bool d_single_invocation; // single invocation portion of quantified formula Node d_single_inv; - // transition relation version per program - std::map< Node, Node > d_trans_pre; - std::map< Node, Node > d_trans_post; - // the template for each function to synthesize - std::map< Node, Node > d_templ; - // the template argument for each function to synthesize (occurs in exactly one position of its template) - std::map< Node, Node > d_templ_arg; public: - CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p); + CegSingleInv(QuantifiersEngine* qe); ~CegSingleInv(); // get simplified conjecture @@ -144,35 +132,6 @@ class CegSingleInv /** preregister conjecture */ void preregisterConjecture( Node q ); - Node getTransPre(Node prog) const { - std::map::const_iterator location = d_trans_pre.find(prog); - return location->second; - } - - Node getTransPost(Node prog) const { - std::map::const_iterator location = d_trans_post.find(prog); - return location->second; - } - // get template for program prog. This returns a term of the form t[x] where x is the template argument (see below) - Node getTemplate(Node prog) const { - std::map::const_iterator tmpl = d_templ.find(prog); - if( tmpl!=d_templ.end() ){ - return tmpl->second; - }else{ - return Node::null(); - } - } - // get the template argument for program prog. - // This is a variable which indicates the position of the function/predicate to synthesize. - Node getTemplateArg(Node prog) const { - std::map::const_iterator tmpla = d_templ_arg.find(prog); - if( tmpla != d_templ_arg.end() ){ - return tmpla->second; - }else{ - return Node::null(); - } - } - private: /** solve trivial * diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 33fce2e84..4549a0945 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -21,6 +21,7 @@ #include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/transition_inference.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/smt_engine_subsolver.h" diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index c65ac9e65..2b4eba3b7 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -50,7 +50,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qe, this)), + d_ceg_si(new CegSingleInv(qe)), + d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), @@ -116,15 +117,18 @@ void SynthConjecture::assign(Node q) { d_ceg_si->initialize(d_simp_quant); d_simp_quant = d_ceg_si->getSimplifiedConjecture(); + if (!d_ceg_si->isSingleInvocation()) + { + d_templInfer->initialize(d_simp_quant); + } // carry the templates - for (unsigned i = 0; i < q[0].getNumChildren(); i++) + for (const Node& v : q[0]) { - Node v = q[0][i]; - Node templ = d_ceg_si->getTemplate(v); + Node templ = d_templInfer->getTemplate(v); if (!templ.isNull()) { templates[v] = templ; - templates_arg[v] = d_ceg_si->getTemplateArg(v); + templates_arg[v] = d_templInfer->getTemplateArg(v); } } } @@ -1334,7 +1338,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, // check if there was a template Node sf = d_quant[0][i]; - Node templ = d_ceg_si->getTemplate(sf); + Node templ = d_templInfer->getTemplate(sf); if (!templ.isNull()) { Trace("cegqi-inv-debug") @@ -1342,7 +1346,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, // if it was not embedded into the grammar if (!options::sygusTemplEmbedGrammar()) { - TNode templa = d_ceg_si->getTemplateArg(sf); + TNode templa = d_templInfer->getTemplateArg(sf); // make the builtin version of the full solution sol = d_tds->sygusToBuiltin(sol, sol.getType()); Trace("cegqi-inv") << "Builtin version of solution is : " << sol diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 5572032b6..7f499b1b3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -33,6 +33,7 @@ #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "theory/quantifiers/sygus/sygus_stats.h" +#include "theory/quantifiers/sygus/template_infer.h" namespace CVC4 { namespace theory { @@ -216,6 +217,8 @@ class SynthConjecture std::unique_ptr d_feasible_strategy; /** single invocation utility */ std::unique_ptr d_ceg_si; + /** template inference utility */ + std::unique_ptr d_templInfer; /** utility for static preprocessing and analysis of conjectures */ std::unique_ptr d_ceg_proc; /** grammar utility */ diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp new file mode 100644 index 000000000..2f6964f3a --- /dev/null +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -0,0 +1,205 @@ +/********************* */ +/*! \file template_infer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief utility for processing single invocation synthesis conjectures + ** + **/ +#include "theory/quantifiers/sygus/template_infer.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/term_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void SygusTemplateInfer::initialize(Node q) +{ + Assert(d_quant.isNull()); + Assert(q.getKind() == FORALL); + d_quant = q; + // We are processing without single invocation techniques, now check if + // we should fix an invariant template (post-condition strengthening or + // pre-condition weakening). + options::SygusInvTemplMode tmode = options::sygusInvTemplMode(); + if (tmode != options::SygusInvTemplMode::NONE) + { + // currently only works for single predicate synthesis + if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) + { + tmode = options::SygusInvTemplMode::NONE; + } + else if (!options::sygusInvTemplWhenSyntax()) + { + // only use invariant templates if no syntactic restrictions + if (CegGrammarConstructor::hasSyntaxRestrictions(q)) + { + tmode = options::SygusInvTemplMode::NONE; + } + } + } + + if (tmode == options::SygusInvTemplMode::NONE) + { + // not processing invariant templates + return; + } + + Node qq; + if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL) + { + qq = q[1][0][1]; + } + else + { + qq = TermUtil::simpleNegate(q[1]); + } + if (qq.isConst()) + { + // trivial, do not use transition inference + return; + } + + // if we are doing invariant templates, then construct the template + Trace("sygus-si") << "- Do transition inference..." << std::endl; + d_ti.process(qq, q[0][0]); + Trace("cegqi-inv") << std::endl; + Node prog = d_ti.getFunction(); + if (!d_ti.isComplete()) + { + // the invariant could not be inferred + return; + } + Assert(prog == q[0][0]); + NodeManager* nm = NodeManager::currentNM(); + // map the program back via non-single invocation map + std::vector prog_templ_vars; + d_ti.getVariables(prog_templ_vars); + d_trans_pre[prog] = d_ti.getPreCondition(); + d_trans_post[prog] = d_ti.getPostCondition(); + Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + + // construct template argument + TypeNode atn = prog.getType(); + if (atn.isFunction()) + { + atn = atn.getRangeType(); + } + d_templ_arg[prog] = nm->mkSkolem("I", atn); + + // construct template + Node templ; + if (options::sygusInvAutoUnfold()) + { + if (d_ti.isComplete()) + { + Trace("cegqi-inv-auto-unfold") + << "Automatic deterministic unfolding... " << std::endl; + // auto-unfold + DetTrace dt; + int init_dt = d_ti.initializeTrace(dt); + if (init_dt == 0) + { + Trace("cegqi-inv-auto-unfold") << " Init : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") << std::endl; + unsigned counter = 0; + unsigned status = 0; + while (counter < 100 && status == 0) + { + status = d_ti.incrementTrace(dt); + counter++; + Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") + << "...status = " << status << std::endl; + } + if (status == 1) + { + // we have a trivial invariant + templ = d_ti.constructFormulaTrace(dt); + Trace("cegqi-inv") << "By finite deterministic terminating trace, a " + "solution invariant is : " + << std::endl; + Trace("cegqi-inv") << " " << templ << std::endl; + // this should be unnecessary + templ = nm->mkNode(AND, templ, d_templ_arg[prog]); + } + } + else + { + Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; + } + } + } + Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ + << std::endl; + if (templ.isNull()) + { + if (tmode == options::SygusInvTemplMode::PRE) + { + templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]); + } + else + { + Assert(tmode == options::SygusInvTemplMode::POST); + templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]); + } + } + Trace("cegqi-inv") << " template (pre-substitution) : " << templ + << std::endl; + Assert(!templ.isNull()); + + // get the variables + Node sfvl = CegGrammarConstructor::getSygusVarList(prog); + if (!sfvl.isNull()) + { + std::vector prog_vars(sfvl.begin(), sfvl.end()); + // subsitute the template arguments + Trace("cegqi-inv") << "vars : " << prog_templ_vars << " " << prog_vars + << std::endl; + Assert(prog_templ_vars.size() == prog_vars.size()); + templ = templ.substitute(prog_templ_vars.begin(), + prog_templ_vars.end(), + prog_vars.begin(), + prog_vars.end()); + } + Trace("cegqi-inv") << " template : " << templ << std::endl; + d_templ[prog] = templ; +} + +Node SygusTemplateInfer::getTemplate(Node prog) const +{ + std::map::const_iterator tmpl = d_templ.find(prog); + if (tmpl != d_templ.end()) + { + return tmpl->second; + } + return Node::null(); +} + +Node SygusTemplateInfer::getTemplateArg(Node prog) const +{ + std::map::const_iterator tmpla = d_templ_arg.find(prog); + if (tmpla != d_templ_arg.end()) + { + return tmpla->second; + } + return Node::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h new file mode 100644 index 000000000..97879dc22 --- /dev/null +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -0,0 +1,76 @@ +/********************* */ +/*! \file template_infer.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief utility for inferring templates for invariant problems + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H + +#include + +#include "expr/node.h" +#include "theory/quantifiers/sygus/transition_inference.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * 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 +{ + public: + SygusTemplateInfer() {} + ~SygusTemplateInfer() {} + /** + * Initialize this class for synthesis conjecture q. If applicable, the + * templates for functions-to-synthesize for q are accessible by the + * calls below afterwards. + */ + void initialize(Node q); + /** + * Get template for program prog. This returns a term of the form t[x] where + * x is the template argument (see below) + */ + Node getTemplate(Node prog) const; + /** + * Get the template argument for program prog. This is a variable which + * indicates the position of the function/predicate to synthesize. + */ + Node getTemplateArg(Node prog) const; + + private: + /** The quantified formula we initialized with */ + Node d_quant; + /** transition relation pre and post version per function to synthesize */ + std::map d_trans_pre; + std::map d_trans_post; + /** the template for each function to synthesize */ + std::map d_templ; + /** + * The template argument for each function to synthesize (occurs in exactly + * one position of its template) + */ + std::map d_templ_arg; + /** transition inference module */ + TransitionInference d_ti; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif -- 2.30.2