This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.
This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.
default = "1000"
help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
+[[option]]
+ name = "sygusVerifyInstMaxRounds"
+ category = "regular"
+ long = "sygus-verify-inst-max-rounds=N"
+ type = "int"
+ default = "3"
+ help = "maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 3)"
+
# Internal uses of sygus
[[option]]
std::unique_ptr<SmtEngine> optChecker;
// initializeSubSolver will copy the options and theories enabled
// from the current solver to optChecker and adds timeout
- theory::initializeSubsolver(optChecker, needsTimeout, timeout);
+ theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
// we need to be in incremental mode for multiple objectives since we need to
// push pop we need to produce models to inrement on our objective
optChecker->setOption("incremental", "true");
Assert (!query.isNull());
if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
{
- initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
+ initializeSubsolver(
+ checker, nullptr, true, options::sygusExprMinerCheckTimeout());
}
else
{
Node f = h.hasOperator() ? h.getOperator() : h;
Assert(d_funDefMap.find(f) == d_funDefMap.end())
<< "FunDefEvaluator::assertDefinition: function already defined";
+ d_funDefs.push_back(q);
FunDefInfo& fdi = d_funDefMap[f];
+ fdi.d_quant = q;
fdi.d_body = QuantAttributes::getFunDefBody(q);
Assert(!fdi.d_body.isNull());
fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
+const std::vector<Node>& FunDefEvaluator::getDefinitions() const
+{
+ return d_funDefs;
+}
+Node FunDefEvaluator::getDefinitionFor(Node f) const
+{
+ std::map<Node, FunDefInfo>::const_iterator it = d_funDefMap.find(f);
+ if (it != d_funDefMap.end())
+ {
+ return it->second.d_quant;
+ }
+ return Node::null();
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
*/
bool hasDefinitions() const;
+ /** Get definitions */
+ const std::vector<Node>& getDefinitions() const;
+ /** Get definition for function symbol f, if it is cached by this class */
+ Node getDefinitionFor(Node f) const;
+
private:
/** information cached per function definition */
class FunDefInfo
{
public:
+ /** the quantified formula */
+ Node d_quant;
/** the body */
Node d_body;
/** the formal argument list */
};
/** maps functions to the above information */
std::map<Node, FunDefInfo> d_funDefMap;
+ /** list of all definitions */
+ std::vector<Node> d_funDefs;
/** evaluator utility */
Evaluator d_eval;
};
// make the satisfiability query
std::unique_ptr<SmtEngine> repcChecker;
// initialize the subsolver using the standard method
- initializeSubsolver(repcChecker,
- Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
- options::sygusRepairConstTimeout());
+ initializeSubsolver(
+ repcChecker,
+ nullptr,
+ Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
+ options::sygusRepairConstTimeout());
// renable options disabled by sygus
repcChecker->setOption("miniscope-quant", "true");
repcChecker->setOption("miniscope-quant-fv", "true");
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "base/configuration.h"
+#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
d_modules.push_back(d_sygus_ccore.get());
}
d_modules.push_back(d_ceg_cegis.get());
+ // determine the options to use for the verification subsolvers we spawn
+ // we start with the options of the current SmtEngine
+ SmtEngine* smtCurr = smt::currentSmtEngine();
+ d_subOptions.copyValues(smtCurr->getOptions());
+ // limit the number of instantiation rounds on subcalls
+ d_subOptions.quantifiers.instMaxRounds =
+ d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
+ // Disable sygus on the subsolver. This is particularly important since it
+ // ensures that recursive function definitions have the standard ownership
+ // instead of being claimed by sygus in the subsolver.
+ d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
+ d_subOptions.quantifiers.sygus = false;
}
SynthConjecture::~SynthConjecture() {}
if (!query.isConst() || query.getConst<bool>())
{
+ // add recursive function definitions
+ FunDefEvaluator* feval = d_tds->getFunDefEvaluator();
+ const std::vector<Node>& fdefs = feval->getDefinitions();
+ if (!fdefs.empty())
+ {
+ // Get the relevant definitions based on the symbols in the query.
+ // Notice in some cases, this may have the effect of making the subcall
+ // involve no recursive function definitions at all, in which case the
+ // subcall to verification may be decidable, in which case the call
+ // below is guaranteed to generate a new counterexample point.
+ std::unordered_set<Node> syms;
+ expr::getSymbols(query, syms);
+ std::vector<Node> qconj;
+ qconj.push_back(query);
+ for (const Node& f : syms)
+ {
+ Node q = feval->getDefinitionFor(f);
+ if (!q.isNull())
+ {
+ qconj.push_back(q);
+ }
+ }
+ query = nm->mkAnd(qconj);
+ Trace("cegqi-debug") << "query is " << query << std::endl;
+ }
Trace("sygus-engine") << " *** Verify with subcall..." << std::endl;
- Result r = checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs);
+ Result r =
+ checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs, &d_subOptions);
Trace("sygus-engine") << " ...got " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
* rewrite rules.
*/
std::map<Node, ExpressionMinerManager> d_exprm;
+ /** The options for subsolver calls */
+ Options d_subOptions;
};
} // namespace quantifiers
// take ownership of quantified formulas with sygus attribute, and function
// definitions when options::sygusRecFun is true.
QuantAttributes& qa = d_qreg.getQuantAttributes();
- if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
+ if (qa.isSygus(q) || (qa.isFunDef(q) && options::sygusRecFun()))
{
d_qreg.setOwner(q, this, 2);
}
}
void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Options* opts,
bool needsTimeout,
unsigned long timeout)
{
NodeManager* nm = NodeManager::currentNM();
SmtEngine* smtCurr = smt::currentSmtEngine();
- // must copy the options
- smte.reset(new SmtEngine(nm, &smtCurr->getOptions()));
+ if (opts == nullptr)
+ {
+ // must copy the options
+ opts = &smtCurr->getOptions();
+ }
+ smte.reset(new SmtEngine(nm, opts));
smte->setIsInternalSubsolver();
smte->setLogic(smtCurr->getLogicInfo());
// set the options
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
Node query,
+ Options* opts,
bool needsTimeout,
unsigned long timeout)
{
{
return r;
}
- initializeSubsolver(smte, needsTimeout, timeout);
+ initializeSubsolver(smte, opts, needsTimeout, timeout);
smte->assertFormula(query);
return smte->checkSat();
}
-Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout)
+Result checkWithSubsolver(Node query,
+ Options* opts,
+ bool needsTimeout,
+ unsigned long timeout)
{
std::vector<Node> vars;
std::vector<Node> modelVals;
- return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout);
+ return checkWithSubsolver(
+ query, vars, modelVals, opts, needsTimeout, timeout);
}
Result checkWithSubsolver(Node query,
const std::vector<Node>& vars,
std::vector<Node>& modelVals,
+ Options* opts,
bool needsTimeout,
unsigned long timeout)
{
return r;
}
std::unique_ptr<SmtEngine> smte;
- initializeSubsolver(smte, needsTimeout, timeout);
+ initializeSubsolver(smte, opts, needsTimeout, timeout);
smte->assertFormula(query);
r = smte->checkSat();
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
* if the current SMT engine has declared a separation logic heap.
*
* @param smte The smt engine pointer to initialize
+ * @param opts The options for the subsolver. If nullptr, then we copy the
+ * options from the current SmtEngine in scope.
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Options* opts = nullptr,
bool needsTimeout = false,
unsigned long timeout = 0);
*/
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
Node query,
+ Options* opts = nullptr,
bool needsTimeout = false,
unsigned long timeout = 0);
* concerned with the state of the SMT engine after the check.
*
* @param query The query to check
+ * @param opts The options for the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
+ Options* opts = nullptr,
bool needsTimeout = false,
unsigned long timeout = 0);
* @param query The query to check
* @param vars The variables we are interesting in getting a model for.
* @param modelVals A vector storing the model values of variables in vars.
+ * @param opts The options for the subsolver
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
Result checkWithSubsolver(Node query,
const std::vector<Node>& vars,
std::vector<Node>& modelVals,
+ Options* opts = nullptr,
bool needsTimeout = false,
unsigned long timeout = 0);
regress2/sygus/process-arg-invariance.sy
regress2/sygus/real-grammar-neg.sy
regress2/sygus/sets-fun-test.sy
+ regress2/sygus/sumn_recur_synth.sy
regress2/sygus/strings-no-syntax-len.sy
regress2/sygus/three.sy
regress2/typed_v1l50016-simp.cvc
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic UFLIA)
+
+(declare-var x Int)
+(declare-var x! Int)
+(declare-var y Int)
+(declare-var y! Int)
+
+(define-fun-rec sum_n ((x Int)) Int
+ (ite (>= x 1)
+ (+ x (sum_n (- x 1)))
+ 0))
+
+(synth-fun inv_fun ((x Int) (y Int)) Bool
+ ((C Bool) (B Bool) (E Int))
+ ((C Bool ((and (>= y 1) B)))
+ (B Bool ((= (sum_n E) E) (>= E E)))
+ (E Int (0 1 x y (+ E E))))
+)
+
+(define-fun pre_fun ((x Int) (y Int)) Bool
+ (and (= x 0) (= y 1)))
+
+(define-fun trans_fun ((x Int) (y Int) (x! Int) (y! Int)) Bool
+ (and (<= y 2) (= x! (+ x y)) (= y! (+ y 1))))
+
+(define-fun post_fun ((x Int) (y Int)) Bool
+ (= x (sum_n (- y 1)))
+)
+
+(constraint (=> (pre_fun x y) (inv_fun x y)))
+(constraint (=> (and (inv_fun x y) (trans_fun x y x! y!)) (inv_fun x! y!)))
+(constraint (=> (inv_fun x y) (post_fun x y)))
+
+
+(check-synth)
projects / cvc5.git / commitdiff