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.
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
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),
// 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<Node> progs(q[0].begin(), q[0].end());
// compute single invocation partition
Node qq;
if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL)
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<Node> 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<Node> 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<Node> 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)
#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 {
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;
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
/** preregister conjecture */
void preregisterConjecture( Node q );
- Node getTransPre(Node prog) const {
- std::map<Node, Node>::const_iterator location = d_trans_pre.find(prog);
- return location->second;
- }
-
- Node getTransPost(Node prog) const {
- std::map<Node, Node>::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<Node, Node>::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<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog);
- if( tmpla != d_templ_arg.end() ){
- return tmpla->second;
- }else{
- return Node::null();
- }
- }
-
private:
/** solve trivial
*
#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"
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)),
{
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);
}
}
}
// 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")
// 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
#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 {
std::unique_ptr<DecisionStrategy> d_feasible_strategy;
/** single invocation utility */
std::unique_ptr<CegSingleInv> d_ceg_si;
+ /** template inference utility */
+ std::unique_ptr<SygusTemplateInfer> d_templInfer;
/** utility for static preprocessing and analysis of conjectures */
std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
/** grammar utility */
--- /dev/null
+/********************* */
+/*! \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<Node> 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<Node> 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<Node, Node>::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<Node, Node>::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
--- /dev/null
+/********************* */
+/*! \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 <map>
+
+#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<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;
+ /** transition inference module */
+ TransitionInference d_ti;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} /* namespace CVC4 */
+
+#endif
projects / cvc5.git / commitdiff