Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.
This includes improvements to the robustness of the sygus solver.
theory/quantifiers/sygus/sygus_unif_strat.h \
theory/quantifiers/sygus/term_database_sygus.cpp \
theory/quantifiers/sygus/term_database_sygus.h \
+ theory/quantifiers/sygus_inference.cpp \
+ theory/quantifiers/sygus_inference.h \
theory/quantifiers/sygus_sampler.cpp \
theory/quantifiers/sygus_sampler.h \
theory/quantifiers/symmetry_breaking.cpp \
### Synthesis options
+[[option]]
+ name = "sygusInference"
+ category = "regular"
+ long = "sygus-inference"
+ type = "bool"
+ default = "false"
+ read_only = false
+ help = "attempt to preprocess arbitrary inputs to sygus conjectures"
+
[[option]]
name = "ceGuidedInst"
category = "regular"
#include "theory/bv/bvintropow2.h"
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/logic_info.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/global_negate.h"
#include "theory/quantifiers/macros.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/single_inv_partition.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus_inference.h"
#include "theory/quantifiers/term_util.h"
#include "theory/sort_inference.h"
#include "theory/strings/theory_strings.h"
*/
}
+ // sygus inference may require datatypes
+ if (options::sygusInference())
+ {
+ d_logic = d_logic.getUnlockedCopy();
+ d_logic.enableTheory(THEORY_DATATYPES);
+ d_logic.lock();
+ }
+
if ((options::checkModels() || options::checkSynthSol())
&& !options::produceAssertions())
{
}
//apply counterexample guided instantiation options
+ // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
+ if (options::sygusInference())
+ {
+ if (!options::ceGuidedInst.wasSetByUser())
+ {
+ options::ceGuidedInst.set(true);
+ }
+ // optimization: apply preskolemization, makes it succeed more often
+ if (!options::preSkolemQuant.wasSetByUser())
+ {
+ options::preSkolemQuant.set(true);
+ }
+ if (!options::preSkolemQuantNested.wasSetByUser())
+ {
+ options::preSkolemQuantNested.set(true);
+ }
+ }
if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
if( !options::ceGuidedInst.wasSetByUser() ){
options::ceGuidedInst.set( true );
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- // global negation of the formula
- if (options::globalNegate())
+ if (options::sygusInference())
+ {
+ // try recast as sygus
+ quantifiers::SygusInference si;
+ if (si.simplify(d_assertions.ref()))
+ {
+ Trace("smt-proc") << "...converted to sygus conjecture." << std::endl;
+ d_smt.d_globalNegation = !d_smt.d_globalNegation;
+ }
+ }
+ else if (options::globalNegate())
{
+ // global negation of the formula
quantifiers::GlobalNegate gn;
gn.simplify(d_assertions.ref());
d_smt.d_globalNegation = !d_smt.d_globalNegation;
static Node rewriteRewriteRule( Node r );
static bool containsQuantifiers( Node n );
static bool isPrenexNormalForm( Node n );
+ /** preprocess
+ *
+ * This returns the result of applying simple quantifiers-specific
+ * preprocessing to n, including but not limited to:
+ * - rewrite rule elimination,
+ * - pre-skolemization,
+ * - aggressive prenexing.
+ * The argument isInst is set to true if n is an instance of a previously
+ * registered quantified formula. If this flag is true, we do not apply
+ * certain steps like pre-skolemization since we know they will have no
+ * effect.
+ */
static Node preprocess( Node n, bool isInst = false );
static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
d_simp_quant = q;
Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl;
// infer single invocation-ness
+
+ // get the variables
std::vector< Node > progs;
std::map< Node, std::vector< Node > > prog_vars;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- Node sf = q[0][i];
+ for (const Node& sf : q[0])
+ {
progs.push_back( sf );
- Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
- for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
- prog_vars[sf].push_back( sfvl[j] );
+ Node sfvl = CegGrammarConstructor::getSygusVarList(sf);
+ if (!sfvl.isNull())
+ {
+ for (const Node& sfv : sfvl)
+ {
+ prog_vars[sf].push_back(sfv);
+ }
}
}
// compute single invocation partition
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;
collectTerms( q[1], extra_cons );
}
+ NodeManager* nm = NodeManager::currentNM();
+
std::vector< Node > qchildren;
std::map< Node, Node > synth_fun_vars;
std::vector< Node > ebvl;
Node qbody_subs = q[1];
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
Node sf = q[0][i];
- // v encodes the syntactic restrictions (via an inductive datatype) on sf
- // from the input
+ // if non-null, v encodes the syntactic restrictions (via an inductive
+ // datatype) on sf from the input.
Node v = sf.getAttribute(SygusSynthGrammarAttribute());
- Assert(!v.isNull());
- Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
+ TypeNode preGrammarType;
+ if (!v.isNull())
+ {
+ preGrammarType = v.getType();
+ }
+ else
+ {
+ // otherwise, the grammar is the default for the range of the function
+ preGrammarType = sf.getType();
+ if (preGrammarType.isFunction())
+ {
+ preGrammarType = preGrammarType.getRangeType();
+ }
+ }
+ Node sfvl = getSygusVarList(sf);
// sfvl may be null for constant synthesis functions
Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+ // the actual sygus datatype we will use (normalized below)
TypeNode tn;
std::stringstream ss;
ss << sf;
- if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
- tn = v.getType();
+ if (preGrammarType.isDatatype()
+ && static_cast<DatatypeType>(preGrammarType.toType())
+ .getDatatype()
+ .isSygus())
+ {
+ tn = preGrammarType;
}else{
// check which arguments are irrelevant
std::unordered_set<unsigned> arg_irrelevant;
// make the default grammar
tn = mkSygusDefaultType(
- v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant);
+ preGrammarType, sfvl, ss.str(), extra_cons, term_irrelevant);
}
+
// normalize type
SygusGrammarNorm sygus_norm(d_qe);
tn = sygus_norm.normalizeSygusType(tn, sfvl);
std::vector< Node > largs;
for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
schildren.push_back( sfvl[j] );
- largs.push_back( NodeManager::currentNM()->mkBoundVar( sfvl[j].getType() ) );
+ largs.push_back(nm->mkBoundVar(sfvl[j].getType()));
}
std::vector< Node > subsfn_children;
subsfn_children.push_back( sf );
subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() );
- Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children );
+ Node subsfn = nm->mkNode(kind::APPLY_UF, subsfn_children);
TNode subsf = subsfn;
Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl;
templ = templ.substitute( templ_arg, subsf );
// substitute lambda arguments
templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() );
- Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ );
+ Node subsn =
+ nm->mkNode(kind::LAMBDA, nm->mkNode(BOUND_VAR_LIST, largs), templ);
TNode var = sf;
TNode subs = subsn;
Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl;
// ev is the first-order variable corresponding to this synth fun
std::stringstream ssf;
ssf << "f" << sf;
- Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn );
+ Node ev = nm->mkBoundVar(ssf.str(), tn);
ebvl.push_back( ev );
synth_fun_vars[sf] = ev;
Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl;
}
- qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
+ qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl));
if( qbody_subs!=q[1] ){
Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
qbody_subs = Rewriter::rewrite( qbody_subs );
if( q.getNumChildren()==3 ){
qchildren.push_back( q[2] );
}
- return NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
+ return nm->mkNode(kind::FORALL, qchildren);
}
Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){
return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
}
+Node CegGrammarConstructor::getSygusVarList(Node f)
+{
+ Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
+ if (sfvl.isNull() && f.getType().isFunction())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<TypeNode> argTypes = f.getType().getArgTypes();
+ // make default variable list if none was specified by input
+ std::vector<Node> bvs;
+ for (unsigned j = 0, size = argTypes.size(); j < size; j++)
+ {
+ std::stringstream ss;
+ ss << "arg" << j;
+ bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
+ }
+ sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
+ f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
+ }
+ return sfvl;
+}
+
}/* namespace CVC4::theory::quantifiers */
}/* namespace CVC4::theory */
}/* namespace CVC4 */
* fun is for naming
*/
static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
+ /**
+ * Returns the sygus variable list for function-to-synthesize variable f.
+ * These are the names of the arguments of f, which should be included in the
+ * grammar for f. This returns either the variable list set explicitly via the
+ * attribute SygusSynthFunVarListAttribute, or a fresh variable list of the
+ * proper type otherwise. It will return null if f is not a function.
+ */
+ static Node getSygusVarList(Node f);
/**
* Returns true iff there are syntax restrictions on the
* functions-to-synthesize of sygus conjecture q.
*/
static bool hasSyntaxRestrictions(Node q);
-
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
--- /dev/null
+/********************* */
+/*! \file sygus_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Implementation of sygus_inference
+ **/
+
+#include "theory/quantifiers/sygus_inference.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusInference::SygusInference() {}
+
+bool SygusInference::simplify(std::vector<Node>& assertions)
+{
+ Trace("sygus-infer") << "Sygus inference : " << std::endl;
+
+ if (assertions.empty())
+ {
+ Trace("sygus-infer") << "...fail: empty assertions." << std::endl;
+ return false;
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ // collect free variables in all assertions
+ std::vector<Node> qvars;
+ std::map<TypeNode, std::vector<Node> > qtvars;
+ std::vector<Node> free_functions;
+
+ std::vector<TNode> visit;
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+
+ // add top-level conjuncts to eassertions
+ std::vector<Node> assertions_proc = assertions;
+ std::vector<Node> eassertions;
+ unsigned index = 0;
+ while (index < assertions_proc.size())
+ {
+ Node ca = assertions_proc[index];
+ if (ca.getKind() == AND)
+ {
+ for (const Node& ai : ca)
+ {
+ assertions_proc.push_back(ai);
+ }
+ }
+ else
+ {
+ eassertions.push_back(ca);
+ }
+ }
+
+ // process eassertions
+ std::vector<Node> processed_assertions;
+ for (const Node& as : eassertions)
+ {
+ // substitution for this assertion
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ std::map<TypeNode, unsigned> type_count;
+ Node pas = as;
+ // rewrite
+ pas = Rewriter::rewrite(pas);
+ Trace("sygus-infer") << " " << pas << std::endl;
+ if (pas.getKind() == FORALL)
+ {
+ // preprocess the quantified formula
+ pas = quantifiers::QuantifiersRewriter::preprocess(pas);
+ Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl;
+
+ pas = pas[1];
+ // infer prefix
+ for (const Node& v : pas[0])
+ {
+ TypeNode tnv = v.getType();
+ unsigned vnum = type_count[tnv];
+ type_count[tnv]++;
+ if (vnum < qtvars[tnv].size())
+ {
+ vars.push_back(v);
+ subs.push_back(qtvars[tnv][vnum]);
+ }
+ else
+ {
+ Assert(vnum == qtvars[tnv].size());
+ qtvars[tnv].push_back(v);
+ qvars.push_back(v);
+ }
+ }
+ if (!vars.empty())
+ {
+ pas =
+ pas.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ }
+ }
+ Trace("sygus-infer-debug") << " ...substituted to " << pas << std::endl;
+
+ // collect free functions, ensure no quantified formulas
+ TNode cur = pas;
+ // compute free variables
+ visit.push_back(cur);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ if (cur.getKind() == APPLY_UF)
+ {
+ Node op = cur.getOperator();
+ if (std::find(free_functions.begin(), free_functions.end(), op)
+ == free_functions.end())
+ {
+ free_functions.push_back(op);
+ }
+ }
+ else if (cur.getKind() == FORALL)
+ {
+ Trace("sygus-infer")
+ << "...fail: non-top-level quantifier." << std::endl;
+ return false;
+ }
+ for (const TNode& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ } while (!visit.empty());
+ processed_assertions.push_back(pas);
+ }
+
+ // if no free function symbols, there is no use changing into SyGuS
+ if (free_functions.empty())
+ {
+ Trace("sygus-infer") << "...fail: no free function symbols." << std::endl;
+ return false;
+ }
+
+ // conjunction of the assertions
+ Node body;
+ if (processed_assertions.size() == 1)
+ {
+ body = processed_assertions[0];
+ }
+ else
+ {
+ body = nm->mkNode(AND, processed_assertions);
+ }
+
+ // for each free function symbol, make a bound variable of the same type
+ std::vector<Node> ff_vars;
+ for (const Node& ff : free_functions)
+ {
+ Node ffv = nm->mkBoundVar(ff.getType());
+ ff_vars.push_back(ffv);
+ }
+ // substitute free functions -> variables
+ body = body.substitute(free_functions.begin(),
+ free_functions.end(),
+ ff_vars.begin(),
+ ff_vars.end());
+
+ // quantify the body
+ if (!qvars.empty())
+ {
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars);
+ body = nm->mkNode(EXISTS, bvl, body.negate());
+ }
+
+ // sygus attribute to mark the conjecture as a sygus conjecture
+ Node sygusVar = nm->mkBoundVar("sygus", nm->booleanType());
+ SygusAttribute ca;
+ sygusVar.setAttribute(ca, true);
+ Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
+ Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr);
+
+ Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars);
+
+ body = nm->mkNode(FORALL, fbvl, body, instAttrList);
+
+ Trace("sygus-infer") << "...return : " << body << std::endl;
+
+ // replace all assertions except the first with true
+ Node truen = nm->mkConst(true);
+ for (unsigned i = 0, size = assertions.size(); i < size; i++)
+ {
+ if (i == 0)
+ {
+ assertions[i] = body;
+ }
+ else
+ {
+ assertions[i] = truen;
+ }
+ }
+ return true;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_inference.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 sygus_inference
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** SygusInference
+ *
+ * A preprocessing utility to turn a set of (quantified) assertions into a
+ * single SyGuS conjecture.
+ */
+class SygusInference
+{
+ public:
+ SygusInference();
+ ~SygusInference() {}
+ /** simplify assertions
+ *
+ * Either replaces assertions with the negation of an equivalent SyGuS
+ * conjecture and returns true, or otherwise returns false.
+ */
+ bool simplify(std::vector<Node>& assertions);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H */
regress1/quantifiers/smtlibe99bbe.smt2 \
regress1/quantifiers/smtlibf957ea.smt2 \
regress1/quantifiers/stream-x2014-09-18-unsat.smt2 \
+ regress1/quantifiers/sygus-infer-nested.smt2 \
regress1/quantifiers/symmetric_unsat_7.smt2 \
regress1/quantifiers/z3.620661-no-fv-trigger.smt2 \
regress1/rels/addr_book_1.cvc \
--- /dev/null
+; COMMAND-LINE: --sygus-inference --no-check-models
+(set-logic LIA)
+(set-info :status sat)
+(assert (forall ((x Int) (y Int)) (or (<= x (+ y 1)) (exists ((z Int)) (and (> z y) (< z x))))))
+(check-sat)
projects / cvc5.git / commitdiff