summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/smt/smt_engine.cpp5
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp22
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp11
-rw-r--r--src/theory/quantifiers/ceg_t_instantiator.cpp4
-rw-r--r--src/theory/quantifiers/sygus_grammar_cons.cpp3
-rw-r--r--src/theory/quantifiers/term_database_sygus.cpp45
-rw-r--r--src/theory/quantifiers/term_database_sygus.h63
-rw-r--r--test/regress/regress0/sygus/Makefile.am4
-rw-r--r--test/regress/regress0/sygus/real-grammar-neg.sy14
-rw-r--r--test/regress/regress0/sygus/real-si-all.sy12
-rw-r--r--test/regress/regress1/sygus/Makefile.am4
-rw-r--r--test/regress/regress1/sygus/lustre-real.sy322
-rw-r--r--test/regress/regress1/sygus/real-grammar.sy14
14 files changed, 481 insertions, 44 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f997a8923..ef20881db 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -323,7 +323,7 @@ option cbqiMinBounds --cbqi-min-bounds bool :default false
use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
-option cbqiMidpoint --cbqi-midpoint bool :default false
+option cbqiMidpoint --cbqi-midpoint bool :read-write :default false
choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
option cbqiNopt --cbqi-nopt bool :default true
non-optimal bounds for counterexample-based quantifier instantiation
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 12f822503..a007fa412 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1310,6 +1310,11 @@ void SmtEngine::setDefaults() {
{
options::ceGuidedInst.set(true);
}
+ // must use Ferrante/Rackoff for real arithmetic
+ if (!options::cbqiMidpoint.wasSetByUser())
+ {
+ options::cbqiMidpoint.set(true);
+ }
}
if(options::forceLogicString.wasSetByUser()) {
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 82766bf49..b06c96e68 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -17,7 +17,9 @@
#include "theory/datatypes/datatypes_sygus.h"
#include "expr/node_manager.h"
+#include "options/base_options.h"
#include "options/quantifiers_options.h"
+#include "printer/printer.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/quantifiers/ce_guided_conjecture.h"
@@ -255,7 +257,9 @@ void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
if( it!=d_term_to_anchor.end() ) {
d_term_to_anchor[n] = it->second;
d_term_to_anchor_conj[n] = d_term_to_anchor_conj[n[0]];
- d = d_term_to_depth[n[0]] + 1;
+ unsigned sel_weight =
+ d_tds->getSelectorWeight(n[0].getType(), n.getOperator());
+ d = d_term_to_depth[n[0]] + sel_weight;
is_top_level = computeTopLevel( tn, n[0] );
success = true;
}
@@ -757,6 +761,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl;
Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
Trace("sygus-sb-debug") << " ......rewrites to " << bvr << std::endl;
+ Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl;
unsigned sz = d_tds->getSygusTermSize( nv );
std::vector< Node > exp;
bool do_exclude = false;
@@ -854,6 +859,9 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
*/
Trace("sygus-sb-exc") << " ........exc lemma is " << lem << ", size = " << sz << std::endl;
registerSymBreakLemma( tn, lem, sz, a, lemmas );
+ Trace("dt-sygus")
+ << " ...excluded by dynamic symmetry breaking, based on " << n
+ << " == " << bvr << std::endl;
return false;
}
}
@@ -1089,6 +1097,14 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
if( it->second ){
Node prog = it->first;
Node progv = d_td->getValuation().getModel()->getValue( prog );
+ if (Trace.isOn("dt-sygus"))
+ {
+ Trace("dt-sygus") << "* DT model : " << prog << " -> ";
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, progv);
+ Trace("dt-sygus") << ss.str() << std::endl;
+ }
// TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point)
if( !debugTesters( prog, progv, 0, lemmas ) ){
Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog << "." << std::endl;
@@ -1117,6 +1133,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
if( !registerSearchValue( prog, prog, progv, 0, lemmas ) ){
Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
}
+ else
+ {
+ Trace("dt-sygus") << " ...success." << std::endl;
+ }
}
}
}
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d2592c842..674e0d6b3 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -311,10 +311,13 @@ void TheoryDatatypes::check(Effort e) {
Trace("dt-split") << "*************Split for constructors on " << n << endl;
std::vector< Node > children;
if( dt.isSygus() && d_sygus_split ){
- Trace("dt-sygus") << "DtSygus : split on " << n << std::endl;
+ Trace("dt-split") << "DtSygus : split on " << n
+ << std::endl;
std::vector< Node > lemmas;
d_sygus_split->getSygusSplits( n, dt, children, lemmas );
- Trace("dt-sygus") << "Finished compute split, returned " << lemmas.size() << " lemmas." << std::endl;
+ Trace("dt-split") << "Finished compute split, returned "
+ << lemmas.size() << " lemmas."
+ << std::endl;
for( unsigned i=0; i<lemmas.size(); i++ ){
Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
doSendLemma( lemmas[i] );
@@ -501,11 +504,11 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
Trace("dt-tester") << "Done pending merges." << std::endl;
if( !d_conflict && polarity ){
if( d_sygus_sym_break ){
- Trace("dt-sygus") << "Assert tester to sygus : " << atom << std::endl;
+ Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
//Assert( !d_sygus_util->d_conflict );
std::vector< Node > lemmas;
d_sygus_sym_break->assertTester( tindex, t_arg, atom, lemmas );
- Trace("dt-sygus") << "Done assert tester to sygus." << std::endl;
+ Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
doSendLemmas( lemmas );
}
}
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 4d5affd2e..4fb31f90b 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -538,7 +538,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
Trace("cegqi-arith-bound") << std::endl;
best_used[rr] = best;
//if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict
- if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){
+ if (!options::cbqiMidpoint() || d_type.isInteger()
+ || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull()))
+ {
Node val = d_mbp_bounds[rr][best];
val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(),
d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index d6a62826f..092880047 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -580,7 +580,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
cargs.back().push_back(unres_types[i]);
cargs.back().push_back(unres_types[i]);
//type specific predicates
- if( types[i].isInteger() ){
+ if (types[i].isReal())
+ {
CVC4::Kind k = kind::LEQ;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index ed4e8a951..8b1ff37f1 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -286,9 +286,6 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
}
ret = mkGeneric( dt, i, var_count, pre );
Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl;
- ret = Rewriter::rewrite(ret);
- Trace("sygus-db-debug") << "SygusToBuiltin : After rewriting " << ret
- << std::endl;
d_sygus_to_builtin[tn][n] = ret;
}else{
Assert( isFreeVar( n ) );
@@ -409,11 +406,16 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){
if( n.getNumChildren()==0 ){
return 0;
}else{
+ Assert(n.getKind() == APPLY_CONSTRUCTOR);
unsigned sum = 0;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
sum += getSygusTermSize( n[i] );
}
- return 1+sum;
+ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+ int cindex = Datatype::indexOf(n.getOperator().toExpr());
+ Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
+ unsigned weight = dt[cindex].getWeight();
+ return weight + sum;
}
}
@@ -1246,6 +1248,36 @@ unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
}
}
+unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
+{
+ std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
+ d_sel_weight.find(tn);
+ if (itsw == d_sel_weight.end())
+ {
+ d_sel_weight[tn].clear();
+ itsw = d_sel_weight.find(tn);
+ Type t = tn.toType();
+ const Datatype& dt = static_cast<DatatypeType>(t).getDatatype();
+ Trace("sygus-db") << "Compute selector weights for " << dt.getName()
+ << std::endl;
+ for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
+ {
+ unsigned cw = dt[i].getWeight();
+ for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
+ {
+ Node csel = Node::fromExpr(dt[i].getSelectorInternal(t, j));
+ std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
+ if (its == itsw->second.end() || cw < its->second)
+ {
+ d_sel_weight[tn][csel] = cw;
+ Trace("sygus-db") << " w(" << csel << ") <= " << cw << std::endl;
+ }
+ }
+ }
+ }
+ Assert(itsw->second.find(sel) != itsw->second.end());
+ return itsw->second[sel];
+}
int TermDbSygus::getKindConsNum( TypeNode tn, Kind k ) {
Assert( isRegistered( tn ) );
@@ -1813,13 +1845,14 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
for( unsigned j=1; j<n.getNumChildren(); j++ ){
Node nc = getEagerUnfold( n[j], visited );
subs.push_back( nc );
- Assert( subs[j-1].getType()==var_list[j-1].getType() );
+ Assert(subs[j - 1].getType().isComparableTo(
+ var_list[j - 1].getType()));
}
Assert( vars.size()==subs.size() );
bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
- Assert( n.getType()==bTerm.getType() );
+ Assert(n.getType().isComparableTo(bTerm.getType()));
ret = bTerm;
}
}
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 45851c0c8..01e518eb1 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -115,33 +115,37 @@ public:
private:
void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
-private:
- // information for sygus types
- std::map<TypeNode, TypeNode> d_register; // stores sygus -> builtin type
- std::map<TypeNode, std::vector<Node> > d_var_list;
- std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
- std::map<TypeNode, std::map<Kind, int> > d_kinds;
- std::map<TypeNode, std::map<int, Node> > d_arg_const;
- std::map<TypeNode, std::map<Node, int> > d_consts;
- std::map<TypeNode, std::map<Node, int> > d_ops;
- std::map<TypeNode, std::map<int, Node> > d_arg_ops;
- std::map<TypeNode, std::vector<int> > d_id_funcs;
- std::map<TypeNode, std::vector<Node> >
- d_const_list; // sorted list of constants for type
- std::map<TypeNode, unsigned> d_const_list_pos;
- std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
- // normalized map
- std::map<TypeNode, std::map<Node, Node> > d_normalized;
- std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
- std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
- // grammar information
- // root -> type -> _
- std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
- // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
- // d_consider_const;
- // type -> cons -> _
- std::map<TypeNode, unsigned> d_min_term_size;
- std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
+
+ private:
+ // information for sygus types
+ std::map<TypeNode, TypeNode> d_register; // stores sygus -> builtin type
+ std::map<TypeNode, std::vector<Node> > d_var_list;
+ std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
+ std::map<TypeNode, std::map<Kind, int> > d_kinds;
+ std::map<TypeNode, std::map<int, Node> > d_arg_const;
+ std::map<TypeNode, std::map<Node, int> > d_consts;
+ std::map<TypeNode, std::map<Node, int> > d_ops;
+ std::map<TypeNode, std::map<int, Node> > d_arg_ops;
+ std::map<TypeNode, std::vector<int> > d_id_funcs;
+ std::map<TypeNode, std::vector<Node> >
+ d_const_list; // sorted list of constants for type
+ std::map<TypeNode, unsigned> d_const_list_pos;
+ std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
+ // normalized map
+ std::map<TypeNode, std::map<Node, Node> > d_normalized;
+ std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+ std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
+ // grammar information
+ // root -> type -> _
+ std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
+ // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
+ // d_consider_const;
+ // type -> cons -> _
+ std::map<TypeNode, unsigned> d_min_term_size;
+ std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
+ /** a cache for getSelectorWeight */
+ std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
+
public: // general sygus utilities
bool isRegistered( TypeNode tn );
// get the minimum depth of type in its parent grammar
@@ -149,7 +153,10 @@ private:
// get the minimum size for a constructor term
unsigned getMinTermSize( TypeNode tn );
unsigned getMinConsTermSize( TypeNode tn, unsigned cindex );
-public:
+ /** get the weight of the selector, where tn is the domain of sel */
+ unsigned getSelectorWeight(TypeNode tn, Node sel);
+
+ public:
TypeNode sygusToBuiltinType( TypeNode tn );
int getKindConsNum( TypeNode tn, Kind k );
int getConstConsNum( TypeNode tn, Node n );
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index b2cf8a069..dc721248c 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -76,7 +76,9 @@ TESTS = commutative.sy \
strings-template-infer-unused.sy \
strings-trivial-two-type.sy \
strings-double-rec.sy \
- hd-19-d1-prog-dup-op.sy
+ hd-19-d1-prog-dup-op.sy \
+ real-grammar-neg.sy \
+ real-si-all.sy
# sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/real-grammar-neg.sy b/test/regress/regress0/sygus/real-grammar-neg.sy
new file mode 100644
index 000000000..523c95ec2
--- /dev/null
+++ b/test/regress/regress0/sygus/real-grammar-neg.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --cegqi-si=none --no-sygus-pbe
+
+(set-logic LRA)
+
+(synth-fun f ((x Real)) Real)
+
+(declare-var x Real)
+
+(constraint (and (= (f -4) -2) (= (f -9) (/ -9 2))))
+
+(check-synth)
+
+; a solution is f = (/ x (+ 1 1))
diff --git a/test/regress/regress0/sygus/real-si-all.sy b/test/regress/regress0/sygus/real-si-all.sy
new file mode 100644
index 000000000..81f0ad22f
--- /dev/null
+++ b/test/regress/regress0/sygus/real-si-all.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic LRA)
+
+(synth-fun f ((x Real)) Real)
+
+(declare-var x Real)
+
+(constraint (and (< (/ 1500 3) (f x)) (< (f x) (/ 1507 3))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
index 190cf0f9f..b2a428bd1 100644
--- a/test/regress/regress1/sygus/Makefile.am
+++ b/test/regress/regress1/sygus/Makefile.am
@@ -28,7 +28,9 @@ TESTS = \
three.sy \
nia-max-square.sy \
MPwL_d1s3.sy \
- process-arg-invariance.sy
+ process-arg-invariance.sy \
+ real-grammar.sy \
+ lustre-real.sy
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress1/sygus/lustre-real.sy b/test/regress/regress1/sygus/lustre-real.sy
new file mode 100644
index 000000000..2ca010898
--- /dev/null
+++ b/test/regress/regress1/sygus/lustre-real.sy
@@ -0,0 +1,322 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+(set-logic LIRA)
+(define-fun
+__node_init_top_0 (
+(top.usr.onOff@0 Bool) (top.usr.decelSet@0 Bool) (top.usr.accelResume@0 Bool) (top.usr.cancel@0 Bool) (top.usr.brakePedal@0 Bool) (top.usr.carGear@0 Int) (top.usr.carSpeed@0 Real) (top.usr.validInputs@0 Bool) (top.usr.OK@0 Bool) (top.res.init_flag@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int) ) Bool
+
+(let ((X1 Int 0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@0 X3) (let ((X4 Bool false)) (let ((X5 Bool (and (and (and (and (not top.usr.cancel@0) (not top.usr.brakePedal@0)) (ite (= top.usr.carGear@0 3) true false)) (ite (>= top.usr.carSpeed@0 15.0) true false)) top.usr.validInputs@0))) (let ((X6 Bool false)) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
+(ite (<= (ite (>= 0 (ite top.usr.decelSet@0 1 0)) 0
+(ite top.usr.decelSet@0 1 0)) 20) (ite (>= 0 (ite top.usr.decelSet@0 1 0)) 0
+(ite top.usr.decelSet@0 1 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
+(ite (<= (ite (>= 0 (ite top.usr.accelResume@0 1 0)) 0
+(ite top.usr.accelResume@0 1 0)) 20) (ite (>= 0 (ite top.usr.accelResume@0 1 0)) 0
+(ite top.usr.accelResume@0 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 true) (let ((X7 Int (ite (not top.usr.onOff@0) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20
+Int (ite X19
+(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25
+Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27
+Int (ite X26
+(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not
+(= (ite (not
+(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31
+Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32
+Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not
+(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34
+Int (ite X33
+(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not
+(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38
+Int (ite X37
+(ite (= X35 7) 2 X35) X35))) (let ((X39
+Int (ite (not
+(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not
+(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41
+Int (ite X40
+(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45
+Int (ite X44
+(ite (= X42 4) 3 X42) X42))) (let ((X46
+Int (ite X44
+(ite (not (= X45 4)) 4 X45) X45))) (let ((X47
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49
+Int (ite X48
+(ite (= X46 4) 3 X46) X46))) (let ((X50
+Int (ite X48
+(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54
+Int (ite X53
+(ite (= X50 4) 3 X50) X50))) (let ((X55
+Int (ite X53
+(ite (not
+(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58
+Int (ite X57
+(ite (= X55 6) 3 X55) X55))) (let ((X59
+Int (ite X57
+(ite (not
+(= X58 4)) 4 X58) X58))) (let ((X60 Bool
+(or X57 X56))) (let ((X61 Bool
+(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62
+Int (ite X61
+(ite (= X59 5) 3 X59) X59))) (let ((X63
+Int (ite X61
+(ite (not
+(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 X2
+(ite (and (not X17) (and (>= X16 2) (<= X16
+8))) (ite (and (not X43) (and (>= X42
+3) (<= X42
+6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) top.res.init_flag@0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
+(define-fun
+__node_trans_top_0 (
+(top.usr.onOff@1 Bool) (top.usr.decelSet@1 Bool) (top.usr.accelResume@1 Bool) (top.usr.cancel@1 Bool) (top.usr.brakePedal@1 Bool) (top.usr.carGear@1 Int) (top.usr.carSpeed@1 Real) (top.usr.validInputs@1 Bool) (top.usr.OK@1 Bool) (top.res.init_flag@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 Int) (top.usr.onOff@0 Bool) (top.usr.decelSet@0 Bool) (top.usr.accelResume@0 Bool) (top.usr.cancel@0 Bool) (top.usr.brakePedal@0 Bool) (top.usr.carGear@0 Int) (top.usr.carSpeed@0 Real) (top.usr.validInputs@0 Bool) (top.usr.OK@0 Bool) (top.res.init_flag@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int) ) Bool
+
+(let ((X1
+Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK@1 X3) (let ((X4 Bool (and (not top.usr.decelSet@0) top.usr.decelSet@1))) (let ((X5 Bool (and (and (and (and (not top.usr.cancel@1) (not top.usr.brakePedal@1)) (ite (= top.usr.carGear@1 3) true false)) (ite (>= top.usr.carSpeed@1 15.0) true false)) top.usr.validInputs@1))) (let ((X6 Bool (and (not top.usr.accelResume@0) top.usr.accelResume@1))) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1
+(ite (<= (ite (>= 0
+(ite top.usr.decelSet@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 0
+(ite top.usr.decelSet@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 20) (ite (>= 0
+(ite top.usr.decelSet@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 0
+(ite top.usr.decelSet@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 1) 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1
+(ite (<= (ite (>= 0
+(ite top.usr.accelResume@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 0
+(ite top.usr.accelResume@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 20) (ite (>= 0
+(ite top.usr.accelResume@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 0
+(ite top.usr.accelResume@1
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 1) 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0
+false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0)) (let ((X7 Int (ite (not top.usr.onOff@1) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20
+Int (ite X19
+(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25
+Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27
+Int (ite X26
+(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not
+(= (ite (not
+(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31
+Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32
+Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not
+(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34
+Int (ite X33
+(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not
+(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38
+Int (ite X37
+(ite (= X35 7) 2 X35) X35))) (let ((X39
+Int (ite (not
+(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not
+(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41
+Int (ite X40
+(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45
+Int (ite X44
+(ite (= X42 4) 3 X42) X42))) (let ((X46
+Int (ite X44
+(ite (not (= X45 4)) 4 X45) X45))) (let ((X47
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49
+Int (ite X48
+(ite (= X46 4) 3 X46) X46))) (let ((X50
+Int (ite X48
+(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54
+Int (ite X53
+(ite (= X50 4) 3 X50) X50))) (let ((X55
+Int (ite X53
+(ite (not
+(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58
+Int (ite X57
+(ite (= X55 6) 3 X55) X55))) (let ((X59
+Int (ite X57
+(ite (not
+(= X58 4)) 4 X58) X58))) (let ((X60 Bool
+(or X57 X56))) (let ((X61 Bool
+(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62
+Int (ite X61
+(ite (= X59 5) 3 X59) X59))) (let ((X63
+Int (ite X61
+(ite (not
+(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 X2
+(ite (and (not X17) (and (>= X16 2) (<= X16
+8))) (ite (and (not X43) (and (>= X42
+3) (<= X42
+6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) (not top.res.init_flag@1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
+
+
+(synth-inv str_invariant(
+(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) ))
+
+(declare-primed-var top.usr.onOff Bool) (declare-primed-var top.usr.decelSet Bool) (declare-primed-var top.usr.accelResume Bool) (declare-primed-var top.usr.cancel Bool) (declare-primed-var top.usr.brakePedal Bool) (declare-primed-var top.usr.carGear Int) (declare-primed-var top.usr.carSpeed Real) (declare-primed-var top.usr.validInputs Bool) (declare-primed-var top.usr.OK Bool) (declare-primed-var top.res.init_flag Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (declare-primed-var top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (declare-primed-var top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (declare-primed-var top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int)
+(define-fun
+init (
+(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) ) Bool
+
+(let ((X1 Int 0)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK X3) (let ((X4 Bool false)) (let ((X5 Bool (and (and (and (and (not top.usr.cancel) (not top.usr.brakePedal)) (ite (= top.usr.carGear 3) true false)) (ite (>= top.usr.carSpeed 15.0) true false)) top.usr.validInputs))) (let ((X6 Bool false)) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out
+(ite (<= (ite (>= 0 (ite top.usr.decelSet 1 0)) 0
+(ite top.usr.decelSet 1 0)) 20) (ite (>= 0 (ite top.usr.decelSet 1 0)) 0
+(ite top.usr.decelSet 1 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out
+(ite (<= (ite (>= 0 (ite top.usr.accelResume 1 0)) 0
+(ite top.usr.accelResume 1 0)) 20) (ite (>= 0 (ite top.usr.accelResume 1 0)) 0
+(ite top.usr.accelResume 1 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep true) (let ((X7 Int (ite (not top.usr.onOff) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20
+Int (ite X19
+(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25
+Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27
+Int (ite X26
+(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not
+(= (ite (not
+(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31
+Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32
+Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not
+(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34
+Int (ite X33
+(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not
+(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38
+Int (ite X37
+(ite (= X35 7) 2 X35) X35))) (let ((X39
+Int (ite (not
+(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not
+(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41
+Int (ite X40
+(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45
+Int (ite X44
+(ite (= X42 4) 3 X42) X42))) (let ((X46
+Int (ite X44
+(ite (not (= X45 4)) 4 X45) X45))) (let ((X47
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49
+Int (ite X48
+(ite (= X46 4) 3 X46) X46))) (let ((X50
+Int (ite X48
+(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54
+Int (ite X53
+(ite (= X50 4) 3 X50) X50))) (let ((X55
+Int (ite X53
+(ite (not
+(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58
+Int (ite X57
+(ite (= X55 6) 3 X55) X55))) (let ((X59
+Int (ite X57
+(ite (not
+(= X58 4)) 4 X58) X58))) (let ((X60 Bool
+(or X57 X56))) (let ((X61 Bool
+(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62
+Int (ite X61
+(ite (= X59 5) 3 X59) X59))) (let ((X63
+Int (ite X61
+(ite (not
+(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep X2
+(ite (and (not X17) (and (>= X16 2) (<= X16
+8))) (ite (and (not X43) (and (>= X42
+3) (<= X42
+6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) top.res.init_flag)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
+(define-fun trans (
+
+;; Current state.
+(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int)
+;; Next state.
+(top.usr.onOff! Bool) (top.usr.decelSet! Bool) (top.usr.accelResume! Bool) (top.usr.cancel! Bool) (top.usr.brakePedal! Bool) (top.usr.carGear! Int) (top.usr.carSpeed! Real) (top.usr.validInputs! Bool) (top.usr.OK! Bool) (top.res.init_flag! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep! Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root! Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! Int)
+) Bool
+
+(let ((X1
+Int top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root)) (let ((X2 Int (ite (not (= X1 1)) 1 X1))) (let ((X3 Bool (or (= X2 1) (and (>= X2 2) (<= X2 8))))) (and (= top.usr.OK! X3) (let ((X4 Bool (and (not top.usr.decelSet) top.usr.decelSet!))) (let ((X5 Bool (and (and (and (and (not top.usr.cancel!) (not top.usr.brakePedal!)) (ite (= top.usr.carGear! 3) true false)) (ite (>= top.usr.carSpeed! 15.0) true false)) top.usr.validInputs!))) (let ((X6 Bool (and (not top.usr.accelResume) top.usr.accelResume!))) (and (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out!
+(ite (<= (ite (>= 0
+(ite top.usr.decelSet!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 0
+(ite top.usr.decelSet!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 20) (ite (>= 0
+(ite top.usr.decelSet!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 0
+(ite top.usr.decelSet!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out 1) 0)) 20)) (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out!
+(ite (<= (ite (>= 0
+(ite top.usr.accelResume!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 0
+(ite top.usr.accelResume!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 20) (ite (>= 0
+(ite top.usr.accelResume!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 0
+(ite top.usr.accelResume!
+(+ top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out 1) 0)) 20)) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep!
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___
+false top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep)) (let ((X7 Int (ite (not top.usr.onOff!) 0 1))) (let ((X8 Bool (and (and (>= X1 2) (<= X1 8)) (not (ite (not (= X7 0)) true false))))) (let ((X9 Int (ite X8 (ite (and (>= X1 2) (<= X1 8)) 0 X1) X1))) (let ((X10 Int (ite X8 (ite (not (= X9 1)) 1 X9) X9))) (let ((X11 Bool (and (= X10 1) (and (ite (not (= X7 0)) true false) (not X8))))) (let ((X12 Int (ite X11 (ite (= X10 1) 0 X10) X10))) (let ((X13 Int (ite (not (and (>= X12 2) (<= X12 8))) 2 X12))) (let ((X14 Bool (and (not (and (>= X12 2) (<= X12 8))) (and (>= X13 2) (<= X13 8))))) (let ((X15 Int (ite X14 (ite (not (= X13 7)) 7 X13) X13))) (let ((X16 Int (ite X11 X15 X12))) (let ((X17 Bool (or X11 X8))) (let ((X18 Int (ite (not X5) 0 1))) (let ((X19 Bool (and (and (>= X16 3) (<= X16 6)) (not (ite (not (= X18 0)) true false))))) (let ((X20
+Int (ite X19
+(ite (and (>= X16 3) (<= X16 6)) 2 X16) X16))) (let ((X21 Int (ite X19 (ite (not (= X20 8)) 8 X20) X20))) (let ((X22 Int (ite (not X4) 0 1))) (let ((X23 Bool (and (= X21 8) (and (and (ite (not (= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not (= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X19))))) (let ((X24 Int (ite X23 (ite (= X21 8) 2 X21) X21))) (let ((X25
+Int (ite (not (and (>= X24 3) (<= X24 6))) 3 X24))) (let ((X26 Bool (and (not (and (>= X24 3) (<= X24 6))) (and (>= X25 3) (<= X25 6))))) (let ((X27
+Int (ite X26
+(ite (not (= X25 4)) 4 X25) X25))) (let ((X28 Int (ite X23 X27 X24))) (let ((X29 Bool (or X23 X19))) (let ((X30 Bool (and (= X28 8) (and (and (ite (not
+(= (ite (not
+(= (ite (not X6) 0 1) 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X29))))) (let ((X31
+Int (ite X30 (ite (= X28 8) 2 X28) X28))) (let ((X32
+Int (ite (not (and (>= X31 3) (<= X31 6))) 3 X31))) (let ((X33 Bool (and (not
+(and (>= X31 3) (<= X31 6))) (and (>= X32 3) (<= X32 6))))) (let ((X34
+Int (ite X33
+(ite (not (= X32 4)) 4 X32) X32))) (let ((X35 Int (ite X30 X34 X31))) (let ((X36 Bool (or X30 X29))) (let ((X37 Bool (and (= X35 7) (and (and (ite (not
+(= (ite (not (= X22 1)) 0 1) 0)) true false) (ite (not
+(= (ite (not (= X18 1)) 0 1) 0)) true false)) (not X36))))) (let ((X38
+Int (ite X37
+(ite (= X35 7) 2 X35) X35))) (let ((X39
+Int (ite (not
+(and (>= X38 3) (<= X38 6))) 3 X38))) (let ((X40 Bool (and (not
+(and (>= X38 3) (<= X38 6))) (and (>= X39 3) (<= X39 6))))) (let ((X41
+Int (ite X40
+(ite (not (= X39 4)) 4 X39) X39))) (let ((X42 Int (ite X37 X41 X38))) (let ((X43 Bool (or X37 X36))) (let ((X44 Bool (and (= X42 4) (= X22 1)))) (let ((X45
+Int (ite X44
+(ite (= X42 4) 3 X42) X42))) (let ((X46
+Int (ite X44
+(ite (not (= X45 4)) 4 X45) X45))) (let ((X47
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X48 Bool (and (= X46 4) (and (= X47 1) (not X44))))) (let ((X49
+Int (ite X48
+(ite (= X46 4) 3 X46) X46))) (let ((X50
+Int (ite X48
+(ite (not (= X49 5)) 5 X49) X49))) (let ((X51 Bool (or X48 X44))) (let ((X52
+Int (ite (not
+(ite (= top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out! 20) true false)) 0 1))) (let ((X53 Bool (and (= X50 4) (and (= X52 1) (not X51))))) (let ((X54
+Int (ite X53
+(ite (= X50 4) 3 X50) X50))) (let ((X55
+Int (ite X53
+(ite (not
+(= X54 6)) 6 X54) X54))) (let ((X56 Bool (or X53 X51))) (let ((X57 Bool (and (= X55 6) (and (= X52 0) (not X56))))) (let ((X58
+Int (ite X57
+(ite (= X55 6) 3 X55) X55))) (let ((X59
+Int (ite X57
+(ite (not
+(= X58 4)) 4 X58) X58))) (let ((X60 Bool
+(or X57 X56))) (let ((X61 Bool
+(and (= X59 5) (and (= X47 0) (not X60))))) (let ((X62
+Int (ite X61
+(ite (= X59 5) 3 X59) X59))) (let ((X63
+Int (ite X61
+(ite (not
+(= X62 4)) 4 X62) X62))) (and (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___! true) (= top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root!
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___!
+(ite top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep! X2
+(ite (and (not X17) (and (>= X16 2) (<= X16
+8))) (ite (and (not X43) (and (>= X42
+3) (<= X42
+6))) X63 X42) X16)) X1)) (<= 0 X47 1) (<= 0 X22 1) (<= 0 X18 1) (<= 0 X7 1) (<= 0 X52 1) (not top.res.init_flag!))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
+(define-fun
+prop (
+(top.usr.onOff Bool) (top.usr.decelSet Bool) (top.usr.accelResume Bool) (top.usr.cancel Bool) (top.usr.brakePedal Bool) (top.usr.carGear Int) (top.usr.carSpeed Real) (top.usr.validInputs Bool) (top.usr.OK Bool) (top.res.init_flag Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep Bool) (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out Int) (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out Int) ) Bool
+ top.usr.OK
+)
+(inv-constraint str_invariant init trans prop)
+(check-synth)
diff --git a/test/regress/regress1/sygus/real-grammar.sy b/test/regress/regress1/sygus/real-grammar.sy
new file mode 100644
index 000000000..c2f4ae0bc
--- /dev/null
+++ b/test/regress/regress1/sygus/real-grammar.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --cegqi-si=none
+
+(set-logic LRA)
+
+(synth-fun f ((x Real)) Real)
+
+(declare-var x Real)
+
+(constraint (and (< 0 (f x)) (< (f x) 1)))
+
+(check-synth)
+
+; any number between 0 and 1 is a solution, e.g. (f x) = (/ 1 (+ 1 1)) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback