}else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type
d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
Node c = getUsedRepresentative( cond[j] );
+ c = getRepresentative( c );
children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
}
}
types.push_back(f[0][i].getType());
}
TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
- Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" );
+ Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" );
d_quant_cond[f] = op;
}
//make sure all types are set
}
else if( n.getType().isArray() ){
//make the definition
+ bool success = false;
+ /*
Node r = fm->getRepresentative(n);
Trace("fmc-debug") << "Representative for array is " << r << std::endl;
while( r.getKind() == kind::STORE ){
success = true;
}
}
+ */
if( !success ){
- Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
- Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl;
- Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+ //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
+ //Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl;
+ //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
//can't process this array
d.reset();
d.addEntry(fm, mkCondDefault(fm, f), Node::null());
void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val ) {
+ Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl;
+ for( unsigned i=1; i<cond.size(); i++) {
+ debugPrint("fmc-if-process", cond[i], true);
+ Trace("fmc-if-process") << " ";
+ }
+ Trace("fmc-if-process") << std::endl;
if ( index==(int)dc.size() ){
Node c = mkCond(cond);
Node v = evaluateInterpreted(n, val);
cond.push_back(d_quant_cond[f]);
for (unsigned i=0; i<f[0].getNumChildren(); i++) {
Node ts = fm->getStarElement( f[0][i].getType() );
+ Assert( ts.getType()==f[0][i].getType() );
cond.push_back(ts);
}
}
void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
std::vector< int > fd_assertions;
+ std::map< int, Node > subs_head;
//first pass : find defined functions, transform quantifiers
for( unsigned i=0; i<assertions.size(); i++ ){
Node n = TermDb::getFunDefHead( assertions[i] );
subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
}
bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+ Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
Trace("fmf-fun-def") << " to " << std::endl;
Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
new_q = Rewriter::rewrite( new_q );
if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){
std::vector< Node > constraints;
Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
- Node n = simplify( assertions[i], true, true, constraints, is_fd );
+ Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd );
Assert( constraints.empty() );
if( n!=assertions[i] ){
n = Rewriter::rewrite( n );
}
}
-Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) {
+//is_fun_def 1 : top of fun-def, 2 : top of fun-def body, 0 : not top
+Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def ) {
Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
if( n.getKind()==FORALL ){
- Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def );
+ Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def );
if( c!=n[1] ){
return NodeManager::currentNM()->mkNode( FORALL, n[0], c );
}else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
Node c = n[i];
//do not process LHS of definition
- if( is_fun_def!=1 || i!=0 ){
+ if( is_fun_def!=1 || c!=hd ){
bool newHasPol;
bool newPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
//get child constraints
std::vector< Node > cconstraints;
- c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 );
+ c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, is_fun_def==1 ? 2 : 0 );
constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
}
children.push_back( c );
//defined functions to injections input -> argument elements
std::map< Node, std::vector< Node > > d_input_arg_inj;
//simplify
- Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 );
+ Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 );
//simplify term
void simplifyTerm( Node n, std::vector< Node >& constraints );
public:
return d_vals[i];
}
+void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ Node val = get( i );
+ if( val.isNull() ){
+ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
+ val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+ }
+ inst.push_back( val );
+ }
+}
+
void InstMatch::setValue( int i, TNode n ) {
d_vals[i] = n;
}
void applyRewrite();
/** get */
Node get( int i );
+ void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst );
/** set */
void setValue( int i, TNode n );
bool set( QuantifiersEngine* qe, int i, TNode n );
}
bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
- // For resource-limiting (also does a time check).
- getOutputChannel().safePoint();
-
std::vector< Node > terms;
- //make sure there are values for each variable we are instantiating
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Node val = m.get( i );
- if( val.isNull() ){
- Node ic = d_term_db->getInstantiationConstant( f, i );
- val = d_term_db->getFreeVariableForInstConstant( ic );
- Trace("inst-add-debug") << "mkComplete " << val << std::endl;
- }
- terms.push_back( val );
- }
+ m.getTerms( this, f, terms );
return addInstantiation( f, terms, mkRep, modEq, modInst );
}
bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
+ // For resource-limiting (also does a time check).
+ getOutputChannel().safePoint();
+
Assert( terms.size()==f[0].getNumChildren() );
Trace("inst-add-debug") << "Add instantiation: ";
for( unsigned i=0; i<terms.size(); i++ ){
}
Trace(c) << std::endl;
for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
- Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
+ Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
}
}
if( !options::internalReps() ){
return r;
}else{
+ if( options::finiteModelFind() ){
+ if( r.isConst() ){
+ //map back from values assigned by model, if any
+ if( d_qe->getModel() ){
+ std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
+ if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
+ r = it->second;
+ r = getRepresentative( r );
+ }else{
+ if( r.getType().isSort() ){
+ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+ }
+ }
+ }
+ }
+ }
+
if( d_int_rep.find( r )==d_int_rep.end() ){
//find best selection for representative
Node r_best;
Trace("internal-rep-select") << " } " << std::endl;
int r_best_score = -1;
for( size_t i=0; i<eqc.size(); i++ ){
- //if cbqi is active, do not choose instantiation constant terms
- if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
- int score = getRepScore( eqc[i], f, index );
+ int score = getRepScore( eqc[i], f, index );
+ if( score!=-2 ){
if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
r_best = eqc[i];
r_best_score = score;
//smaller the score, the better
int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
- int s;
- if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
+ if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
+ return -2;
+ }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
return -1;
}else if( options::instMaxLevel()!=-1 ){
//score prefer lowest instantiation level
if( n.hasAttribute(InstLevelAttribute()) ){
- s = n.getAttribute(InstLevelAttribute());
+ return n.getAttribute(InstLevelAttribute());
}else{
- s = options::instLevelInputOnly() ? -1 : 0;
+ return options::instLevelInputOnly() ? -1 : 0;
}
}else{
//score prefers earliest use of this term as a representative
- s = d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+ return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
}
- return s;
//return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
}
d_type_reps.clear();
d_type_complete.clear();
d_tmap.clear();
+ d_values_to_terms.clear();
}
bool RepSet::hasRep( TypeNode tn, Node n ) {
std::map< TypeNode, std::vector< Node > > d_type_reps;
std::map< TypeNode, bool > d_type_complete;
std::map< Node, int > d_tmap;
+ // map from values to terms they were assigned for
+ std::map< Node, Node > d_values_to_terms;
/** clear the set */
void clear();
/** has type */
}
if (!d_equalityEngine->hasTerm(n)) {
- if(n.getType().isRegExp()) {
+ if(n.getType().isRegExp()) {
ret = Rewriter::rewrite(ret);
} else {
// Unknown term - return first enumerated value for this type
}
} while (changed);
- if (!fullModel || !unassignedAssignable) {
+ if (!unassignedAssignable) {
break;
}
// different are different.
// Only make assignments on a type if:
- // 1. fullModel is true
- // 2. there are no terms that share the same base type with un-normalized representatives
- // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
+ // 1. there are no terms that share the same base type with un-normalized representatives
+ // 2. there are no terms that share teh same base type that are unevaluated evaluable terms
// Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
changed = false;
for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
Assert(!n.isNull());
constantReps[*i2] = n;
Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
+ if( !fullModel ){
+ tm->d_rep_set.d_values_to_terms[n] = (*i2);
+ }
changed = true;
noRepSet.erase(i2);
if (assignOne) {
fc-pigeonhole19.smt2 \
Hoare-z3.931718.smt \
bug0909.smt2 \
- lst-no-self-rev-exp.smt2
+ lst-no-self-rev-exp.smt2 \
+ fib-core.smt2 \
+ fore19-exp2-core.smt2 \
+ with-ind-104-core.smt2
+
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort I_fb 0)
+(declare-fun fb_arg_0_1 (I_fb) Int)
+(declare-fun fb (Int) Int)
+
+(assert (forall ((?j I_fb)) (= (fb (fb_arg_0_1 ?j)) (ite (not (>= (fb_arg_0_1 ?j) 2)) (fb_arg_0_1 ?j) (+ (fb (+ (- 1) (fb_arg_0_1 ?j))) (fb (+ (- 2) (fb_arg_0_1 ?j)))))) ) )
+
+(assert (forall ((?i I_fb)) (ite (not (>= (fb_arg_0_1 ?i) 2)) true (and (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) ) )
+
+(assert (forall ((?i I_fb)) (or (>= (fb_arg_0_1 ?i) 2) (and (not (>= (fb_arg_0_1 ?i) 2)) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) ))
+
+
+(assert (not (= (fb 5) 5)) )
+(assert (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?z) 5)) )))
+
+(check-sat)
\ No newline at end of file
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((St (Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St)))
+(Ex (Var!2291 (varID!2292 (_ BitVec 32))))
+(List!2293 (Cons!2294 (head!2295 St) (tail!2296 List!2293)) (Nil!2297))
+))
+(declare-fun error_value!2298 () Bool)
+(declare-fun error_value!2299 () List!2293)
+(declare-fun s () St)
+(declare-fun body!2242_uf_1 (St) St)
+(declare-fun step!2241_uf_2 (St) St)
+(declare-fun init!2239_uf_3 (St) St)
+(declare-fun elze!2246_uf_4 (St) St)
+(declare-fun then!2245_uf_5 (St) St)
+(declare-fun body!2237_uf_6 (St) List!2293)
+(declare-fun tail!2296_uf_7 (List!2293) List!2293)
+(declare-fun head!2295_uf_8 (List!2293) St)
+(declare-fun expr!2240_uf_9 (St) Ex)
+(declare-fun body_uf_10 (St) St)
+(declare-fun expr!2252_uf_11 (St) Ex)
+(declare-fun expr!2244_uf_12 (St) Ex)
+(declare-fun iwf (St) Bool)
+(declare-fun iwfl (List!2293) Bool)
+(declare-fun ewl (St) St)
+(declare-fun ewlList!211 (List!2293) List!2293)
+(declare-sort I_iwf 0)
+(declare-fun iwf_arg_0_13 (I_iwf) St)
+(declare-sort I_iwfl 0)
+(declare-fun iwfl_arg_0_14 (I_iwfl) List!2293)
+(declare-sort I_ewl 0)
+(declare-fun ewl_arg_0_15 (I_ewl) St)
+(declare-sort I_ewlList!211 0)
+(declare-fun ewlList!211_arg_0_16 (I_ewlList!211) List!2293)
+(declare-fun termITE_17 () St)
+(declare-fun termITE_18 () St)
+(declare-fun termITE_19 () St)
+(declare-fun termITE_20 () St)
+
+(assert
+(and
+(forall ((?i1 I_ewl)) (= (ewl (ewl_arg_0_15 ?i1))
+
+(ite (is-IfTE (ewl_arg_0_15 ?i1)) (IfTE (ite (is-IfTE (ewl_arg_0_15 ?i1)) (expr!2244 (ewl_arg_0_15 ?i1)) (expr!2244_uf_12 (ewl_arg_0_15 ?i1))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (then!2245 (ewl_arg_0_15 ?i1)) (then!2245_uf_5 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (elze!2246 (ewl_arg_0_15 ?i1)) (elze!2246_uf_4 (ewl_arg_0_15 ?i1)))))
+
+(ite (is-While (ewl_arg_0_15 ?i1)) (For!2238 Skip!2250 (ite (is-While (ewl_arg_0_15 ?i1)) (expr!2252 (ewl_arg_0_15 ?i1)) (expr!2252_uf_11 (ewl_arg_0_15 ?i1))) Skip!2250 (ewl (ite (is-While (ewl_arg_0_15 ?i1)) (body (ewl_arg_0_15 ?i1)) (body_uf_10 (ewl_arg_0_15 ?i1)))))
+
+(ite (is-For!2238 (ewl_arg_0_15 ?i1)) (For!2238 (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (init!2239 (ewl_arg_0_15 ?i1)) (init!2239_uf_3 (ewl_arg_0_15 ?i1)))) (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (expr!2240 (ewl_arg_0_15 ?i1)) (expr!2240_uf_9 (ewl_arg_0_15 ?i1))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (step!2241 (ewl_arg_0_15 ?i1)) (step!2241_uf_2 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (body!2242 (ewl_arg_0_15 ?i1)) (body!2242_uf_1 (ewl_arg_0_15 ?i1)))))
+
+(ewl_arg_0_15 ?i1))))) )
+
+
+(forall ((?i2 I_ewl)) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (then!2245 (ewl_arg_0_15 ?i2)) (then!2245_uf_5 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (elze!2246 (ewl_arg_0_15 ?i2)) (elze!2246_uf_4 (ewl_arg_0_15 ?i2))))) ))) (ite (is-While (ewl_arg_0_15 ?i2)) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-While (ewl_arg_0_15 ?i2)) (body (ewl_arg_0_15 ?i2)) (body_uf_10 (ewl_arg_0_15 ?i2))))) )) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (init!2239 (ewl_arg_0_15 ?i2)) (init!2239_uf_3 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (step!2241 (ewl_arg_0_15 ?i2)) (step!2241_uf_2 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (body!2242 (ewl_arg_0_15 ?i2)) (body!2242_uf_1 (ewl_arg_0_15 ?i2))))) ))) true))) )
+(forall ((?i3 I_iwf)) (= (iwf (iwf_arg_0_13 ?i3)) (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (iwfl (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (body!2237 (iwf_arg_0_13 ?i3)) (body!2237_uf_6 (iwf_arg_0_13 ?i3)))) (ite (is-IfTE (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (elze!2246 (iwf_arg_0_13 ?i3)) (elze!2246_uf_4 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (then!2245 (iwf_arg_0_13 ?i3)) (then!2245_uf_5 (iwf_arg_0_13 ?i3))))) (ite (is-While (iwf_arg_0_13 ?i3)) false (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (body!2242 (iwf_arg_0_13 ?i3)) (body!2242_uf_1 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (step!2241 (iwf_arg_0_13 ?i3)) (step!2241_uf_2 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (init!2239 (iwf_arg_0_13 ?i3)) (init!2239_uf_3 (iwf_arg_0_13 ?i3))))) true))))) )
+(forall ((?i4 I_iwf)) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (not (forall ((?z I_iwfl)) (not (= (iwfl_arg_0_14 ?z) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (body!2237 (iwf_arg_0_13 ?i4)) (body!2237_uf_6 (iwf_arg_0_13 ?i4))))) )) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (elze!2246 (iwf_arg_0_13 ?i4)) (elze!2246_uf_4 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (then!2245 (iwf_arg_0_13 ?i4)) (then!2245_uf_5 (iwf_arg_0_13 ?i4))))) ))) (ite (is-While (iwf_arg_0_13 ?i4)) true (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (body!2242 (iwf_arg_0_13 ?i4)) (body!2242_uf_1 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (step!2241 (iwf_arg_0_13 ?i4)) (step!2241_uf_2 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (init!2239 (iwf_arg_0_13 ?i4)) (init!2239_uf_3 (iwf_arg_0_13 ?i4))))) ))) true)))) )
+(is-IfTE s)
+(iwf s)
+(not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) s)) ))
+(ite (is-IfTE s) (= termITE_17 (then!2245 s)) (= termITE_17 (then!2245_uf_5 s)))
+(ite (is-IfTE s) (= termITE_18 (then!2245 s)) (= termITE_18 (then!2245_uf_5 s)))
+(=> (and (iwf termITE_17) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_18)) ))) (and (= (ewl termITE_17) termITE_17) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_18)) ))))
+(ite (is-IfTE s) (= termITE_19 (elze!2246 s)) (= termITE_19 (elze!2246_uf_4 s)))
+(ite (is-IfTE s) (= termITE_20 (elze!2246 s)) (= termITE_20 (elze!2246_uf_4 s)))
+(=> (and (iwf termITE_19) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_20)) ))) (and (= (ewl termITE_19) termITE_19) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_20)) ))))
+(not (= (ewl s) s))
+(not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) s)) ))
+
+
+)
+)
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Nat!2409 (succ!2410 (pred!2411 Nat!2409)) (zero!2412))
+))
+(declare-datatypes () ((Lst!2413 (cons!2414 (head!2415 Nat!2409) (tail!2416 Lst!2413)) (nil!2417))
+))
+(declare-fun error_value!2418 () Nat!2409)
+(declare-fun plus!237 (Nat!2409 Nat!2409) Nat!2409)
+(declare-fun error_value!2419 () Nat!2409)
+(declare-fun count!263 (Nat!2409 Lst!2413) Nat!2409)
+(declare-fun pred!2411_uf_1 (Nat!2409) Nat!2409)
+(declare-fun tail!2416_uf_2 (Lst!2413) Lst!2413)
+(declare-fun head!2415_uf_3 (Lst!2413) Nat!2409)
+(declare-sort I_plus!237 0)
+(set-info :notes "plus!237_arg_0_4 is op created during fun def fmf")
+(declare-fun plus!237_arg_0_4 (I_plus!237) Nat!2409)
+(set-info :notes "plus!237_arg_1_5 is op created during fun def fmf")
+(declare-fun plus!237_arg_1_5 (I_plus!237) Nat!2409)
+(declare-sort I_count!263 0)
+(set-info :notes "count!263_arg_0_6 is op created during fun def fmf")
+(declare-fun count!263_arg_0_6 (I_count!263) Nat!2409)
+(set-info :notes "count!263_arg_1_7 is op created during fun def fmf")
+(declare-fun count!263_arg_1_7 (I_count!263) Lst!2413)
+(assert
+(and
+(not (forall ((h!413 Nat!2409) (BOUND_VARIABLE_663 I_plus!237) (BOUND_VARIABLE_671 I_count!263) (BOUND_VARIABLE_679 I_count!263) (BOUND_VARIABLE_687 I_count!263) (BOUND_VARIABLE_695 I_plus!237) (BOUND_VARIABLE_703 I_count!263) (BOUND_VARIABLE_711 I_count!263) (BOUND_VARIABLE_719 I_count!263)) (or (not (= (plus!237 (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) (= (plus!237 (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_679) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_687) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_687) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_703) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_703) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_711) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_711) (count!263_arg_1_7 BOUND_VARIABLE_679))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_719) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_719) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) ))
+(forall ((?j I_plus!237)) (= (plus!237 (plus!237_arg_0_4 ?j) (plus!237_arg_1_5 ?j)) (ite (is-zero!2412 (plus!237_arg_0_4 ?j)) (plus!237_arg_1_5 ?j) (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (succ!2410 (plus!237 (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (pred!2411 (plus!237_arg_0_4 ?j)) (pred!2411_uf_1 (plus!237_arg_0_4 ?j))) (plus!237_arg_1_5 ?j))) error_value!2418))) )
+(forall ((?i I_plus!237)) (ite (is-zero!2412 (plus!237_arg_0_4 ?i)) true (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (not (forall ((?z I_plus!237)) (or (not (= (plus!237_arg_0_4 ?z) (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (pred!2411 (plus!237_arg_0_4 ?i)) (pred!2411_uf_1 (plus!237_arg_0_4 ?i))))) (not (= (plus!237_arg_1_5 ?z) (plus!237_arg_1_5 ?i)))) )) true)) )
+(forall ((?i I_count!263)) (= (count!263 (count!263_arg_0_6 ?i) (count!263_arg_1_7 ?i)) (ite (is-nil!2417 (count!263_arg_1_7 ?i)) zero!2412 (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (ite (= (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (head!2415 (count!263_arg_1_7 ?i)) (head!2415_uf_3 (count!263_arg_1_7 ?i)))) (succ!2410 (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) error_value!2419))) )
+(forall ((?j I_count!263)) (ite (is-nil!2417 (count!263_arg_1_7 ?j)) true (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (ite (= (count!263_arg_0_6 ?j) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (head!2415 (count!263_arg_1_7 ?j)) (head!2415_uf_3 (count!263_arg_1_7 ?j)))) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) )) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) ))) true)) )
+)
+)
+(check-sat)
\ No newline at end of file
projects / cvc5.git / commitdiff