From f07e8a3f06feb789692ede8ad9d25a2e049af769 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 26 Apr 2015 19:26:21 +0200 Subject: [PATCH] Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions. --- src/theory/quantifiers/first_order_model.cpp | 1 + src/theory/quantifiers/full_model_check.cpp | 18 +++-- src/theory/quantifiers/fun_def_process.cpp | 15 ++-- src/theory/quantifiers/fun_def_process.h | 2 +- src/theory/quantifiers/inst_match.cpp | 11 +++ src/theory/quantifiers/inst_match.h | 1 + src/theory/quantifiers_engine.cpp | 53 ++++++++------ src/theory/rep_set.cpp | 1 + src/theory/rep_set.h | 2 + src/theory/theory_model.cpp | 12 ++-- test/regress/regress0/fmf/Makefile.am | 6 +- test/regress/regress0/fmf/fib-core.smt2 | 19 +++++ .../regress0/fmf/fore19-exp2-core.smt2 | 70 +++++++++++++++++++ .../regress0/fmf/with-ind-104-core.smt2 | 33 +++++++++ 14 files changed, 204 insertions(+), 40 deletions(-) create mode 100755 test/regress/regress0/fmf/fib-core.smt2 create mode 100755 test/regress/regress0/fmf/fore19-exp2-core.smt2 create mode 100755 test/regress/regress0/fmf/with-ind-104-core.smt2 diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 50b04123c..5cb8cf278 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -703,6 +703,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { }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 ) ); } } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 5be263254..c0a734c35 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -593,7 +593,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, 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 @@ -847,6 +847,8 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n } 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 ){ @@ -867,10 +869,11 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n 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()); @@ -1133,6 +1136,12 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ) { + Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl; + for( unsigned i=1; igetStarElement( f[0][i].getType() ); + Assert( ts.getType()==f[0][i].getType() ); cond.push_back(ts); } } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index cb379ec92..22dac2225 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -31,6 +31,7 @@ using namespace CVC4::kind; 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, bool doRewrite ) { 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 ); @@ -91,7 +93,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { 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 ); @@ -105,10 +107,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } } -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{ @@ -123,13 +126,13 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co for( unsigned i=0; i 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 ); diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 63aa1bf94..54735d4d6 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -36,7 +36,7 @@ private: //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: diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 078614509..cb969088d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -127,6 +127,17 @@ Node InstMatch::get( int i ) { return d_vals[i]; } +void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){ + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } + inst.push_back( val ); + } +} + void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8753c0bb1..21220491f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -78,6 +78,7 @@ public: 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 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8dec3898c..3fa3b2a1b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -748,24 +748,15 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ } 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; igetInstantiationConstant( 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::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; } } @@ -1075,6 +1066,23 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, 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; @@ -1093,9 +1101,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i=0 && ( r_best_score<0 || scoregetTermDatabase()->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 } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index db0524034..5580dc3d7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -26,6 +26,7 @@ void RepSet::clear(){ d_type_reps.clear(); d_type_complete.clear(); d_tmap.clear(); + d_values_to_terms.clear(); } bool RepSet::hasRep( TypeNode tn, Node n ) { diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 19bb6d3d3..4aab230e6 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -33,6 +33,8 @@ public: 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 */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 072f579be..52b018234 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -198,7 +198,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const } 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 @@ -666,7 +666,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) } } while (changed); - if (!fullModel || !unassignedAssignable) { + if (!unassignedAssignable) { break; } @@ -675,9 +675,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // 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) { @@ -730,6 +729,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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) { diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index ca3907b0b..45e174026 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -36,7 +36,11 @@ TESTS = \ 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) diff --git a/test/regress/regress0/fmf/fib-core.smt2 b/test/regress/regress0/fmf/fib-core.smt2 new file mode 100755 index 000000000..e00f19ad4 --- /dev/null +++ b/test/regress/regress0/fmf/fib-core.smt2 @@ -0,0 +1,19 @@ +; 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 diff --git a/test/regress/regress0/fmf/fore19-exp2-core.smt2 b/test/regress/regress0/fmf/fore19-exp2-core.smt2 new file mode 100755 index 000000000..9a6e1e270 --- /dev/null +++ b/test/regress/regress0/fmf/fore19-exp2-core.smt2 @@ -0,0 +1,70 @@ +(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) diff --git a/test/regress/regress0/fmf/with-ind-104-core.smt2 b/test/regress/regress0/fmf/with-ind-104-core.smt2 new file mode 100755 index 000000000..a2e3a9ed0 --- /dev/null +++ b/test/regress/regress0/fmf/with-ind-104-core.smt2 @@ -0,0 +1,33 @@ +(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 -- 2.30.2