From: Andrew Reynolds Date: Mon, 30 Apr 2018 03:25:42 +0000 (-0500) Subject: Allow multiple functions in sygus unif approaches (#1831) X-Git-Tag: cvc5-1.0.0~5111 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58985bed1bb0a812d97b3d490268023a164ba5e5;p=cvc5.git Allow multiple functions in sygus unif approaches (#1831) --- diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 7794ec912..256955bbd 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -44,7 +44,7 @@ bool CegisUnif::initialize(Node n, 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"; @@ -129,14 +129,13 @@ bool CegisUnif::constructCandidates(const std::vector& enums, } /* 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, diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 65b8ba133..472cfbd89 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -143,45 +143,53 @@ bool CegConjecturePbe::initialize(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 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, @@ -384,11 +392,15 @@ bool CegConjecturePbe::constructCandidates(const std::vector& enums, for( unsigned i=0; i 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; diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 9a017d21b..dc927388e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -29,27 +29,40 @@ namespace quantifiers { SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {} SygusUnif::~SygusUnif() {} - void SygusUnif::initialize(QuantifiersEngine* qe, - Node f, + const std::vector& funs, std::vector& enums, std::vector& 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& 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& solved) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index beb2023f9..e55f7e6ff 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -29,18 +29,13 @@ namespace quantifiers { /** 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. @@ -53,8 +48,8 @@ class SygusUnif /** 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 @@ -66,7 +61,7 @@ class SygusUnif * strategy is ITE_strat). */ virtual void initialize(QuantifiersEngine* qe, - Node f, + const std::vector& funs, std::vector& enums, std::vector& lemmas); @@ -78,12 +73,12 @@ class SygusUnif virtual void notifyEnumeration(Node e, Node v, std::vector& 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& sols); protected: /** reference to quantifier engine */ @@ -99,10 +94,10 @@ class SygusUnif std::vector& vals, bool pol = true); //-----------------------end debug printing - /** the candidate for this class */ - Node d_candidate; + /** the candidates for this class */ + std::vector d_candidates; /** maps a function-to-synthesize to the above information */ - SygusUnifStrategy d_strategy; + std::map d_strategy; /** domain-specific enumerator exclusion techniques * @@ -139,6 +134,12 @@ class SygusUnif * 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 @@ -146,7 +147,7 @@ class SygusUnif * * 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& solved); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 7a134b1c0..eb607d2c3 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -466,16 +466,17 @@ SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0) } SygusUnifIo::~SygusUnifIo() {} - void SygusUnifIo::initialize(QuantifiersEngine* qe, - Node f, + const std::vector& funs, std::vector& enums, std::vector& 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& input, Node output) @@ -492,7 +493,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) 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; @@ -528,7 +529,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) { 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]; @@ -677,7 +678,18 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) lemmas.push_back(exp_exc); } -Node SygusUnifIo::constructSolution() +bool SygusUnifIo::constructSolution(std::vector& 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()) @@ -699,9 +711,10 @@ Node SygusUnifIo::constructSolution() 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() @@ -740,10 +753,11 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) 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) { @@ -833,9 +847,14 @@ void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector& results) } 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")) @@ -858,10 +877,10 @@ Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind) 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]; @@ -1264,7 +1283,7 @@ Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind) } else { - rec_c = constructSol(cenum.first, cenum.second, ind + 2); + rec_c = constructSol(f, cenum.first, cenum.second, ind + 2); } // undo update the context diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 276cc9da2..b0d6ce3ce 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -252,6 +252,16 @@ class SubsumeTrie * 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 { @@ -261,9 +271,13 @@ 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& funs, std::vector& enums, std::vector& lemmas) override; /** Notify enumeration */ @@ -272,7 +286,7 @@ class SygusUnifIo : public SygusUnif std::vector& lemmas) override; /** Construct solution */ - virtual Node constructSolution() override; + virtual bool constructSolution(std::vector& sols) override; /** add example * @@ -284,6 +298,8 @@ class SygusUnifIo : public SygusUnif void addExample(const std::vector& 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 @@ -356,7 +372,13 @@ class SygusUnifIo : public SygusUnif }; /** maps enumerators to the information above */ std::map 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 @@ -390,8 +412,10 @@ class SygusUnifIo : public SygusUnif 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 */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 723210ca1..bf23cd0d1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -25,9 +25,8 @@ namespace quantifiers { SygusUnifRl::SygusUnifRl() {} SygusUnifRl::~SygusUnifRl() {} - void SygusUnifRl::initialize(QuantifiersEngine* qe, - Node f, + const std::vector& funs, std::vector& enums, std::vector& lemmas) { @@ -37,7 +36,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, 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& lemmas) @@ -120,7 +119,8 @@ void SygusUnifRl::initializeConstructSol() } } -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()) diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 0f3871056..13d0d1e56 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -38,7 +38,7 @@ class SygusUnifRl : public SygusUnif /** initialize */ void initialize(QuantifiersEngine* qe, - Node f, + const std::vector& funs, std::vector& enums, std::vector& lemmas) override; /** Notify enumeration */ @@ -87,6 +87,8 @@ class SygusUnifRl : public SygusUnif * 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 @@ -95,7 +97,7 @@ class SygusUnifRl : public SygusUnif 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 */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 1ec6323b2..f799c20d5 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1479,6 +1479,7 @@ REG1_TESTS = \ 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 \ diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy new file mode 100644 index 000000000..70cb6b2d2 --- /dev/null +++ b/test/regress/regress1/sygus/pbe_multi.sy @@ -0,0 +1,67 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) + + +(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee)) +(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2)) +(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e)) +(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee)) +(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42)) +(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4)) +(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4)) +(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60)) +(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee)) +(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a)) + +(synth-fun g ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) + +(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe)) +(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd)) +(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d)) +(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe)) +(constraint (= (g #x352367e34d76550b) #x352367e34d76550b)) +(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe)) +(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe)) +(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe)) +(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe)) +(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe)) +(check-synth)