From: Andrew Reynolds Date: Fri, 18 May 2018 17:53:53 +0000 (-0500) Subject: Unified fairness scheme for cegis unif (#1941) X-Git-Tag: cvc5-1.0.0~5039 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a94704db9d3e66ed7f54f75a37096e543552866;p=cvc5.git Unified fairness scheme for cegis unif (#1941) --- diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 692055b87..57c4c1ad3 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -330,11 +330,23 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, std::vector& es, unsigned index) const { - std::map::const_iterator itc = d_ce_info.find(e); - Assert(itc != d_ce_info.end()); - es.insert(es.end(), - itc->second.d_enums[index].begin(), - itc->second.d_enums[index].end()); + // the number of active enumerators is related to the current cost value + unsigned num_enums = d_curr_guq_val.get(); + Assert(num_enums > 0); + if (index == 1) + { + // we always use (cost-1) conditions + num_enums = num_enums - 1; + } + if (num_enums > 0) + { + std::map::const_iterator itc = d_ce_info.find(e); + Assert(itc != d_ce_info.end()); + Assert(num_enums <= itc->second.d_enums[index].size()); + es.insert(es.end(), + itc->second.d_enums[index].begin(), + itc->second.d_enums[index].begin() + num_enums); + } } void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) @@ -469,6 +481,57 @@ void CegisUnifEnumManager::incrementNumEnumerators() registerEvalPtAtSize(c, ei, new_lit, new_size); } } + // enforce fairness between number of enumerators and enumerator size + if (new_size > 1) + { + // construct the "virtual enumerator" + if (d_virtual_enum.isNull()) + { + // we construct the default integer grammar with no variables, e.g.: + // A -> 0 | 1 | A+A + TypeNode intTn = nm->integerType(); + // use a null variable list + Node bvl; + std::stringstream ss; + ss << "_virtual_enum_grammar"; + std::string virtualEnumName(ss.str()); + std::map> extra_cons; + std::map> exclude_cons; + // do not include "-", which is included by default for integers + exclude_cons[intTn].push_back(nm->operatorOf(MINUS)); + std::unordered_set term_irrelevant; + TypeNode vtn = + CegGrammarConstructor::mkSygusDefaultType(intTn, + bvl, + virtualEnumName, + extra_cons, + exclude_cons, + term_irrelevant); + d_virtual_enum = nm->mkSkolem("_ve", vtn); + d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + } + // if new_size is a power of two, then isPow2 returns log2(new_size)+1 + // otherwise, this returns 0. In the case it returns 0, we don't care + // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not + // increase our size bound. + unsigned pow_two = Integer(new_size).isPow2(); + if (pow_two > 0) + { + Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); + Node fair_lemma = + nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); + fair_lemma = nm->mkNode(OR, new_lit, fair_lemma); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; + // this lemma relates the number of conditions we enumerate and the + // maximum size of a term that is part of our solution. It is of the + // form: + // G_uq_i => size(ve) >= log_2( i-1 ) + // In other words, if we use i conditions, then we allow terms in our + // solution whose size is at most log_2(i-1). + d_qe->getOutputChannel().lemma(fair_lemma); + } + } } } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 5c2c11e4d..80c11f82d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -142,6 +142,24 @@ class CegisUnifEnumManager std::map d_guq_lit; /** Have we returned a decision in the current SAT context? */ context::CDO d_ret_dec; + /** the "virtual" enumerator + * + * This enumerator is used for enforcing fairness. In particular, we relate + * its size to the number of conditions allocated by this class such that: + * ~G_uq_i => size(d_virtual_enum) >= floor( log2( i-1 ) ) + * In other words, if we are using (i-1) conditions in our solution, + * the size of the virtual enumerator is at least the floor of the log (base + * two) of (i-1). Due to the default fairness scheme in the quantifier-free + * datatypes solver (if --sygus-fair-max is enabled), this ensures that other + * enumerators are allowed to have at least this size. This affect other + * fairness schemes in an analogous fashion. In particular, we enumerate + * based on the tuples for (term size, #conditions): + * (0,0), (0,1) [size 0] + * (0,2), (0,3), (1,1), (1,2), (1,3) [size 1] + * (0,4), ..., (0,7), (1,4), ..., (1,7), (2,0), ..., (2,7) [size 2] + * (0,8), ..., (0,15), (1,8), ..., (1,15), ... [size 3] + */ + Node d_virtual_enum; /** * The minimal n such that G_uq_n is not asserted negatively in the * current SAT context. diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 412d1b211..3d8052ae4 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -99,6 +99,7 @@ Node CegGrammarConstructor::process(Node q, Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; collectTerms( q[1], extra_cons ); } + std::map> exc_cons; NodeManager* nm = NodeManager::currentNM(); @@ -140,20 +141,17 @@ Node CegGrammarConstructor::process(Node q, // check which arguments are irrelevant std::unordered_set arg_irrelevant; d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); - std::unordered_set term_irrelevant; + std::unordered_set term_irlv; // convert to term - for (std::unordered_set::iterator ita = arg_irrelevant.begin(); - ita != arg_irrelevant.end(); - ++ita) + for (const unsigned& arg : arg_irrelevant) { - unsigned arg = *ita; Assert(arg < sfvl.getNumChildren()); - term_irrelevant.insert(sfvl[arg]); + term_irlv.insert(sfvl[arg]); } // make the default grammar tn = mkSygusDefaultType( - preGrammarType, sfvl, ss.str(), extra_cons, term_irrelevant); + preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv); } // normalize type @@ -389,7 +387,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, - std::map >& extra_cons, + std::map>& extra_cons, + std::map>& exc_cons, std::unordered_set& term_irrelevant, std::vector& datatypes, std::set& unres) @@ -589,8 +588,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl; datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); - for( unsigned j=0; j>::iterator itexc = + exc_cons.find(types[i]); + for (unsigned j = 0, size = ops[i].size(); j < size; j++) + { + // add the constructor if it is not excluded + Node opn = Node::fromExpr(ops[i][j]); + if (itexc == exc_cons.end() + || std::find(itexc->second.begin(), itexc->second.end(), opn) + == itexc->second.end()) + { + datatypes[i].addSygusConstructor(ops[i][j], cnames[j], cargs[j]); + } } Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " "; @@ -717,7 +726,8 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, - std::map >& extra_cons, + std::map>& extra_cons, + std::map>& exclude_cons, std::unordered_set& term_irrelevant) { Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; @@ -726,8 +736,14 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( } std::set unres; std::vector< CVC4::Datatype > datatypes; - mkSygusDefaultGrammar( - range, bvl, fun, extra_cons, term_irrelevant, datatypes, unres); + mkSygusDefaultGrammar(range, + bvl, + fun, + extra_cons, + exclude_cons, + term_irrelevant, + datatypes, + unres); Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert( !datatypes.empty() ); std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 39f95527f..578325fea 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -67,7 +67,8 @@ public: /** make the default sygus datatype type corresponding to builtin type range * bvl is the set of free variables to include in the grammar * fun is for naming - * extra_cons is a set of extra constant symbols to include in the grammar + * extra_cons is a set of extra constant symbols to include in the grammar, + * exclude_cons is used to exclude operators from the grammar, * term_irrelevant is a set of terms that should not be included in the * grammar. */ @@ -76,6 +77,7 @@ public: Node bvl, const std::string& fun, std::map >& extra_cons, + std::map >& exclude_cons, std::unordered_set& term_irrelevant); /** make the default sygus datatype type corresponding to builtin type range */ static TypeNode mkSygusDefaultType(TypeNode range, @@ -83,8 +85,10 @@ public: const std::string& fun) { std::map > extra_cons; + std::map > exclude_cons; std::unordered_set term_irrelevant; - return mkSygusDefaultType(range, bvl, fun, extra_cons, term_irrelevant); + return mkSygusDefaultType( + range, bvl, fun, extra_cons, exclude_cons, term_irrelevant); } /** make the sygus datatype type that encodes the solution space (lambda * templ_arg. templ[templ_arg]) where templ_arg @@ -138,6 +142,7 @@ public: Node bvl, const std::string& fun, std::map >& extra_cons, + std::map >& exclude_cons, std::unordered_set& term_irrelevant, std::vector& datatypes, std::set& unres); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 85ff5c896..5efa1198b 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -752,8 +752,14 @@ void TermDbSygus::registerEnumerator(Node e, CegConjecture* conj, bool mkActiveGuard) { - Assert(d_enum_to_conjecture.find(e) == d_enum_to_conjecture.end()); - Trace("sygus-db") << "Register measured term : " << e << std::endl; + if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) + { + // already registered + return; + } + Trace("sygus-db") << "Register enumerator : " << e << std::endl; + // register its type + registerSygusType(e.getType()); d_enum_to_conjecture[e] = conj; d_enum_to_synth_fun[e] = f; if( mkActiveGuard ){ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index a9e17fdf9..d53e436e0 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -38,7 +38,13 @@ class TermDbSygus { bool reset(Theory::Effort e); /** Identify this utility */ std::string identify() const { return "TermDbSygus"; } - /** register the sygus type */ + /** register the sygus type + * + * This initializes this database for sygus datatype type tn. This may + * throw an assertion failure if the sygus grammar has type errors. Otherwise, + * after registering a sygus type, the query functions in this class (such + * as sygusToBuiltinType, getKindConsNum, etc.) can be called for tn. + */ void registerSygusType(TypeNode tn); //------------------------------utilities diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 687ed3c86..745183a6b 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1471,6 +1471,7 @@ REG1_TESTS = \ regress1/sygus/array_sum_2_5.sy \ regress1/sygus/cegar1.sy \ regress1/sygus/cegisunif-depth1.sy \ + regress1/sygus/cegis-unif-inv-eq-fair.sy \ regress1/sygus/cggmp.sy \ regress1/sygus/clock-inc-tuple.sy \ regress1/sygus/commutative.sy \ diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy new file mode 100644 index 000000000..7d1c35234 --- /dev/null +++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -0,0 +1,536 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status +(set-logic LIA) + +(define-fun + __node_init_Sofar_0 ( + (Sofar.usr.X@0 Bool) + (Sofar.usr.Sofar@0 Bool) + (Sofar.res.init_flag@0 Bool) + ) Bool + + (and (= Sofar.usr.Sofar@0 Sofar.usr.X@0) Sofar.res.init_flag@0) +) + +(define-fun + __node_trans_Sofar_0 ( + (Sofar.usr.X@1 Bool) + (Sofar.usr.Sofar@1 Bool) + (Sofar.res.init_flag@1 Bool) + (Sofar.usr.X@0 Bool) + (Sofar.usr.Sofar@0 Bool) + (Sofar.res.init_flag@0 Bool) + ) Bool + + (and + (= Sofar.usr.Sofar@1 (and Sofar.usr.X@1 Sofar.usr.Sofar@0)) + (not Sofar.res.init_flag@1)) +) + +(define-fun + __node_init_excludes2_0 ( + (excludes2.usr.X1@0 Bool) + (excludes2.usr.X2@0 Bool) + (excludes2.usr.excludes@0 Bool) + (excludes2.res.init_flag@0 Bool) + ) Bool + + (and + (= + excludes2.usr.excludes@0 + (not (and excludes2.usr.X1@0 excludes2.usr.X2@0))) + excludes2.res.init_flag@0) +) + +(define-fun + __node_trans_excludes2_0 ( + (excludes2.usr.X1@1 Bool) + (excludes2.usr.X2@1 Bool) + (excludes2.usr.excludes@1 Bool) + (excludes2.res.init_flag@1 Bool) + (excludes2.usr.X1@0 Bool) + (excludes2.usr.X2@0 Bool) + (excludes2.usr.excludes@0 Bool) + (excludes2.res.init_flag@0 Bool) + ) Bool + + (and + (= + excludes2.usr.excludes@1 + (not (and excludes2.usr.X1@1 excludes2.usr.X2@1))) + (not excludes2.res.init_flag@1)) +) + +(define-fun + __node_init_voiture_0 ( + (voiture.usr.m@0 Bool) + (voiture.usr.s@0 Bool) + (voiture.usr.toofast@0 Bool) + (voiture.usr.stop@0 Bool) + (voiture.usr.bump@0 Bool) + (voiture.usr.dist@0 Int) + (voiture.usr.speed@0 Int) + (voiture.usr.time@0 Int) + (voiture.usr.move@0 Bool) + (voiture.usr.second@0 Bool) + (voiture.usr.meter@0 Bool) + (voiture.res.init_flag@0 Bool) + (voiture.res.abs_0@0 Bool) + ) Bool + + (and + (= voiture.usr.speed@0 0) + (= voiture.usr.toofast@0 (>= voiture.usr.speed@0 3)) + (= voiture.usr.move@0 true) + (= voiture.usr.time@0 0) + (= voiture.usr.dist@0 0) + (= voiture.usr.bump@0 (= voiture.usr.dist@0 10)) + (= voiture.usr.stop@0 (>= voiture.usr.time@0 4)) + (= + voiture.res.abs_0@0 + (and + (and + (and voiture.usr.move@0 (not voiture.usr.stop@0)) + (not voiture.usr.toofast@0)) + (not voiture.usr.bump@0))) + (= voiture.usr.second@0 false) + (= voiture.usr.meter@0 false) + voiture.res.init_flag@0) +) + +(define-fun + __node_trans_voiture_0 ( + (voiture.usr.m@1 Bool) + (voiture.usr.s@1 Bool) + (voiture.usr.toofast@1 Bool) + (voiture.usr.stop@1 Bool) + (voiture.usr.bump@1 Bool) + (voiture.usr.dist@1 Int) + (voiture.usr.speed@1 Int) + (voiture.usr.time@1 Int) + (voiture.usr.move@1 Bool) + (voiture.usr.second@1 Bool) + (voiture.usr.meter@1 Bool) + (voiture.res.init_flag@1 Bool) + (voiture.res.abs_0@1 Bool) + (voiture.usr.m@0 Bool) + (voiture.usr.s@0 Bool) + (voiture.usr.toofast@0 Bool) + (voiture.usr.stop@0 Bool) + (voiture.usr.bump@0 Bool) + (voiture.usr.dist@0 Int) + (voiture.usr.speed@0 Int) + (voiture.usr.time@0 Int) + (voiture.usr.move@0 Bool) + (voiture.usr.second@0 Bool) + (voiture.usr.meter@0 Bool) + (voiture.res.init_flag@0 Bool) + (voiture.res.abs_0@0 Bool) + ) Bool + + (and + (= voiture.usr.meter@1 (and voiture.usr.m@1 (not voiture.usr.s@1))) + (= voiture.usr.second@1 voiture.usr.s@1) + (= voiture.usr.move@1 voiture.res.abs_0@0) + (= + voiture.usr.speed@1 + (ite + (or (not voiture.usr.move@1) voiture.usr.second@1) + 0 + (ite + (and voiture.usr.move@1 voiture.usr.meter@1) + (+ (- voiture.usr.speed@0 1) 1) + voiture.usr.speed@0))) + (= voiture.usr.toofast@1 (>= voiture.usr.speed@1 3)) + (= + voiture.usr.time@1 + (ite voiture.usr.second@1 (+ voiture.usr.time@0 1) voiture.usr.time@0)) + (= + voiture.usr.dist@1 + (ite + (and voiture.usr.move@1 voiture.usr.meter@1) + (+ voiture.usr.dist@0 1) + voiture.usr.dist@0)) + (= voiture.usr.bump@1 (= voiture.usr.dist@1 10)) + (= voiture.usr.stop@1 (>= voiture.usr.time@1 4)) + (= + voiture.res.abs_0@1 + (and + (and + (and voiture.usr.move@1 (not voiture.usr.stop@1)) + (not voiture.usr.toofast@1)) + (not voiture.usr.bump@1))) + (not voiture.res.init_flag@1)) +) + +(define-fun + __node_init_top_0 ( + (top.usr.m@0 Bool) + (top.usr.s@0 Bool) + (top.usr.OK@0 Bool) + (top.res.init_flag@0 Bool) + (top.res.abs_0@0 Bool) + (top.res.abs_1@0 Bool) + (top.res.abs_2@0 Bool) + (top.res.abs_3@0 Int) + (top.res.abs_4@0 Int) + (top.res.abs_5@0 Int) + (top.res.abs_6@0 Bool) + (top.res.abs_7@0 Bool) + (top.res.abs_8@0 Bool) + (top.res.abs_9@0 Bool) + (top.res.abs_10@0 Bool) + (top.res.inst_3@0 Bool) + (top.res.inst_2@0 Bool) + (top.res.inst_1@0 Bool) + (top.res.inst_0@0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10@0)) + (let + ((X2 Int top.res.abs_4@0)) + (and + (= top.usr.OK@0 (=> X1 (< X2 4))) + (__node_init_voiture_0 + top.usr.m@0 + top.usr.s@0 + top.res.abs_0@0 + top.res.abs_1@0 + top.res.abs_2@0 + top.res.abs_3@0 + top.res.abs_4@0 + top.res.abs_5@0 + top.res.abs_6@0 + top.res.abs_7@0 + top.res.abs_8@0 + top.res.inst_3@0 + top.res.inst_2@0) + (__node_init_Sofar_0 top.res.abs_9@0 top.res.abs_10@0 top.res.inst_1@0) + (__node_init_excludes2_0 + top.usr.m@0 + top.usr.s@0 + top.res.abs_9@0 + top.res.inst_0@0) + top.res.init_flag@0))) +) + +(define-fun + __node_trans_top_0 ( + (top.usr.m@1 Bool) + (top.usr.s@1 Bool) + (top.usr.OK@1 Bool) + (top.res.init_flag@1 Bool) + (top.res.abs_0@1 Bool) + (top.res.abs_1@1 Bool) + (top.res.abs_2@1 Bool) + (top.res.abs_3@1 Int) + (top.res.abs_4@1 Int) + (top.res.abs_5@1 Int) + (top.res.abs_6@1 Bool) + (top.res.abs_7@1 Bool) + (top.res.abs_8@1 Bool) + (top.res.abs_9@1 Bool) + (top.res.abs_10@1 Bool) + (top.res.inst_3@1 Bool) + (top.res.inst_2@1 Bool) + (top.res.inst_1@1 Bool) + (top.res.inst_0@1 Bool) + (top.usr.m@0 Bool) + (top.usr.s@0 Bool) + (top.usr.OK@0 Bool) + (top.res.init_flag@0 Bool) + (top.res.abs_0@0 Bool) + (top.res.abs_1@0 Bool) + (top.res.abs_2@0 Bool) + (top.res.abs_3@0 Int) + (top.res.abs_4@0 Int) + (top.res.abs_5@0 Int) + (top.res.abs_6@0 Bool) + (top.res.abs_7@0 Bool) + (top.res.abs_8@0 Bool) + (top.res.abs_9@0 Bool) + (top.res.abs_10@0 Bool) + (top.res.inst_3@0 Bool) + (top.res.inst_2@0 Bool) + (top.res.inst_1@0 Bool) + (top.res.inst_0@0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10@1)) + (let + ((X2 Int top.res.abs_4@1)) + (and + (= top.usr.OK@1 (=> X1 (< X2 4))) + (__node_trans_voiture_0 + top.usr.m@1 + top.usr.s@1 + top.res.abs_0@1 + top.res.abs_1@1 + top.res.abs_2@1 + top.res.abs_3@1 + top.res.abs_4@1 + top.res.abs_5@1 + top.res.abs_6@1 + top.res.abs_7@1 + top.res.abs_8@1 + top.res.inst_3@1 + top.res.inst_2@1 + top.usr.m@0 + top.usr.s@0 + top.res.abs_0@0 + top.res.abs_1@0 + top.res.abs_2@0 + top.res.abs_3@0 + top.res.abs_4@0 + top.res.abs_5@0 + top.res.abs_6@0 + top.res.abs_7@0 + top.res.abs_8@0 + top.res.inst_3@0 + top.res.inst_2@0) + (__node_trans_Sofar_0 + top.res.abs_9@1 + top.res.abs_10@1 + top.res.inst_1@1 + top.res.abs_9@0 + top.res.abs_10@0 + top.res.inst_1@0) + (__node_trans_excludes2_0 + top.usr.m@1 + top.usr.s@1 + top.res.abs_9@1 + top.res.inst_0@1 + top.usr.m@0 + top.usr.s@0 + top.res.abs_9@0 + top.res.inst_0@0) + (not top.res.init_flag@1)))) +) + + + +(synth-inv str_invariant( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) +)) + + +(declare-primed-var top.usr.m Bool) +(declare-primed-var top.usr.s Bool) +(declare-primed-var top.usr.OK Bool) +(declare-primed-var top.res.init_flag Bool) +(declare-primed-var top.res.abs_0 Bool) +(declare-primed-var top.res.abs_1 Bool) +(declare-primed-var top.res.abs_2 Bool) +(declare-primed-var top.res.abs_3 Int) +(declare-primed-var top.res.abs_4 Int) +(declare-primed-var top.res.abs_5 Int) +(declare-primed-var top.res.abs_6 Bool) +(declare-primed-var top.res.abs_7 Bool) +(declare-primed-var top.res.abs_8 Bool) +(declare-primed-var top.res.abs_9 Bool) +(declare-primed-var top.res.abs_10 Bool) +(declare-primed-var top.res.inst_3 Bool) +(declare-primed-var top.res.inst_2 Bool) +(declare-primed-var top.res.inst_1 Bool) +(declare-primed-var top.res.inst_0 Bool) + +(define-fun + init ( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10)) + (let + ((X2 Int top.res.abs_4)) + (and + (= top.usr.OK (=> X1 (< X2 4))) + (__node_init_voiture_0 + top.usr.m + top.usr.s + top.res.abs_0 + top.res.abs_1 + top.res.abs_2 + top.res.abs_3 + top.res.abs_4 + top.res.abs_5 + top.res.abs_6 + top.res.abs_7 + top.res.abs_8 + top.res.inst_3 + top.res.inst_2) + (__node_init_Sofar_0 top.res.abs_9 top.res.abs_10 top.res.inst_1) + (__node_init_excludes2_0 + top.usr.m + top.usr.s + top.res.abs_9 + top.res.inst_0) + top.res.init_flag))) +) + +(define-fun + trans ( + + ;; Current state. + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + + ;; Next state. + (top.usr.m! Bool) + (top.usr.s! Bool) + (top.usr.OK! Bool) + (top.res.init_flag! Bool) + (top.res.abs_0! Bool) + (top.res.abs_1! Bool) + (top.res.abs_2! Bool) + (top.res.abs_3! Int) + (top.res.abs_4! Int) + (top.res.abs_5! Int) + (top.res.abs_6! Bool) + (top.res.abs_7! Bool) + (top.res.abs_8! Bool) + (top.res.abs_9! Bool) + (top.res.abs_10! Bool) + (top.res.inst_3! Bool) + (top.res.inst_2! Bool) + (top.res.inst_1! Bool) + (top.res.inst_0! Bool) + + ) Bool + + (let + ((X1 Bool top.res.abs_10!)) + (let + ((X2 Int top.res.abs_4!)) + (and + (= top.usr.OK! (=> X1 (< X2 4))) + (__node_trans_voiture_0 + top.usr.m! + top.usr.s! + top.res.abs_0! + top.res.abs_1! + top.res.abs_2! + top.res.abs_3! + top.res.abs_4! + top.res.abs_5! + top.res.abs_6! + top.res.abs_7! + top.res.abs_8! + top.res.inst_3! + top.res.inst_2! + top.usr.m + top.usr.s + top.res.abs_0 + top.res.abs_1 + top.res.abs_2 + top.res.abs_3 + top.res.abs_4 + top.res.abs_5 + top.res.abs_6 + top.res.abs_7 + top.res.abs_8 + top.res.inst_3 + top.res.inst_2) + (__node_trans_Sofar_0 + top.res.abs_9! + top.res.abs_10! + top.res.inst_1! + top.res.abs_9 + top.res.abs_10 + top.res.inst_1) + (__node_trans_excludes2_0 + top.usr.m! + top.usr.s! + top.res.abs_9! + top.res.inst_0! + top.usr.m + top.usr.s + top.res.abs_9 + top.res.inst_0) + (not top.res.init_flag!)))) +) + +(define-fun + prop ( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + ) Bool + + top.usr.OK +) + +(inv-constraint str_invariant init trans prop) + +(check-synth)