std::vector<Node>& es,
unsigned index) const
{
- std::map<Node, StrategyPtInfo>::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<Node, StrategyPtInfo>::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<Node>& eis, Node e)
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<TypeNode, std::vector<Node>> extra_cons;
+ std::map<TypeNode, std::vector<Node>> exclude_cons;
+ // do not include "-", which is included by default for integers
+ exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
+ std::unordered_set<Node, NodeHashFunction> 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);
+ }
+ }
}
}
std::map<unsigned, Node> d_guq_lit;
/** Have we returned a decision in the current SAT context? */
context::CDO<bool> 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.
Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
collectTerms( q[1], extra_cons );
}
+ std::map<TypeNode, std::vector<Node>> exc_cons;
NodeManager* nm = NodeManager::currentNM();
// check which arguments are irrelevant
std::unordered_set<unsigned> arg_irrelevant;
d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
- std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ std::unordered_set<Node, NodeHashFunction> term_irlv;
// convert to term
- for (std::unordered_set<unsigned>::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
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::map<TypeNode, std::vector<Node>>& extra_cons,
+ std::map<TypeNode, std::vector<Node>>& exc_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
std::vector<CVC4::Datatype>& datatypes,
std::set<Type>& unres)
}
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<ops[i].size(); j++ ){
- datatypes[i].addSygusConstructor( ops[i][j], cnames[j], cargs[j] );
+ std::map<TypeNode, std::vector<Node>>::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] << " ";
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::map<TypeNode, std::vector<Node>>& extra_cons,
+ std::map<TypeNode, std::vector<Node>>& exclude_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
{
Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
}
std::set<Type> 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<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
/** 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.
*/
Node bvl,
const std::string& fun,
std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::map<TypeNode, std::vector<Node> >& exclude_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
/** make the default sygus datatype type corresponding to builtin type range */
static TypeNode mkSygusDefaultType(TypeNode range,
const std::string& fun)
{
std::map<TypeNode, std::vector<Node> > extra_cons;
+ std::map<TypeNode, std::vector<Node> > exclude_cons;
std::unordered_set<Node, NodeHashFunction> 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
Node bvl,
const std::string& fun,
std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::map<TypeNode, std::vector<Node> >& exclude_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
std::vector<CVC4::Datatype>& datatypes,
std::set<Type>& unres);
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 ){
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
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 \
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff