help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
[[option]]
- name = "sygusDirectEval"
+ name = "sygusEvalUnfold"
category = "regular"
- long = "sygus-direct-eval"
+ long = "sygus-eval-unfold"
type = "bool"
default = "true"
read_only = true
- help = "direct unfolding of evaluation functions"
+ help = "do unfolding of sygus evaluation functions"
[[option]]
- name = "sygusUnfoldBool"
+ name = "sygusEvalUnfoldBool"
category = "regular"
- long = "sygus-unfold-bool"
+ long = "sygus-eval-unfold-bool"
type = "bool"
default = "true"
read_only = true
help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
[[option]]
- name = "sygusCRefEval"
+ name = "sygusRefEval"
category = "regular"
- long = "sygus-cref-eval"
+ long = "sygus-ref-eval"
type = "bool"
default = "true"
read_only = true
help = "direct evaluation of refinement lemmas for conflict analysis"
-[[option]]
- name = "sygusCRefEvalMinExp"
- category = "regular"
- long = "sygus-cref-eval-min-exp"
- type = "bool"
- default = "true"
- read_only = true
- help = "use min explain for direct evaluation of refinement lemmas for conflict analysis"
-
[[option]]
name = "sygusStream"
category = "regular"
addedLemma = true;
}else{
//this may happen if we eagerly unfold, simplify to true
- if( !options::sygusDirectEval() ){
- Trace("cegqi-warn") << " ...FAILED to add candidate!" << std::endl;
- }else{
- Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl;
- }
+ Trace("cegqi-engine-debug")
+ << " ...FAILED to add candidate!" << std::endl;
}
}
if( addedLemma ){
**/
#include "theory/quantifiers/sygus/cegis.h"
+#include "options/base_options.h"
#include "options/quantifiers_options.h"
+#include "printer/printer.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/theory_engine.h"
namespace quantifiers {
Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+
bool Cegis::initialize(Node n,
const std::vector<Node>& candidates,
std::vector<Node>& lemmas)
TypeNode bt = d_base_body.getType();
d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
}
+ return processInitialize(n, candidates, lemmas);
+}
+bool Cegis::processInitialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas)
+{
// initialize an enumerator for each candidate
for (unsigned i = 0; i < candidates.size(); i++)
{
{
NodeManager* nm = NodeManager::currentNM();
bool addedEvalLemmas = false;
- if (options::sygusCRefEval())
+ if (options::sygusRefEval())
{
- Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..."
+ Trace("cegqi-engine") << " *** Do refinement lemma evaluation..."
<< std::endl;
// see if any refinement lemma is refuted by evaluation
std::vector<Node> cre_lems;
{
if (d_qe->addLemma(lem))
{
- Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
- << std::endl;
+ Trace("cegqi-lemma")
+ << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
addedEvalLemmas = true;
}
}
add the lemmas below as well, in parallel. */
}
}
- if (!options::sygusDirectEval())
- {
- return addedEvalLemmas;
- }
- Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl;
- std::vector<Node> eager_terms, eager_vals, eager_exps;
- for (unsigned i = 0, size = candidates.size(); i < size; ++i)
+ if (options::sygusEvalUnfold())
{
- Trace("cegqi-debug") << " register " << candidates[i] << " -> "
- << candidate_values[i] << std::endl;
- d_tds->registerModelValue(candidates[i],
- candidate_values[i],
- eager_terms,
- eager_vals,
- eager_exps);
- }
- Trace("cegqi-debug") << "...produced " << eager_terms.size()
- << " eager evaluation lemmas.\n";
- for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
- {
- Node lem = nm->mkNode(
- OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
- if (d_qe->addLemma(lem))
+ Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl;
+ std::vector<Node> eager_terms, eager_vals, eager_exps;
+ for (unsigned i = 0, size = candidates.size(); i < size; ++i)
{
- Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
- << std::endl;
- addedEvalLemmas = true;
+ Trace("cegqi-debug") << " register " << candidates[i] << " -> "
+ << candidate_values[i] << std::endl;
+ d_tds->registerModelValue(candidates[i],
+ candidate_values[i],
+ eager_terms,
+ eager_vals,
+ eager_exps);
+ }
+ Trace("cegqi-debug") << "...produced " << eager_terms.size()
+ << " evaluation unfold lemmas.\n";
+ for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
+ {
+ Node lem = nm->mkNode(
+ OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
+ if (d_qe->addLemma(lem))
+ {
+ Trace("cegqi-lemma")
+ << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl;
+ addedEvalLemmas = true;
+ }
}
}
return addedEvalLemmas;
}
-/** construct candidate */
bool Cegis::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
std::vector<Node>& lems)
{
- if (addEvalLemmas(enums, enum_values))
+ if (Trace.isOn("cegis"))
{
- // it may be repairable
- SygusRepairConst* src = d_parent->getRepairConst();
- std::vector<Node> fail_cvs = enum_values;
- if (src->repairSolution(candidates, fail_cvs, candidate_values))
+ Trace("cegis") << " Enumerators :\n";
+ for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
- return true;
+ Trace("cegis") << " " << enums[i] << " -> ";
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, enum_values[i]);
+ Trace("cegis") << ss.str() << std::endl;
}
+ }
+ // evaluate on refinement lemmas
+ bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
+
+ // try to construct candidates
+ if (!processConstructCandidates(enums,
+ enum_values,
+ candidates,
+ candidate_values,
+ !addedEvalLemmas,
+ lems))
+ {
return false;
}
- candidate_values.insert(
- candidate_values.end(), enum_values.begin(), enum_values.end());
+
+ if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
+ {
+ // if we didn't add a lemma, trying sampling to add a refinement lemma
+ // that immediately refutes the candidate we just constructed
+ if (sampleAddRefinementLemma(enums, enum_values, lems))
+ {
+ // restart (should be guaranteed to add evaluation lemmas on this call)
+ return constructCandidates(
+ enums, enum_values, candidates, candidate_values, lems);
+ }
+ }
return true;
}
+bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& lems)
+{
+ if (satisfiedRl)
+ {
+ candidate_values.insert(
+ candidate_values.end(), enum_values.begin(), enum_values.end());
+ return true;
+ }
+ SygusRepairConst* src = d_parent->getRepairConst();
+ if (src != nullptr)
+ {
+ // it may be repairable
+ std::vector<Node> fail_cvs = enum_values;
+ Assert(candidates.size() == fail_cvs.size());
+ return src->repairSolution(candidates, fail_cvs, candidate_values);
+ }
+ return false;
+}
+
void Cegis::addRefinementLemma(Node lem)
{
d_refinement_lemmas.push_back(lem);
break;
}
}
- // if we didn't add a lemma, trying sampling to add one
- if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
- {
- if (sampleAddRefinementLemma(vs, ms, lems))
- {
- // restart (should be guaranteed to add evaluation lemmas
- getRefinementEvalLemmas(vs, ms, lems);
- }
- }
}
bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
const std::vector<Node>& vals,
std::vector<Node>& lems)
{
+ Trace("cegqi-engine") << " *** Do sample add refinement..." << std::endl;
if (Trace.isOn("cegis-sample"))
{
Trace("cegis-sample") << "Check sampling for candidate solution"
* formula P( CegConjecture::d_candidates, y ).
*/
Node d_base_body;
+ //----------------------------------cegis-implementation-specific
+ /** do cegis-implementation-specific intialization for this class */
+ virtual bool processInitialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas);
+ /** do cegis-implementation-specific construct candidate
+ *
+ * satisfiedRl is whether all refinement lemmas are satisfied under the
+ * substitution { enums -> enum_values }.
+ */
+ virtual bool processConstructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& lems);
+ //----------------------------------end cegis-implementation-specific
//-----------------------------------refinement lemmas
/** refinement lemmas */
}
CegisUnif::~CegisUnif() {}
-bool CegisUnif::initialize(Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+bool CegisUnif::processInitialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas)
{
Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
// list of strategy points for unification candidates
}
}
-bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
- const std::vector<Node>& enum_values,
- const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems)
+bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& lems)
{
- if (Trace.isOn("cegis-unif-enum"))
- {
- Trace("cegis-unif-enum") << " Evaluation heads :\n";
- for (unsigned i = 0, size = enums.size(); i < size; ++i)
- {
- Trace("cegis-unif-enum") << " " << enums[i] << " -> ";
- std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, enum_values[i]);
- Trace("cegis-unif-enum") << ss.str() << std::endl;
- }
- }
- // evaluate on refinement lemmas
- if (addEvalLemmas(enums, enum_values))
+ if (!satisfiedRl)
{
+ // if we didn't satisfy the specification, there is no way to repair
return false;
}
// the unification enumerators (return values, conditions) and their model
{
for (unsigned index = 0; index < 2; index++)
{
- Trace("cegis-unif-enum")
- << " " << (index == 0 ? "Return values" : "Conditions") << " for "
- << e << ":\n";
+ Trace("cegis") << " " << (index == 0 ? "Return values" : "Conditions")
+ << " for " << e << ":\n";
// get the current unification enumerators
d_u_enum_manager.getEnumeratorsForStrategyPt(
e, unif_enums[index][e], index);
for (const Node& eu : unif_enums[index][e])
{
Node m_eu = d_parent->getModelValue(eu);
- if (Trace.isOn("cegis-unif-enum"))
+ if (Trace.isOn("cegis"))
{
- Trace("cegis-unif-enum") << " " << eu << " -> ";
+ Trace("cegis") << " " << eu << " -> ";
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())
->toStreamSygus(ss, m_eu);
- Trace("cegis-unif-enum") << ss.str() << std::endl;
+ Trace("cegis") << ss.str() << std::endl;
}
unif_values[index][e].push_back(m_eu);
}
public:
CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
~CegisUnif();
- /** initialize this class */
- bool initialize(Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas) override;
/** Retrieves enumerators for constructing solutions
*
* Non-unification candidates have themselves as enumerators, while for
*/
void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& enums) override;
- /** Tries to build new candidate solutions with new enumerated expressions
- *
- * This function relies on a data-driven unification-based approach for
- * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
- * more details.
- *
- * Calls to this function are such that terms is the list of active
- * enumerators (returned by getTermList), and term_values are their current
- * model values. This function registers { terms -> terms_values } in
- * the database of values that have been enumerated, which are in turn used
- * for constructing candidate solutions when possible.
- *
- * This function also excludes models where (terms = terms_values) by adding
- * blocking clauses to lems. For example, for grammar:
- * A -> A+A | x | 1 | 0
- * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
- * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
- * to lems, where G is active guard of the enumerator d (see
- * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
- * indicates that d should not be given the model value +( x, 1 ) anymore,
- * since { d -> +( x, 1 ) } has now been added to the database of this class.
- */
- bool constructCandidates(const std::vector<Node>& enums,
- const std::vector<Node>& enum_values,
- const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems) override;
/** Communicates refinement lemma to unification utility and external modules
*
Node getNextDecisionRequest(unsigned& priority) override;
private:
+ /** do cegis-implementation-specific intialization for this class */
+ bool processInitialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas) override;
+ /** Tries to build new candidate solutions with new enumerated expressions
+ *
+ * This function relies on a data-driven unification-based approach for
+ * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
+ * more details.
+ *
+ * Calls to this function are such that terms is the list of active
+ * enumerators (returned by getTermList), and term_values are their current
+ * model values. This function registers { terms -> terms_values } in
+ * the database of values that have been enumerated, which are in turn used
+ * for constructing candidate solutions when possible.
+ *
+ * This function also excludes models where (terms = terms_values) by adding
+ * blocking clauses to lems. For example, for grammar:
+ * A -> A+A | x | 1 | 0
+ * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+ * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+ * to lems, where G is active guard of the enumerator d (see
+ * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+ * indicates that d should not be given the model value +( x, 1 ) anymore,
+ * since { d -> +( x, 1 ) } has now been added to the database of this class.
+ */
+ bool processConstructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& lems) override;
/**
* Sygus unif utility. This class implements the core algorithm (e.g. decision
* tree learning) that this module relies upon.
void TermDbSygus::registerEvalTerm( Node n ) {
- if( options::sygusDirectEval() ){
+ if (options::sygusEvalUnfold())
+ {
if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
TypeNode tn = n[0].getType();
if( tn.isDatatype() ){
Node expn;
// unfold?
bool do_unfold = false;
- if( options::sygusUnfoldBool() ){
+ if (options::sygusEvalUnfoldBool())
+ {
if( bTerm.getKind()==ITE || bTerm.getType().isBoolean() ){
do_unfold = true;
}
regress1/sygus/dt-test-ns.sy \
regress1/sygus/dup-op.sy \
regress1/sygus/fg_polynomial3.sy \
+ regress1/sygus/find_sc_bvult_bvnot.sy \
regress1/sygus/hd-01-d1-prog.sy \
regress1/sygus/hd-19-d1-prog-dup-op.sy \
regress1/sygus/hd-sdiv.sy \
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --cegis-sample=use
(set-logic LIA)
(synth-fun f ((x1 Int) (x2 Int)) Int
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --cegis-sample=trust
+(set-logic BV)
+
+; we test --cegis-sample=trust since we can exhaustively sample BV4
+
+(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool
+ ((Start Bool (
+ true
+ false
+ (not Start)
+ (and Start Start)
+ (or Start Start)
+; (=> Start Start)
+ (= StartBv StartBv)
+ (bvult StartBv StartBv)
+ (bvslt StartBv StartBv)
+ (bvuge StartBv StartBv)
+ (bvsge StartBv StartBv)
+ ))
+ (StartBv (BitVec 4) (
+ s
+ t
+ #x0
+ #x8 ; min_val
+ #x7 ; max_val
+ (bvneg StartBv)
+ (bvnot StartBv)
+ (bvadd StartBv StartBv)
+ (bvsub StartBv StartBv)
+ (bvand StartBv StartBv)
+ (bvlshr StartBv StartBv)
+ (bvor StartBv StartBv)
+ (bvshl StartBv StartBv)
+ ))
+))
+
+(declare-var s (BitVec 4))
+(declare-var t (BitVec 4))
+(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+ (ite (= b #x0) #xF (bvudiv a b))
+)
+(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+ (ite (= b #x0) a (bvurem a b))
+)
+(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool
+(bvult (bvnot x) t)
+)
+(constraint
+ (=
+ (or
+ (case #x0 s t)
+ (case #x1 s t)
+ (case #x2 s t)
+ (case #x3 s t)
+ (case #x4 s t)
+ (case #x5 s t)
+ (case #x6 s t)
+ (case #x7 s t)
+ (case #x8 s t)
+ (case #x9 s t)
+ (case #xA s t)
+ (case #xB s t)
+ (case #xC s t)
+ (case #xD s t)
+ (case #xE s t)
+ (case #xF s t)
+ )
+ (SC s t)
+ )
+)
+
+(check-synth)
projects / cvc5.git / commitdiff