d_candidate = candidates[0];
Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
<< "...\n";
- d_sygus_unif.initialize(d_qe, d_candidate, d_enums, lemmas);
+ d_sygus_unif.initialize(d_qe, candidates, d_enums, lemmas);
Assert(!d_enums.empty());
Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for "
<< d_candidate << "...\n";
}
/* build candidate solution */
Assert(candidates.size() == 1);
- Node vc = d_sygus_unif.constructSolution();
- Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
- if (vc.isNull())
+ if (d_sygus_unif.constructSolution(candidate_values))
{
- return false;
+ Node vc = candidate_values[0];
+ Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
+ return true;
}
- candidate_values.push_back(vc);
- return true;
+ return false;
}
Node CegisUnif::purifyLemma(Node n,
}
}
}
-
- //register candidates
- if( options::sygusUnifCondSol() ){
- if( candidates.size()==1 ){// conditional solutions for multiple function conjectures TODO?
- // collect a pool of types over which we will enumerate terms
- Node c = candidates[0];
- // specification must have at least one example, and must be in PBE form
- if (!d_examples[c].empty()
- && d_examples_out_invalid.find(c) == d_examples_out_invalid.end())
- {
- Assert( d_examples.find( c )!=d_examples.end() );
- Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
- << std::endl;
- d_sygus_unif[c].initialize(d_qe, c, d_candidate_to_enum[c], lemmas);
- Assert(!d_candidate_to_enum[c].empty());
- Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
- << " enumerators for " << c << "..." << std::endl;
- // initialize the enumerators
- for (unsigned i = 0, size = d_candidate_to_enum[c].size(); i < size;
- i++)
- {
- Node e = d_candidate_to_enum[c][i];
- d_tds->registerEnumerator(e, c, d_parent, true);
- Node g = d_tds->getActiveGuardForEnumerator(e);
- d_enum_to_active_guard[e] = g;
- d_enum_to_candidate[e] = c;
- }
- Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
- << " example points for " << c << "..." << std::endl;
- // initialize the examples
- for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
- {
- d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
- }
- d_is_pbe = true;
- }
+
+ if (!options::sygusUnifCondSol())
+ {
+ // we are not doing unification
+ return false;
+ }
+
+ // check if all candidates are valid examples
+ d_is_pbe = true;
+ for (const Node& c : candidates)
+ {
+ if (d_examples[c].empty()
+ || d_examples_out_invalid.find(c) != d_examples_out_invalid.end())
+ {
+ d_is_pbe = false;
+ return false;
+ }
+ }
+ for (const Node& c : candidates)
+ {
+ Assert(d_examples.find(c) != d_examples.end());
+ Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
+ << std::endl;
+ std::vector<Node> singleton_c;
+ singleton_c.push_back(c);
+ d_sygus_unif[c].initialize(
+ d_qe, singleton_c, d_candidate_to_enum[c], lemmas);
+ Assert(!d_candidate_to_enum[c].empty());
+ Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
+ << " enumerators for " << c << "..." << std::endl;
+ // initialize the enumerators
+ for (const Node& e : d_candidate_to_enum[c])
+ {
+ d_tds->registerEnumerator(e, c, d_parent, true);
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ d_enum_to_active_guard[e] = g;
+ d_enum_to_candidate[e] = c;
+ }
+ Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
+ << " example points for " << c << "..." << std::endl;
+ // initialize the examples
+ for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
+ {
+ d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
}
}
- return d_is_pbe;
+ return true;
}
Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
for( unsigned i=0; i<candidates.size(); i++ ){
Node c = candidates[i];
//build decision tree for candidate
- Node vc = d_sygus_unif[c].constructSolution();
- if( vc.isNull() ){
+ std::vector<Node> sol;
+ if (d_sygus_unif[c].constructSolution(sol))
+ {
+ Assert(sol.size() == 1);
+ candidate_values.push_back(sol[0]);
+ }
+ else
+ {
return false;
- }else{
- candidate_values.push_back( vc );
}
}
return true;
SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
SygusUnif::~SygusUnif() {}
-
void SygusUnif::initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas)
{
- Assert(d_candidate.isNull());
- d_candidate = f;
+ Assert(d_candidates.empty());
d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
- // initialize the strategy
- d_strategy.initialize(qe, f, enums, lemmas);
+ for (const Node& f : funs)
+ {
+ d_candidates.push_back(f);
+ // initialize the strategy
+ d_strategy[f].initialize(qe, f, enums, lemmas);
+ }
}
-Node SygusUnif::constructSolution()
+bool SygusUnif::constructSolution(std::vector<Node>& sols)
{
// initialize a call to construct solution
initializeConstructSol();
- // call the virtual construct solution method
- Node e = d_strategy.getRootEnumerator();
- return constructSol(e, role_equal, 1);
+ for (const Node& f : d_candidates)
+ {
+ // initialize a call to construct solution for function f
+ initializeConstructSolFor(f);
+ // call the virtual construct solution method
+ Node e = d_strategy[f].getRootEnumerator();
+ Node sol = constructSol(f, e, role_equal, 1);
+ if (sol.isNull())
+ {
+ return false;
+ }
+ sols.push_back(sol);
+ }
+ return true;
}
Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
/** Sygus unification utility
*
* This utility implements synthesis-by-unification style approaches for a
- * single function to synthesize f.
- * These approaches include a combination of:
+ * set of functions-to-synthesize. These approaches include a combination of:
* (1) Decision tree learning, inspired by Alur et al TACAS 2017,
* (2) Divide-and-conquer via string concatenation.
*
- * This class maintains:
+ * This class maintains, for each function-to-synthesize f:
* (1) A "strategy tree" based on the syntactic restrictions for f that is
* constructed during initialize (d_strategy),
- * (2) A set of input/output examples that are the specification for f. This
- * can be updated via calls to resetExmaples/addExamples,
- * (3) A set of terms that have been enumerated for enumerators (d_ecache). This
- * can be updated via calls to notifyEnumeration.
*
* Based on the above, solutions can be constructed via calls to
* constructSolution.
/** initialize
*
- * This initializes this class with function-to-synthesize f. We also call
- * f the candidate variable.
+ * This initializes this class with functions-to-synthesize funs. We also call
+ * these "candidate variables".
*
* This call constructs a set of enumerators for the relevant subfields of
* the grammar of f and adds them to enums. These enumerators are those that
* strategy is ITE_strat).
*/
virtual void initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas);
virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0;
/** construct solution
*
- * This attempts to construct a solution based on the current set of
- * enumerated values. Returns null if it cannot (for example, if the
- * set of enumerated values is insufficient, or if a non-deterministic
- * strategy aborts).
+ * This attempts to construct a solution for each function-to-synthesize
+ * based on the current set of enumerated values. Returns null if it cannot
+ * for some function (for example, if the set of enumerated values is
+ * insufficient, or if a non-deterministic strategy aborts).
*/
- virtual Node constructSolution();
+ virtual bool constructSolution(std::vector<Node>& sols);
protected:
/** reference to quantifier engine */
std::vector<Node>& vals,
bool pol = true);
//-----------------------end debug printing
- /** the candidate for this class */
- Node d_candidate;
+ /** the candidates for this class */
+ std::vector<Node> d_candidates;
/** maps a function-to-synthesize to the above information */
- SygusUnifStrategy d_strategy;
+ std::map<Node, SygusUnifStrategy> d_strategy;
/** domain-specific enumerator exclusion techniques
*
* Called once before each attempt to construct solutions.
*/
virtual void initializeConstructSol() = 0;
+ /** implementation-dependent initialize construct solution
+ *
+ * Called once before each attempt to construct solution for a
+ * function-to-synthesize f.
+ */
+ virtual void initializeConstructSolFor(Node f) = 0;
/** implementation-dependent function for construct solution.
*
* Construct a solution based on enumerator e for function-to-synthesize of
*
* ind is the term depth of the context (for debugging).
*/
- virtual Node constructSol(Node e, NodeRole nrole, int ind) = 0;
+ virtual Node constructSol(Node f, Node e, NodeRole nrole, int ind) = 0;
/** Heuristically choose the best solved term from solved in context x,
* currently return the first. */
virtual Node constructBestSolvedTerm(const std::vector<Node>& solved);
}
SygusUnifIo::~SygusUnifIo() {}
-
void SygusUnifIo::initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas)
{
+ Assert(funs.size() == 1);
d_examples.clear();
d_examples_out.clear();
d_ecache.clear();
- SygusUnif::initialize(qe, f, enums, lemmas);
+ d_candidate = funs[0];
+ SygusUnif::initialize(qe, funs, enums, lemmas);
}
void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
Assert(!d_examples.empty());
Assert(d_examples.size() == d_examples_out.size());
- EnumInfo& ei = d_strategy.getEnumInfo(e);
+ EnumInfo& ei = d_strategy[c].getEnumInfo(e);
// The explanation for why the current value should be excluded in future
// iterations.
Node exp_exc;
{
Node xs = ei.d_enum_slave[s];
- EnumInfo& eiv = d_strategy.getEnumInfo(xs);
+ EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
EnumCache& ecv = d_ecache[xs];
lemmas.push_back(exp_exc);
}
-Node SygusUnifIo::constructSolution()
+bool SygusUnifIo::constructSolution(std::vector<Node>& sols)
+{
+ Node sol = constructSolutionNode();
+ if (!sol.isNull())
+ {
+ sols.push_back(sol);
+ return true;
+ }
+ return false;
+}
+
+Node SygusUnifIo::constructSolutionNode()
{
Node c = d_candidate;
if (!d_solution.isNull())
Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
// initialize a call to construct solution
initializeConstructSol();
+ initializeConstructSolFor(c);
// call the virtual construct solution method
- Node e = d_strategy.getRootEnumerator();
- Node vcc = constructSol(e, role_equal, 1);
+ Node e = d_strategy[c].getRootEnumerator();
+ Node vcc = constructSol(c, e, role_equal, 1);
// if we constructed the solution, and we either did not previously have
// a solution, or the new solution is better (smaller).
if (!vcc.isNull()
Trace("sygus-sui-enum-debug")
<< "Is " << e << " is str.contains exclusion?" << std::endl;
d_use_str_contains_eexc[e] = true;
- EnumInfo& ei = d_strategy.getEnumInfo(e);
+ Node c = d_candidate;
+ EnumInfo& ei = d_strategy[c].getEnumInfo(e);
for (const Node& sn : ei.d_enum_slave)
{
- EnumInfo& eis = d_strategy.getEnumInfo(sn);
+ EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
EnumRole er = eis.getRole();
if (er != enum_io && er != enum_concat_term)
{
}
void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); }
+void SygusUnifIo::initializeConstructSolFor(Node f)
+{
+ Assert(d_candidate == f);
+}
-Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind)
+Node SygusUnifIo::constructSol(Node f, Node e, NodeRole nrole, int ind)
{
+ Assert(d_candidate == f);
UnifContextIo& x = d_context;
TypeNode etn = e.getType();
if (Trace.isOn("sygus-sui-dt-debug"))
Trace("sygus-sui-dt-debug") << std::endl;
}
// enumerator type info
- EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
// get the enumerator information
- EnumInfo& einfo = d_strategy.getEnumInfo(e);
+ EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
EnumCache& ecache = d_ecache[e];
}
else
{
- rec_c = constructSol(cenum.first, cenum.second, ind + 2);
+ rec_c = constructSol(f, cenum.first, cenum.second, ind + 2);
}
// undo update the context
* This class implement synthesis-by-unification, where the specification is
* I/O examples. With respect to SygusUnif, it's main interface function is
* addExample, which adds an I/O example to the specification.
+ *
+ * Since I/O specifications for multiple functions can be fully separated, we
+ * assume that this class is used only for a single function to synthesize.
+ *
+ * In addition to the base class which maintains a strategy tree, this class
+ * maintains:
+ * (1) A set of input/output examples that are the specification for f. This
+ * can be updated via calls to resetExmaples/addExamples,
+ * (2) A set of terms that have been enumerated for enumerators (d_ecache). This
+ * can be updated via calls to notifyEnumeration.
*/
class SygusUnifIo : public SygusUnif
{
SygusUnifIo();
~SygusUnifIo();
- /** initialize */
+ /** initialize
+ *
+ * The vector funs should be of length one, since I/O specifications across
+ * multiple functions can be separated.
+ */
virtual void initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas) override;
/** Notify enumeration */
std::vector<Node>& lemmas) override;
/** Construct solution */
- virtual Node constructSolution() override;
+ virtual bool constructSolution(std::vector<Node>& sols) override;
/** add example
*
void addExample(const std::vector<Node>& input, Node output);
protected:
+ /** the candidate */
+ Node d_candidate;
/**
* Whether we will try to construct solution on the next call to
* constructSolution. This flag is set to true when we successfully
};
/** maps enumerators to the information above */
std::map<Node, EnumCache> d_ecache;
-
+ /** Construct solution node
+ *
+ * This is called for the (single) function-to-synthesize during a call to
+ * constructSolution. If this returns a non-null node, then that term is a
+ * solution for the function-to-synthesize in the overall conjecture.
+ */
+ Node constructSolutionNode();
/** domain-specific enumerator exclusion techniques
*
* Returns true if the value v for e can be excluded based on a
UnifContextIo d_context;
/** initialize construct solution */
void initializeConstructSol() override;
+ /** initialize construct solution for */
+ void initializeConstructSolFor(Node f) override;
/** construct solution */
- Node constructSol(Node e, NodeRole nrole, int ind) override;
+ Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
};
} /* CVC4::theory::quantifiers namespace */
SygusUnifRl::SygusUnifRl() {}
SygusUnifRl::~SygusUnifRl() {}
-
void SygusUnifRl::initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas)
{
d_rlemmas = d_true;
d_hasRLemmas = false;
d_ecache.clear();
- SygusUnif::initialize(qe, f, enums, lemmas);
+ SygusUnif::initialize(qe, funs, enums, lemmas);
}
void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
}
}
-Node SygusUnifRl::constructSol(Node e, NodeRole nrole, int ind)
+void SygusUnifRl::initializeConstructSolFor(Node f) {}
+Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
{
Node solution = canCloseBranch(e);
if (!solution.isNull())
/** initialize */
void initialize(QuantifiersEngine* qe,
- Node f,
+ const std::vector<Node>& funs,
std::vector<Node>& enums,
std::vector<Node>& lemmas) override;
/** Notify enumeration */
* from d_rlemmas, in which case we may have added or removed data points
*/
void initializeConstructSol() override;
+ /** initialize construction solution for function-to-synthesize f */
+ void initializeConstructSolFor(Node f) override;
/**
* Returns a term covering all data points in the current branch, on null if
* none can be found among the currently enumerated values for the respective
Node canCloseBranch(Node e);
/** construct solution */
- Node constructSol(Node e, NodeRole nrole, int ind) override;
+ Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
};
} /* CVC4::theory::quantifiers namespace */
regress1/sygus/nia-max-square-ns.sy \
regress1/sygus/no-flat-simp.sy \
regress1/sygus/no-mention.sy \
+ regress1/sygus/pbe_multi.sy \
regress1/sygus/process-10-vars.sy \
regress1/sygus/qe.sy \
regress1/sygus/real-grammar.sy \
--- /dev/null
+; EXPECT: unsat\r
+; COMMAND-LINE: --sygus-out=status\r
+(set-logic BV)\r
+\r
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))\r
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))\r
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))\r
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))\r
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))\r
+\r
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)\r
+(\r
+\r
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)\r
+ ))\r
+)\r
+)\r
+\r
+\r
+(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee))\r
+(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2))\r
+(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e))\r
+(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee))\r
+(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42))\r
+(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4))\r
+(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4))\r
+(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60))\r
+(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))\r
+(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))\r
+\r
+(synth-fun g ( (x (BitVec 64))) (BitVec 64)\r
+(\r
+\r
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)\r
+ ))\r
+)\r
+)\r
+\r
+(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe))\r
+(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd))\r
+(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d))\r
+(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe))\r
+(constraint (= (g #x352367e34d76550b) #x352367e34d76550b))\r
+(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe))\r
+(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe))\r
+(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe))\r
+(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe))\r
+(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe))\r
+(check-synth)\r
projects / cvc5.git / commitdiff