}
// if we are doing invariant templates, then construct the template
Trace("cegqi-si") << "- Do transition inference..." << std::endl;
- d_ti[q].process(qq);
+ d_ti[q].process(qq, q[0][0]);
Trace("cegqi-inv") << std::endl;
Node prog = d_ti[q].getFunction();
- if (prog.isNull())
+ 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;
for (const Node& s : symset)
{
TypeNode tn = s.getType();
- if (tn.isFirstClass())
- {
- std::stringstream ss;
- ss << s;
- Node var = nm->mkBoundVar(tn);
- syms.push_back(s);
- vars.push_back(var);
- Node vlv = nm->mkBoundVar(ss.str(), tn);
- varlist.push_back(vlv);
- varlistTypes.push_back(tn);
- // set that this variable encodes the term s
- SygusVarToTermAttribute sta;
- vlv.setAttribute(sta, s);
- }
+ // Notice that we allow for non-first class (e.g. function) variables here.
+ // This is applicable to the case where we are doing get-abduct in a logic
+ // with UF.
+ std::stringstream ss;
+ ss << s;
+ Node var = nm->mkBoundVar(tn);
+ syms.push_back(s);
+ vars.push_back(var);
+ Node vlv = nm->mkBoundVar(ss.str(), tn);
+ varlist.push_back(vlv);
+ varlistTypes.push_back(tn);
+ // set that this variable encodes the term s
+ SygusVarToTermAttribute sta;
+ vlv.setAttribute(sta, s);
}
// make the sygus variable list
Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "printer/sygus_print_callback.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
TypeNode intType = NodeManager::currentNM()->integerType();
collectSygusGrammarTypesFor(intType,types);
}
+ else if (range.isFunction())
+ {
+ std::vector<TypeNode> atypes = range.getArgTypes();
+ for (unsigned i = 0, ntypes = atypes.size(); i < ntypes; i++)
+ {
+ collectSygusGrammarTypesFor(atypes[i], types);
+ }
+ collectSygusGrammarTypesFor(range.getRangeType(), types);
+ }
}
}
}
Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
Type unres_t = unres_types[i];
//add variables
- for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j)
+ for (const Node& sv : sygus_vars)
{
- if( sygus_vars[j].getType()==types[i] ){
+ TypeNode svt = sv.getType();
+ if (svt == types[i])
+ {
std::stringstream ss;
- ss << sygus_vars[j];
- Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
- ops[i].push_back( sygus_vars[j].toExpr() );
+ ss << sv;
+ Trace("sygus-grammar-def")
+ << "...add for variable " << ss.str() << std::endl;
+ ops[i].push_back(sv.toExpr());
cnames[i].push_back(ss.str());
cargs[i].push_back(std::vector<Type>());
pcs[i].push_back(nullptr);
weights[i].push_back(-1);
}
+ else if (svt.isFunction() && svt.getRangeType() == types[i])
+ {
+ // We add an APPLY_UF for all function whose return type is this type
+ // whose argument types are the other sygus types we are constructing.
+ std::vector<TypeNode> argTypes = svt.getArgTypes();
+ std::vector<Type> stypes;
+ for (unsigned k = 0, ntypes = argTypes.size(); k < ntypes; k++)
+ {
+ unsigned index =
+ std::distance(types.begin(),
+ std::find(types.begin(), types.end(), argTypes[k]));
+ stypes.push_back(unres_types[index]);
+ }
+ std::stringstream ss;
+ ss << "apply_" << sv;
+ ops[i].push_back(sv.toExpr());
+ cnames[i].push_back(ss.str());
+ cargs[i].push_back(stypes);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
+ }
}
//add constants
std::vector< Node > consts;
pcs[i].push_back(nullptr);
weights[i].push_back(-1);
}
- }else{
+ }
+ else if (types[i].isSort() || types[i].isFunction())
+ {
+ // do nothing
+ }
+ else
+ {
Warning()
<< "Warning: No implementation for default Sygus grammar of type "
<< types[i] << std::endl;
// add predicates for types
for (unsigned i = 0, size = types.size(); i < size; ++i)
{
+ if (!types[i].isFirstClass())
+ {
+ continue;
+ }
Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
//add equality per type
Kind k = EQUAL;
}
}
+void TransitionInference::process(Node n, Node f)
+{
+ // set the function
+ d_func = f;
+ process(n);
+}
+
void TransitionInference::process(Node n)
{
NodeManager* nm = NodeManager::currentNM();
// if another part mentions UF or a free variable, then fail
bool lit_pol = n.getKind() != NOT;
Node lit = n.getKind() == NOT ? n[0] : n;
- if (lit.getKind() == APPLY_UF)
+ // is it an application of the function-to-synthesize? Yes if we haven't
+ // encountered a function or if it matches the existing d_func.
+ if (lit.getKind() == APPLY_UF
+ && (d_func.isNull() || lit.getOperator() == d_func))
{
Node op = lit.getOperator();
- if (d_func.isNull())
+ // initialize the variables
+ if (d_vars.empty())
{
d_func = op;
Trace("cegqi-inv-debug") << "Use " << op << " with args ";
}
Trace("cegqi-inv-debug") << std::endl;
}
- if (op != d_func)
- {
- Trace("cegqi-inv-debug")
- << "...failed, free function : " << n << std::endl;
- return false;
- }
- else if (topLevel)
+ Assert(!d_func.isNull());
+ if (topLevel)
{
if (terms.find(lit_pol) == terms.end())
{
* The node n should be the inner body of the negated synthesis conjecture,
* prior to generating the deep embedding. That is, given:
* forall f. ~forall x. P( f, x ),
- * this method expects n to be P( f, x ).
+ * this method expects n to be P( f, x ), and the argument f to be the
+ * function f above.
+ */
+ void process(Node n, Node f);
+ /**
+ * Same as above, without specifying f. This will try to infer a function f
+ * based on the body of n.
*/
void process(Node n);
/**
regress1/sygus/hd-01-d1-prog.sy
regress1/sygus/hd-19-d1-prog-dup-op.sy
regress1/sygus/hd-sdiv.sy
+ regress1/sygus/ho-sygus.sy
regress1/sygus/icfp_14.12-flip-args.sy
regress1/sygus/icfp_14.12.sy
regress1/sygus/icfp_14_12_diff_types.sy
regress1/sygus/trivial-stream.sy
regress1/sygus/twolets1.sy
regress1/sygus/twolets2-orig.sy
+ regress1/sygus/uf-abduct.smt2
regress1/sygus/unbdd_inv_gen_ex7.sy
regress1/sygus/unbdd_inv_gen_winf1.sy
regress1/sygus/univ_2-long-repeat.sy
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --uf-ho
+(set-logic ALL)
+(synth-fun f ((y (-> Int Int)) (z Int)) Int)
+(declare-var z (-> Int Int))
+(constraint (= (f z 0) (z 1)))
+(constraint (= (f z 1) (z 2)))
+(check-synth)
--- /dev/null
+; COMMAND-LINE: --produce-abducts --uf-ho
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic UFLIA)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(assert (and (<= 0 a) (< a 4)))
+(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))
projects / cvc5.git / commitdiff