* universally quantified in the constraints.
*/
std::vector<Node> d_sygusVars;
- /** types of sygus primed variables (for debugging) */
- std::vector<Type> d_sygusPrimedVarTypes;
/** sygus constraints */
std::vector<Node> d_sygusConstraints;
/** functions-to-synthesize */
void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
{
-#ifdef CVC4_ASSERTIONS
- d_private->d_sygusPrimedVarTypes.push_back(type);
-#endif
+ // do nothing (the command is spurious)
Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
// don't need to set that the conjecture is stale
}
ss << vars.back() << "'";
primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn));
d_private->d_sygusVars.push_back(primed_vars.back());
-#ifdef CVC4_ASSERTIONS
- bool find_new_declared_var = false;
- for (const Type& t : d_private->d_sygusPrimedVarTypes)
- {
- if (t == ti)
- {
- d_private->d_sygusPrimedVarTypes.erase(
- std::find(d_private->d_sygusPrimedVarTypes.begin(),
- d_private->d_sygusPrimedVarTypes.end(),
- t));
- find_new_declared_var = true;
- break;
- }
- }
- if (!find_new_declared_var)
- {
- Warning()
- << "warning: declared primed variables do not match invariant's "
- "type\n";
- }
-#endif
}
// make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
return addedEvalLemmas;
}
+Node Cegis::getRefinementLemmaFormula()
+{
+ std::vector<Node> conj;
+ conj.insert(
+ conj.end(), d_refinement_lemmas.begin(), d_refinement_lemmas.end());
+ // get the propagated values
+ for (unsigned i = 0, nprops = d_rl_eval_hds.size(); i < nprops; i++)
+ {
+ conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i]));
+ }
+ // make the formula
+ NodeManager* nm = NodeManager::currentNM();
+ Node ret;
+ if (conj.empty())
+ {
+ ret = nm->mkConst(true);
+ }
+ else
+ {
+ ret = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
+ }
+ return ret;
+}
+
bool Cegis::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
{
std::vector<Node> fail_cvs = enum_values;
Assert(candidates.size() == fail_cvs.size());
+ // try to solve entire problem?
if (src->repairSolution(candidates, fail_cvs, candidate_values))
{
return true;
}
- // repair solution didn't work, exclude this solution
+ Node rl = getRefinementLemmaFormula();
+ // try to solve for the refinement lemmas only
+ bool ret =
+ src->repairSolution(rl, candidates, fail_cvs, candidate_values);
+ // Even if ret is true, we will exclude the skeleton as well; this means
+ // that we have one chance to repair each skeleton. It is possible however
+ // that we might want to repair the same skeleton multiple times.
std::vector<Node> exp;
for (unsigned i = 0, size = enums.size(); i < size; i++)
{
// must guard it
expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate());
lems.push_back(expn);
- return false;
+ return ret;
}
}
bool addEvalLemmas(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values,
std::vector<Node>& lems);
+ /** Get the node corresponding to the conjunction of all refinement lemmas. */
+ Node getRefinementLemmaFormula();
//-----------------------------------end refinement lemmas
/** Get refinement evaluation lemmas
const std::vector<Node>& candidate_values,
std::vector<Node>& repair_cv,
bool useConstantsAsHoles)
+{
+ return repairSolution(d_base_inst,
+ candidates,
+ candidate_values,
+ repair_cv,
+ useConstantsAsHoles);
+}
+
+bool SygusRepairConst::repairSolution(Node sygusBody,
+ const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& repair_cv,
+ bool useConstantsAsHoles)
{
Assert(candidates.size() == candidate_values.size());
NodeManager* nm = NodeManager::currentNM();
Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
- Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars);
+ Node fo_body =
+ getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
{
- fo_body = fitToLogic(logic,
+ fo_body = fitToLogic(sygusBody,
+ logic,
fo_body,
candidates,
candidate_skeletons,
return visited[n];
}
-Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
+Node SygusRepairConst::getFoQuery(Node body,
+ const std::vector<Node>& candidates,
const std::vector<Node>& candidate_skeletons,
const std::vector<Node>& sk_vars)
{
NodeManager* nm = NodeManager::currentNM();
- Node body = d_base_inst;
Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
body = body.substitute(candidates.begin(),
candidates.end(),
return fo_body;
}
-Node SygusRepairConst::fitToLogic(LogicInfo& logic,
+Node SygusRepairConst::fitToLogic(Node body,
+ LogicInfo& logic,
Node n,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_skeletons,
Assert(it != sk_vars.end());
sk_vars.erase(it);
// reconstruct the query
- n = getFoQuery(candidates, candidate_skeletons, sk_vars);
+ n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
// reset the exclusion variable
exc_var = Node::null();
}
~SygusRepairConst() {}
/** initialize
*
- * Initialize this class with the base instantiation of the sygus conjecture
- * (see CegConjecture::d_base_inst) and its candidate variables (see
- * CegConjecture::d_candidates).
+ * Initialize this class with the base instantiation (body) of the sygus
+ * conjecture (see SynthConjecture::d_base_inst) and its candidate variables
+ * (see SynthConjecture::d_candidates).
*/
void initialize(Node base_inst, const std::vector<Node>& candidates);
/** repair solution
* candidate_values to be repairable. In addition, if the flag
* useConstantsAsHoles is true, we consider all constants whose (sygus) type
* admit alls constants to be repairable.
+ * The repaired solution has the property that it satisfies the synthesis
+ * conjecture whose body is given by sygusBody.
+ */
+ bool repairSolution(Node sygusBody,
+ const std::vector<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& repair_cv,
+ bool useConstantsAsHoles = false);
+ /**
+ * Same as above, but where sygusBody is the body (base_inst) provided to the
+ * call to initialize of this class.
*/
bool repairSolution(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values,
/** get first-order query
*
* This function returns a formula that is equivalent to the negation of the
- * synthesis conjecture, where candidates are replaced by candidate_skeletons,
+ * synthesis conjecture whose body is given in the first argument, where
+ * candidates are replaced by candidate_skeletons,
* whose free variables are in the set sk_vars. The returned formula
* is a first-order (quantified) formula in the background logic, without UF,
* of the form [***] above.
*/
- Node getFoQuery(const std::vector<Node>& candidates,
+ Node getFoQuery(Node body,
+ const std::vector<Node>& candidates,
const std::vector<Node>& candidate_skeletons,
const std::vector<Node>& sk_vars);
/** fit to logic
* not enabled, we must undo some of the variables we introduced when
* inferring candidate skeletons.
*
+ * body is the (sygus) form of the original synthesis conjecture we are
+ * considering in this call.
+ *
* This function may remove variables from sk_vars and the map
* sk_vars_to_subs. The skeletons candidate_skeletons are obtained by
* getSkeleton(...) on the resulting vectors. If this function returns a
* It uses the function below to choose which variables to remove from
* sk_vars.
*/
- Node fitToLogic(LogicInfo& logic,
+ Node fitToLogic(Node body,
+ LogicInfo& logic,
Node n,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_skeletons,
regress1/sygus/cegisunif-depth1.sy
regress1/sygus/cggmp.sy
regress1/sygus/clock-inc-tuple.sy
+ regress1/sygus/coeff-solve-inv.sy
regress1/sygus/commutative-stream.sy
regress1/sygus/commutative.sy
regress1/sygus/concat_extract_example.sy
regress1/sygus/qe.sy
regress1/sygus/qf_abv.smt2
regress1/sygus/real-grammar.sy
+ regress1/sygus/repair-const-rl.sy
regress1/sygus/repair-const-unk.sy
regress1/sygus/simple-regexp.sy
regress1/sygus/stopwatch-bt.sy
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2
+(set-logic LIA)
+
+(synth-inv inv-f ((x Int) (y Int)) )
+
+
+(define-fun pre-f ((x Int) (y Int)) Bool
+ (and
+ (= x 0)
+ (= y 100)
+ )
+)
+
+(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool
+ (and
+ (< x 100)
+ (= x! (+ x 1))
+ (= y! (+ y 1))
+ )
+)
+
+(define-fun post-f ((x Int) (y Int)) Bool
+ (=> (>= x 100) (>= y 200))
+)
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-repair-const --lang=sygus2
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+ ((Start Int) (CInt Int))
+ (
+ (Start Int ((+ (* CInt x) (* CInt y) CInt)))
+ (CInt Int ((Constant Int)))
+ )
+)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f 0 0) 100))
+
+(constraint (= (f 1 1) 110))
+
+(constraint (= (f 2 1) 117))
+
+(constraint (>= (- (* 3 (f x y)) (f (* 2 x) (+ y 1))) (+ (* 7 x) (* 6 y))))
+
+(check-synth)
projects / cvc5.git / commitdiff