// otherwise expand it
bool doExpand = k == kind::APPLY;
if( !doExpand ){
- if( options::macrosQuant() ){
+ // options that assign substitutions to APPLY_UF
+ if (options::macrosQuant() || options::sygusInference())
+ {
//expand if we have inferred an operator corresponds to a defined function
doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
}
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- 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())
+ if (options::globalNegate())
{
// global negation of the formula
quantifiers::GlobalNegate gn;
d_smt.d_fmfRecFunctionsDefined->push_back( f );
}
}
+ 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;
+ }
+ }
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
}
}
}
+void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
+{
+ SmtScope smts(this);
+ map<Node, Node> sol_mapn;
+ Assert(d_theoryEngine != nullptr);
+ d_theoryEngine->getSynthSolutions(sol_mapn);
+ for (std::pair<const Node, Node>& s : sol_mapn)
+ {
+ sol_map[s.first.toExpr()] = s.second.toExpr();
+ }
+}
+
Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
{
SmtScope smts(this);
*/
void printSynthSolution( std::ostream& out );
+ /**
+ * Get synth solution
+ *
+ * This function adds entries to sol_map that map functions-to-synthesize with
+ * their solutions, for all active conjectures. This should be called
+ * immediately after the solver answers unsat for sygus input.
+ *
+ * Specifically, given a sygus conjecture of the form
+ * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
+ * where x1...xn are second order bound variables, we map each xi to
+ * lambda term in sol_map such that
+ * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
+ * is a valid formula.
+ */
+ void getSynthSolutions(std::map<Expr, Expr>& sol_map);
+
/**
* Do quantifier elimination.
*
rrChecker.assertFormula(crr.toExpr());
Result r = rrChecker.checkSat();
Trace("rr-check") << "...result : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat())
+ if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
success = false;
repcChecker.assertFormula(fo_body.toExpr());
Result r = repcChecker.checkSat();
Trace("sygus-repair-const") << "...got : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat()
+ if (r.asSatisfiabilityResult().isSat() != Result::UNSAT
&& !r.asSatisfiabilityResult().isUnknown())
{
std::vector<Node> sk_sygus_m;
**/
#include "theory/quantifiers/sygus_inference.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
}
if (pas.getKind() == FORALL)
{
+ // it must be a standard quantifier
+ QAttributes qa;
+ QuantAttributes::computeQuantAttributes(pas, qa);
+ if (!qa.isStandard())
+ {
+ Trace("sygus-infer")
+ << "...fail: non-standard top-level quantifier." << std::endl;
+ return false;
+ }
// infer prefix
for (const Node& v : pas[0])
{
// for each free function symbol, make a bound variable of the same type
Trace("sygus-infer") << "Do free function substitution..." << std::endl;
std::vector<Node> ff_vars;
+ std::map<Node, Node> ff_var_to_ff;
for (const Node& ff : free_functions)
{
Node ffv = nm->mkBoundVar(ff.getType());
ff_vars.push_back(ffv);
+ Trace("sygus-infer") << " synth-fun: " << ff << " as " << ffv << std::endl;
+ ff_var_to_ff[ffv] = ff;
}
// substitute free functions -> variables
body = body.substitute(free_functions.begin(),
Trace("sygus-infer") << "*** Return sygus inference : " << 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++)
+ // make a separate smt call
+ SmtEngine* master_smte = smt::currentSmtEngine();
+ SmtEngine rrSygus(nm->toExprManager());
+ rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ rrSygus.assertFormula(body.toExpr());
+ Trace("sygus-infer") << "*** Check sat..." << std::endl;
+ Result r = rrSygus.checkSat();
+ Trace("sygus-infer") << "...result : " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+ {
+ // failed, conjecture was infeasible
+ return false;
+ }
+ // get the synthesis solutions
+ std::map<Expr, Expr> synth_sols;
+ rrSygus.getSynthSolutions(synth_sols);
+
+ std::vector<Node> final_ff;
+ std::vector<Node> final_ff_sol;
+ for (std::map<Expr, Expr>::iterator it = synth_sols.begin();
+ it != synth_sols.end();
+ ++it)
{
- if (i == 0)
+ Node lambda = Node::fromExpr(it->second);
+ Trace("sygus-infer") << " synth sol : " << it->first << " -> "
+ << it->second << std::endl;
+ Node ffv = Node::fromExpr(it->first);
+ std::map<Node, Node>::iterator itffv = ff_var_to_ff.find(ffv);
+ // all synthesis solutions should correspond to a variable we introduced
+ Assert(itffv != ff_var_to_ff.end());
+ if (itffv != ff_var_to_ff.end())
{
- assertions[i] = body;
+ Node ff = itffv->second;
+ std::vector<Expr> args;
+ for (const Node& v : lambda[0])
+ {
+ args.push_back(v.toExpr());
+ }
+ Trace("sygus-infer") << "Define " << ff << " as " << it->second
+ << std::endl;
+ final_ff.push_back(ff);
+ final_ff_sol.push_back(it->second);
+ master_smte->defineFunction(ff.toExpr(), args, it->second[1]);
}
- else
+ }
+
+ // apply substitution to everything, should result in SAT
+ for (unsigned i = 0, size = assertions.size(); i < size; i++)
+ {
+ Node prev = assertions[i];
+ Node curr = assertions[i].substitute(final_ff.begin(),
+ final_ff.end(),
+ final_ff_sol.begin(),
+ final_ff_sol.end());
+ if (curr != prev)
{
- assertions[i] = truen;
+ curr = Rewriter::rewrite(curr);
+ Trace("sygus-infer-debug")
+ << "...rewrote " << prev << " to " << curr << std::endl;
+ assertions[i] = curr;
}
}
return true;
/** SygusInference
*
- * A preprocessing utility to turn a set of (quantified) assertions into a
- * single SyGuS conjecture.
+ * A preprocessing utility that turns a set of (quantified) assertions into a
+ * single SyGuS conjecture. If this is possible, we solve for this single Sygus
+ * conjecture using a separate copy of the SMT engine. If sygus successfully
+ * solves the conjecture, we plug the synthesis solutions back into the original
+ * problem, thus obtaining a set of model substitutions under which the
+ * assertions should simplify to true.
*/
class SygusInference
{
~SygusInference() {}
/** simplify assertions
*
- * Either replaces assertions with the negation of an equivalent SyGuS
- * conjecture and returns true, or otherwise returns false.
+ * Either replaces all uninterpreted functions in assertions by their
+ * interpretation in the solution found by a separate call to an SMT engine
+ * and returns true, or leaves the assertions unmodified and returns false.
+ *
+ * We fail if either a sygus conjecture that corresponds to assertions cannot
+ * be inferred, or the sygus conjecture we infer is infeasible.
*/
bool simplify(std::vector<Node>& assertions);
};
regress1/quantifiers/extract-nproc.smt2 \
regress1/quantifiers/florian-case-ax.smt2 \
regress1/quantifiers/gauss_init_0030.fof.smt2 \
+ regress1/quantifiers/horn-simple.smt2 \
regress1/quantifiers/inst-max-level-segf.smt2 \
regress1/quantifiers/inst-prop-simp.smt2 \
regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \
--- /dev/null
+; COMMAND-LINE: --sygus-unif --sygus-infer
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun I (Int) Bool)
+
+(assert (forall ((x Int)) (=> (= x 0) (I x))))
+
+(assert (forall ((x Int)) (=> (and (I x) (< x 1)) (I (+ x 1)))))
+
+(assert (forall ((x Int)) (=> (I x) (<= x 10))))
+
+(check-sat)
projects / cvc5.git / commitdiff