From 967747b7b279256bd9368e2d392ae71dec1bb1c1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 5 Jul 2016 15:11:28 -0500 Subject: [PATCH] Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743). --- src/options/options_handler.cpp | 32 +- src/options/options_handler.h | 2 + src/options/quantifiers_modes.h | 11 +- src/options/quantifiers_options | 4 +- .../quantifiers/inst_match_generator.cpp | 26 + src/theory/quantifiers/inst_match_generator.h | 5 + .../quantifiers/inst_strategy_e_matching.cpp | 29 +- .../quantifiers/quantifiers_rewriter.cpp | 3 + src/theory/quantifiers/trigger.cpp | 10 +- src/theory/quantifiers/trigger.h | 1 + test/regress/regress0/quantifiers/Makefile.am | 3 +- .../regress/regress0/quantifiers/bug_743.smt2 | 774 ++++++++++++++++++ 12 files changed, 885 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/quantifiers/bug_743.smt2 diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 6a5f6cd39..8cd651da5 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -369,6 +369,19 @@ min-s-all \n\ + Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\ \n\ "; +const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\ +Trigger active selection modes currently supported by the --trigger-sel option:\n\ +\n\ +all \n\ ++ Make all triggers active. \n\ +\n\ +min \n\ ++ Activate triggers with minimal ground terms.\n\ +\n\ +max \n\ ++ Activate triggers with maximal ground terms. \n\ +\n\ +"; const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ \n\ @@ -630,9 +643,7 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string } theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default") { - return theory::quantifiers::TRIGGER_SEL_DEFAULT; - } else if(optarg == "min") { + if(optarg == "default" || optarg == "min") { return theory::quantifiers::TRIGGER_SEL_MIN; } else if(optarg == "max") { return theory::quantifiers::TRIGGER_SEL_MAX; @@ -651,6 +662,21 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std:: } } +theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" || optarg == "all") { + return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL; + } else if(optarg == "min") { + return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN; + } else if(optarg == "max") { + return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX; + } else if(optarg == "help") { + puts(s_triggerActiveSelModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --trigger-active-sel: `") + + optarg + "'. Try --trigger-active-sel help."); + } +} theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "default" ) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 5db2887c0..e327b9c8e 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -94,6 +94,7 @@ public: theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); @@ -221,6 +222,7 @@ public: static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; static const std::string s_triggerSelModeHelp; + static const std::string s_triggerActiveSelModeHelp; static const std::string s_ufssModeHelp; static const std::string s_userPatModeHelp; static const std::string s_errorSelectionRulesHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 65445be17..fe76f8798 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -101,8 +101,6 @@ enum UserPatMode { }; enum TriggerSelMode { - /** default for trigger selection */ - TRIGGER_SEL_DEFAULT, /** only consider minimal terms for triggers */ TRIGGER_SEL_MIN, /** only consider maximal terms for triggers */ @@ -115,6 +113,15 @@ enum TriggerSelMode { TRIGGER_SEL_ALL, }; +enum TriggerActiveSelMode { + /** always use all triggers */ + TRIGGER_ACTIVE_SEL_ALL, + /** only use triggers with minimal # of ground terms */ + TRIGGER_ACTIVE_SEL_MIN, + /** only use triggers with maximal # of ground terms */ + TRIGGER_ACTIVE_SEL_MAX, +}; + enum CVC4_PUBLIC PrenexQuantMode { /** default : prenex quantifiers without user patterns */ PRENEX_NO_USER_PAT, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 980179378..0b5474959 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -89,8 +89,10 @@ option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations -option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode +option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_MIN :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers +option triggerActiveSelMode --trigger-active-sel CVC4::theory::quantifiers::TriggerActiveSelMode :default CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerActiveSelMode + selection mode to activate triggers option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2d3bf76f6..b3df9ca5d 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -65,6 +65,24 @@ void InstMatchGenerator::setActiveAdd(bool val){ } } +int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) { + if( Trigger::isAtomicTrigger( d_match_pattern ) ){ + Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); + unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f ); + Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl; + return ngt; + }else if( d_match_pattern.getKind()==INST_CONSTANT ){ + TypeNode tn = d_match_pattern.getType(); + unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn ); + Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl; + return ngtt; +// }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + + }else{ + return -1; + } +} + void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){ if( !d_pattern.isNull() ){ Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl; @@ -837,6 +855,14 @@ int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){ return qe->addInstantiation( q, m ) ? 1 : 0; } +int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) { + Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); + unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f ); + Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl; + return ngt; +} + + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 096774c51..65c5a1427 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -46,6 +46,8 @@ public: virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; } /** set active add */ virtual void setActiveAdd( bool val ) {} + /** get active score */ + virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; } };/* class IMGenerator */ class CandidateGenerator; @@ -116,6 +118,7 @@ public: bool d_active_add; void setActiveAdd( bool val ); + int getActiveScore( QuantifiersEngine * qe ); static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ); static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); @@ -239,6 +242,8 @@ public: int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t, possibly add instantiations */ int addTerm( Node q, Node t, QuantifiersEngine* qe ); + /** get active score */ + int getActiveScore( QuantifiersEngine * qe ); };/* class InstMatchGeneratorSimple */ } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index efd765c86..49e0a698f 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -149,11 +149,7 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){ //how to select trigger terms - if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){ - d_tr_strategy = quantifiers::TRIGGER_SEL_MIN; - }else{ - d_tr_strategy = options::triggerSelMode(); - } + d_tr_strategy = options::triggerSelMode(); //whether to select new triggers during the search if( options::incrementTriggers() ){ d_regenerate_frequency = 3; @@ -211,6 +207,29 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); //} + if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){ + int max_score = -1; + Trigger * max_trigger = NULL; + for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){ + int score = itt->first->getActiveScore(); + if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){ + if( score>=0 && ( scorefirst; + } + }else{ + if( score>max_score ){ + max_score = score; + max_trigger = itt->first; + } + } + d_auto_gen_trigger[0][f][itt->first] = false; + } + if( max_trigger!=NULL ){ + d_auto_gen_trigger[0][f][max_trigger] = true; + } + } + bool hasInst = false; for( unsigned r=0; r<2; r++ ){ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 68f824c57..2d56f2cdf 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -202,6 +202,9 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { } children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) ); children.push_back( body[1] ); + if( body.getNumChildren()==3 ){ + children.push_back( body[2] ); + } Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ee091919d..2faed3af0 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -386,9 +386,9 @@ bool Trigger::isCbqiKind( Kind k ) { bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; - if( n.getKind()==IFF || n.getKind()==EQUAL ){ - if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){ - t = n[0]; + if( t.getKind()==IFF || t.getKind()==EQUAL ){ + if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){ + t = t[0]; } } if( isAtomicTrigger( t ) ){ @@ -742,6 +742,10 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { } } +int Trigger::getActiveScore() { + return d_mg->getActiveScore( d_quantEngine ); +} + Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ if( nodes.empty() ){ return d_tr.empty() ? NULL : d_tr[0]; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index a3da4d398..6d7bf1f4d 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -134,6 +134,7 @@ class Trigger { } Trace(c) << " )"; } + int getActiveScore(); private: /** trigger constructor */ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes ); diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 4c657adf1..7d02af77d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -83,7 +83,8 @@ TESTS = \ partial-trigger.smt2 \ inst-max-level-segf.smt2 \ small-bug1-fixpoint-3.smt2 \ - z3.620661-no-fv-trigger.smt2 + z3.620661-no-fv-trigger.smt2 \ + bug_743.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/bug_743.smt2 b/test/regress/regress0/quantifiers/bug_743.smt2 new file mode 100644 index 000000000..4e3ee0c96 --- /dev/null +++ b/test/regress/regress0/quantifiers/bug_743.smt2 @@ -0,0 +1,774 @@ +;; produced by cvc4_14.drv ;; +(set-logic AUFBVDTNIRA) +(set-info :source |VC generated by SPARK 2014|) +(set-info :smt-lib-version 2.0) +(set-info :category industrial) +(set-info :status unsat) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +;;; SMT-LIB2: integer arithmetic +(declare-datatypes () ((tuple0 (Tuple0)))) +(declare-sort us_private 0) + +(declare-fun us_null_ext__ () us_private) + +(declare-sort us_type_of_heap 0) + +(declare-datatypes () +((us_type_of_heap__ref + (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap))))) +(declare-sort us_image 0) + +(declare-datatypes () ((int__ref (mk_int__ref (int__content Int))))) +(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool))))) +(declare-datatypes () ((real__ref (mk_real__ref (real__content Real))))) +(declare-datatypes () +((us_private__ref (mk___private__ref (us_private__content us_private))))) +(define-fun int__ref___projection ((a int__ref)) Int (int__content a)) + +(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a)) + +(define-fun real__ref___projection ((a real__ref)) Real (real__content a)) + +(define-fun us_private__ref___projection ((a us_private__ref)) us_private + (us_private__content a)) + +(declare-fun us_compatible_tags (Int Int) Bool) + +;; __compatible_tags_refl + (assert (forall ((tag Int)) (us_compatible_tags tag tag))) + +(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0)) + +(define-fun of_int ((i Int)) Bool (ite (= i 0) false true)) + +(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1))) + +(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool) + +(declare-sort integer 0) + +(define-fun in_range1 ((x Int)) Bool (and (<= (- 2147483648) x) + (<= x 2147483647))) + +(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int) + +(declare-fun to_rep (integer) Int) + +(declare-fun of_rep (Int) integer) + +(declare-fun user_eq (integer integer) Bool) + +(declare-fun dummy () integer) + +;; inversion_axiom + (assert + (forall ((x integer)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) +))) + +;; range_axiom + (assert + (forall ((x integer)) (! (in_range1 (to_rep x)) :pattern ((to_rep x)) +))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range1 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep + (of_rep x))) +))) + +(declare-datatypes () +((integer__ref (mk_integer__ref (integer__content integer))))) +(define-fun integer__ref___projection ((a integer__ref)) integer +(integer__content + a)) + +(declare-sort natural 0) + +(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2147483647))) + +(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int) + +(declare-fun to_rep1 (natural) Int) + +(declare-fun of_rep1 (Int) natural) + +(declare-fun user_eq1 (natural natural) Bool) + +(declare-fun dummy1 () natural) + +;; inversion_axiom + (assert + (forall ((x natural)) + (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) ))) + +;; range_axiom + (assert + (forall ((x natural)) (! (in_range2 (to_rep1 x)) :pattern ((to_rep1 x)) +))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range2 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1 + (of_rep1 +x))) ))) + +(declare-datatypes () +((natural__ref (mk_natural__ref (natural__content natural))))) +(define-fun natural__ref___projection ((a natural__ref)) natural +(natural__content + a)) + +(define-fun dynamic_invariant ((temp___expr_33 Int) (temp___is_init_30 +Bool) + (temp___do_constant_31 Bool) + (temp___do_toplevel_32 Bool)) Bool (=> + (or (= temp___is_init_30 true) + (<= 0 2147483647)) (in_range2 + temp___expr_33))) + +(declare-sort index 0) + +(define-fun in_range3 ((x Int)) Bool (and (<= 1 x) (<= x 100))) + +(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int) + +(declare-fun to_rep2 (index) Int) + +(declare-fun of_rep2 (Int) index) + +(declare-fun user_eq2 (index index) Bool) + +(declare-fun dummy2 () index) + +;; inversion_axiom + (assert + (forall ((x index)) + (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) ))) + +;; range_axiom + (assert + (forall ((x index)) (! (in_range3 (to_rep2 x)) :pattern ((to_rep2 x)) +))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range3 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2 + (of_rep2 +x))) ))) + +(declare-datatypes () ((index__ref (mk_index__ref (index__content +index))))) +(define-fun index__ref___projection ((a index__ref)) index (index__content +a)) + +(define-fun dynamic_invariant1 ((temp___expr_144 Int) + (temp___is_init_141 Bool) (temp___do_constant_142 Bool) + (temp___do_toplevel_143 Bool)) Bool (=> + (or (= temp___is_init_141 true) + (<= 1 100)) (in_range3 + temp___expr_144))) + +(declare-datatypes () +((map__ref (mk_map__ref (map__content (Array Int natural)))))) +(declare-fun bool_eq3 ((Array Int natural) Int Int (Array Int natural) Int + Int) Bool) + +;; T__ada_array___equal_def + (assert + (forall ((a (Array Int natural))) + (forall ((af Int)) + (forall ((al Int)) + (forall ((b (Array Int natural))) + (forall ((bf Int)) + (forall ((bl Int)) + (! (= + (and (ite (<= af al) (= (+ (- al af) 1) (+ (- bl bf) 1)) (< bl bf)) + (forall ((i Int)) + (! (=> (and (<= af i) (<= i al)) + (= (select a i) (select b (+ (- bf af) i)))) :pattern ((select a +i)) ))) + (= (bool_eq3 a af al b bf bl) true)) :pattern ((bool_eq3 a af al b bf + bl)) )))))))) + +(declare-fun slide ((Array Int natural) Int Int) (Array Int natural)) + +;; slide_eq + (assert + (forall ((a (Array Int natural))) + (forall ((first Int)) + (! (= (slide a first first) a) :pattern ((slide a first first)) )))) + +;; slide_def + (assert + (forall ((a (Array Int natural))) + (forall ((old_first Int)) + (forall ((new_first Int)) + (forall ((i Int)) + (! (= (select (slide a old_first new_first) i) (select a (- i (- +new_first old_first)))) :pattern ((select + (slide a old_first new_first) i)) )))))) + +(declare-fun concat1 ((Array Int natural) Int Int (Array Int natural) Int + Int) (Array Int natural)) + +;; concat_def + (assert + (forall ((a (Array Int natural)) (b (Array Int natural))) + (forall ((a_first Int) (a_last Int) (b_first Int) (b_last Int)) + (forall ((i Int)) + (! (and + (=> (and (<= a_first i) (<= i a_last)) + (= (select (concat1 a a_first a_last b b_first b_last) i) (select a +i))) + (=> (< a_last i) + (= (select (concat1 a a_first a_last b b_first b_last) i) (select b +(+ (- i a_last) (- b_first 1)))))) :pattern ((select + (concat1 a a_first a_last b b_first b_last) i)) ))))) + +(declare-fun singleton (natural Int) (Array Int natural)) + +;; singleton_def + (assert + (forall ((v natural)) + (forall ((i Int)) + (! (= (select (singleton v i) i) v) :pattern ((select (singleton v i) +i)) )))) + +(declare-fun compare ((Array Int natural) Int Int (Array Int natural) Int + Int) Int) + +;; compare_def + (assert + (forall ((a (Array Int natural)) (b (Array Int natural))) + (forall ((a_first Int) (a_last Int) (b_first Int) (b_last Int)) + (! (and + (= (= (compare a a_first a_last b b_first b_last) 0) + (= (bool_eq3 a a_first a_last b b_first b_last) true)) + (and + (= (< (compare a a_first a_last b b_first b_last) 0) + (exists ((i Int) (j Int)) + (and (<= i a_last) + (and (< j b_last) + (and (= (bool_eq3 a a_first i b b_first j) true) + (or (= i a_last) + (and (< i a_last) + (< (to_rep1 (select a (+ i 1))) (to_rep1 (select b (+ j 1))))))))))) + (= (< 0 (compare a a_first a_last b b_first b_last)) + (exists ((i Int) (j Int)) + (and (<= i b_last) + (and (< j a_last) + (and (= (bool_eq3 a a_first j b b_first i) true) + (or (= i b_last) + (and (< i b_last) + (< (to_rep1 (select b (+ i 1))) (to_rep1 (select a (+ j +1))))))))))))) :pattern ( + (compare a a_first a_last b b_first b_last)) )))) + +(declare-sort t 0) + +(declare-fun first (t) integer) + +(declare-fun last (t) integer) + +(declare-fun mk (Int Int) t) + +;; mk_def + (assert + (forall ((f Int) (l Int)) + (! (=> (in_range1 f) + (=> (in_range1 l) + (and (= (to_rep (first (mk f l))) f) (= (to_rep (last (mk f l))) +l)))) :pattern ( + (mk f l)) ))) + +(define-fun dynamic_property ((range_first Int) (range_last Int) (low Int) + (high Int)) Bool (and (in_range1 low) + (and (in_range1 high) + (=> (<= low high) (and (in_range3 low) (in_range3 +high)))))) + +(declare-datatypes () ((us_t (mk___t (elts (Array Int natural))(rt t))))) +(define-fun to_array ((a us_t)) (Array Int natural) (elts a)) + +(define-fun of_array ((a (Array Int natural)) (f Int) + (l Int)) us_t (mk___t a (mk f l))) + +(define-fun first1 ((a us_t)) Int (to_rep (first (rt a)))) + +(define-fun last1 ((a us_t)) Int (to_rep (last (rt a)))) + +(define-fun length ((a us_t)) Int (ite (<= (first1 a) (last1 a)) + (+ (- (last1 a) (first1 a)) 1) 0)) + +(declare-fun value__size () Int) + +(declare-fun object__size ((Array Int natural)) Int) + +(declare-fun value__component__size () Int) + +(declare-fun object__component__size ((Array Int natural)) Int) + +(declare-fun value__alignment () Int) + +(declare-fun object__alignment ((Array Int natural)) Int) + +;; value__size_axiom + (assert (<= 0 value__size)) + +;; object__size_axiom + (assert (forall ((a (Array Int natural))) (<= 0 (object__size a)))) + +;; value__component__size_axiom + (assert (<= 0 value__component__size)) + +;; object__component__size_axiom + (assert + (forall ((a (Array Int natural))) (<= 0 (object__component__size a)))) + +;; value__alignment_axiom + (assert (<= 0 value__alignment)) + +;; object__alignment_axiom + (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment a)))) + +(define-fun bool_eq4 ((x us_t) + (y us_t)) Bool (bool_eq3 (elts x) (to_rep (first (rt x))) + (to_rep (last (rt x))) (elts y) (to_rep (first (rt y))) + (to_rep (last (rt y))))) + +(declare-fun user_eq3 (us_t us_t) Bool) + +(declare-fun dummy3 () us_t) + +(declare-datatypes () +((nat_array__ref (mk_nat_array__ref (nat_array__content us_t))))) +(define-fun nat_array__ref___projection ((a nat_array__ref)) us_t +(nat_array__content + a)) + +(define-fun dynamic_invariant2 ((temp___expr_150 us_t) + (temp___is_init_147 Bool) (temp___do_constant_148 Bool) + (temp___do_toplevel_149 Bool)) Bool (=> + (not (= temp___do_constant_148 +true)) + (dynamic_property 1 100 + (first1 temp___expr_150) + (last1 temp___expr_150)))) + +(declare-fun remove_last (us_t) us_t) + +(declare-fun first2 () Int) + +(declare-fun last2 () Int) + +(define-fun dynamic_property1 ((first_int Int) (last_int Int) + (x Int)) Bool (and (<= first_int x) (<= x last_int))) + +(define-fun bool_eq5 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int) + +(declare-fun user_eq4 (integer integer) Bool) + +(declare-fun dummy4 () integer) + +(declare-datatypes () ((t15s__ref (mk_t15s__ref (t15s__content +integer))))) +(define-fun t15s__ref___projection ((a t15s__ref)) integer (t15s__content +a)) + +(declare-sort t1 0) + +(declare-fun first3 (t1) integer) + +(declare-fun last3 (t1) integer) + +(declare-fun mk1 (Int Int) t1) + +;; mk_def + (assert + (forall ((f Int) (l Int)) + (! (=> (in_range1 f) + (=> (in_range1 l) + (and (= (to_rep (first3 (mk1 f l))) f) (= (to_rep (last3 (mk1 f l))) +l)))) :pattern ( + (mk1 f l)) ))) + +(define-fun dynamic_property2 ((range_first Int) (range_last Int) (low +Int) + (high Int)) Bool (and (in_range1 low) + (and (in_range1 high) + (=> (<= low high) + (and (dynamic_property1 range_first range_last low) + (dynamic_property1 range_first range_last high)))))) + +(declare-datatypes () +((us_t1 (mk___t1 (elts1 (Array Int natural))(rt1 t1))))) +(define-fun to_array1 ((a us_t1)) (Array Int natural) (elts1 a)) + +(define-fun of_array1 ((a (Array Int natural)) (f Int) + (l Int)) us_t1 (mk___t1 a (mk1 f l))) + +(define-fun first4 ((a us_t1)) Int (to_rep (first3 (rt1 a)))) + +(define-fun last4 ((a us_t1)) Int (to_rep (last3 (rt1 a)))) + +(define-fun length1 ((a us_t1)) Int (ite (<= (first4 a) (last4 a)) + (+ (- (last4 a) (first4 a)) 1) 0)) + +(declare-fun value__size1 () Int) + +(declare-fun object__size1 ((Array Int natural)) Int) + +(declare-fun value__component__size1 () Int) + +(declare-fun object__component__size1 ((Array Int natural)) Int) + +(declare-fun value__alignment1 () Int) + +(declare-fun object__alignment1 ((Array Int natural)) Int) + +;; value__size_axiom + (assert (<= 0 value__size1)) + +;; object__size_axiom + (assert (forall ((a (Array Int natural))) (<= 0 (object__size1 a)))) + +;; value__component__size_axiom + (assert (<= 0 value__component__size1)) + +;; object__component__size_axiom + (assert + (forall ((a (Array Int natural))) (<= 0 (object__component__size1 a)))) + +;; value__alignment_axiom + (assert (<= 0 value__alignment1)) + +;; object__alignment_axiom + (assert (forall ((a (Array Int natural))) (<= 0 (object__alignment1 +a)))) + +(define-fun bool_eq6 ((x us_t1) + (y us_t1)) Bool (bool_eq3 (elts1 x) (to_rep (first3 (rt1 x))) + (to_rep (last3 (rt1 x))) (elts1 y) + (to_rep (first3 (rt1 y))) (to_rep (last3 (rt1 y))))) + +(declare-fun user_eq5 (us_t1 us_t1) Bool) + +(declare-fun dummy5 () us_t1) + +(declare-datatypes () ((t16s__ref (mk_t16s__ref (t16s__content us_t1))))) +(define-fun t16s__ref___projection ((a t16s__ref)) us_t1 (t16s__content +a)) + +;; remove_last__post_axiom + (assert + (forall ((a us_t)) + (! (=> (and (dynamic_invariant2 a true true true) (< 0 (length a))) + (dynamic_invariant2 (remove_last a) true false true)) :pattern ( + (remove_last a)) ))) + +;; remove_last__def_axiom + (assert + (forall ((a us_t)) + (! (=> (dynamic_invariant2 a true true true) + (= (remove_last a) (let ((temp___163 (let ((temp___162 (- (last1 a) +1))) + (let ((temp___161 (first1 a))) + (of_array1 (to_array a) +temp___161 + temp___162))))) + (of_array (to_array1 temp___163) (first4 +temp___163) + (last4 temp___163))))) :pattern ((remove_last a)) +))) + +(declare-fun occ (us_t Int) Int) + +(declare-sort nb_occ 0) + +(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 100))) + +(define-fun bool_eq7 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE5 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check5 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE5 (us_image) Int) + +(declare-fun to_rep3 (nb_occ) Int) + +(declare-fun of_rep3 (Int) nb_occ) + +(declare-fun user_eq6 (nb_occ nb_occ) Bool) + +(declare-fun dummy6 () nb_occ) + +;; inversion_axiom + (assert + (forall ((x nb_occ)) + (! (= (of_rep3 (to_rep3 x)) x) :pattern ((to_rep3 x)) ))) + +;; range_axiom + (assert + (forall ((x nb_occ)) (! (in_range4 (to_rep3 x)) :pattern ((to_rep3 x)) +))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range4 x) (= (to_rep3 (of_rep3 x)) x)) :pattern ((to_rep3 + (of_rep3 +x))) ))) + +(declare-datatypes () +((nb_occ__ref (mk_nb_occ__ref (nb_occ__content nb_occ))))) +(define-fun nb_occ__ref___projection ((a nb_occ__ref)) nb_occ +(nb_occ__content + a)) + +(define-fun dynamic_invariant3 ((temp___expr_155 Int) + (temp___is_init_152 Bool) (temp___do_constant_153 Bool) + (temp___do_toplevel_154 Bool)) Bool (=> + (or (= temp___is_init_152 true) + (<= 0 100)) (in_range4 + temp___expr_155))) + +(declare-fun occ_def (us_t Int) Int) + +;; occ__post_axiom + (assert + (forall ((a us_t)) + (forall ((e Int)) + (! (=> (and (dynamic_invariant2 a true true true) (in_range2 e)) + (let ((result (occ a e))) + (and (<= result (length a)) (dynamic_invariant3 result true false +true)))) :pattern ( + (occ a e)) )))) + +;; occ__def_axiom + (assert + (forall ((a us_t)) + (forall ((e Int)) + (! (=> (and (dynamic_invariant2 a true true true) (in_range2 e)) + (= (occ a e) (occ_def a e))) :pattern ((occ a e)) )))) + +(declare-fun is_set (us_t Int Int us_t) Bool) + +;; is_set__def_axiom + (assert + (forall ((a us_t) (r us_t)) + (forall ((i Int) (v Int)) + (! (= (= (is_set a i v r) true) + (and + (and (and (= (first1 r) (first1 a)) (= (last1 r) (last1 a))) + (= (to_rep1 (select (to_array r) i)) v)) + (forall ((j Int)) + (=> (and (<= (first1 a) j) (<= j (last1 a))) + (=> (not (= i j)) + (= (to_rep1 (select (to_array r) j)) (to_rep1 (select (to_array a) +j)))))))) :pattern ( + (is_set a i v r)) )))) + +(declare-fun a () us_t) + +(declare-fun attr__ATTRIBUTE_ADDRESS () Int) + +(declare-fun i () Int) + +(declare-fun attr__ATTRIBUTE_ADDRESS1 () Int) + +(declare-fun v () Int) + +(declare-fun attr__ATTRIBUTE_ADDRESS2 () Int) + +(declare-fun e () Int) + +(declare-fun attr__ATTRIBUTE_ADDRESS3 () Int) + +(declare-fun r () us_t) + +(declare-fun attr__ATTRIBUTE_ADDRESS4 () Int) + +(declare-fun b__first () integer) + +(declare-fun b__last () integer) + +(declare-fun attr__ATTRIBUTE_ADDRESS5 () Int) + +(define-fun dynamic_invariant4 ((temp___expr_15 Int) (temp___is_init_12 +Bool) + (temp___do_constant_13 Bool) + (temp___do_toplevel_14 Bool)) Bool (=> + (or (= temp___is_init_12 true) + (<= (- 2147483648) 2147483647)) + (in_range1 temp___expr_15))) + +;; occ_def__def_axiom + (assert + (forall ((a1 us_t)) + (forall ((e1 Int)) + (! (=> (and (dynamic_invariant2 a1 true true true) (in_range2 e1)) + (= (occ_def a1 e1) (ite (= (length a1) 0) 0 + (ite (= (to_rep1 (select (to_array a1) (last1 +a1))) e1) + (+ (occ_def (remove_last a1) e1) 1) + (occ_def (remove_last a1) e1))))) :pattern +((occ_def + a1 +e1)) )))) + +(declare-fun b () (Array Int natural)) + +(declare-fun perm__occ_set__b__assume () (Array Int natural)) + +(declare-fun perm__occ_set__b__assume1 () t) + +(declare-fun o () natural) + +(declare-fun o1 () Int) + +(declare-fun o2 () (Array Int natural)) + +(declare-fun o3 () (Array Int natural)) + +(declare-fun o4 () t) + +(declare-fun result () (Array Int natural)) + +(declare-fun b1 () (Array Int natural)) + +(declare-fun result1 () (Array Int natural)) + +(declare-fun b2 () (Array Int natural)) + +(define-fun o5 () us_t (mk___t o3 o4)) + +(define-fun perm__occ_set__b__assume2 () us_t (mk___t + perm__occ_set__b__assume + perm__occ_set__b__assume1)) + +;; H + (assert (dynamic_invariant2 a true false true)) + +;; H + (assert (in_range3 i)) + +;; H + (assert (in_range2 v)) + +;; H + (assert (in_range2 e)) + +;; H + (assert (dynamic_invariant2 r true false true)) + +;; H + (assert + (and (and (<= (to_rep (first (rt a))) i) (<= i (to_rep (last (rt a))))) + (= (is_set a i v r) true))) + +;; H + (assert + (and (= perm__occ_set__b__assume2 (remove_last a)) + (and (dynamic_invariant2 perm__occ_set__b__assume2 true false true) + (and (= (elts a) perm__occ_set__b__assume) + (= (mk + (to_rep + (first3 (mk1 (to_rep (first (rt a))) (- (to_rep (last (rt a))) 1)))) + (to_rep + (last3 (mk1 (to_rep (first (rt a))) (- (to_rep (last (rt a))) 1))))) + perm__occ_set__b__assume1))))) + +;; H + (assert (= (mk_map__ref result) (mk_map__ref b))) + +;; H + (assert (= b1 perm__occ_set__b__assume)) + +;; H + (assert (= (to_rep b__first) (to_rep (first +perm__occ_set__b__assume1)))) + +;; H + (assert (= (to_rep b__last) (to_rep (last perm__occ_set__b__assume1)))) + +;; H + (assert (dynamic_property 1 100 (to_rep b__first) (to_rep b__last))) + +;; H + (assert (not (= (length a) 0))) + +;; H + (assert (not (= i (to_rep (last (rt a)))))) + +;; H + (assert (= (to_rep1 o) v)) + +;; H + (assert (and (<= (to_rep b__first) i) (<= i (to_rep b__last)))) + +;; H + (assert (= o1 i)) + +;; H + (assert (= o2 (store b1 o1 o))) + +;; H + (assert (= b1 result1)) + +;; H + (assert (= b2 o2)) + +;; H + (assert + (and (= o5 (remove_last r)) + (and (dynamic_invariant2 o5 true false true) + (and (= (elts r) o3) + (= (mk + (to_rep + (first3 (mk1 (to_rep (first (rt r))) (- (to_rep (last (rt r))) 1)))) + (to_rep + (last3 (mk1 (to_rep (first (rt r))) (- (to_rep (last (rt r))) 1))))) + o4))))) + +(assert +;; WP_parameter_def + ;; File "perm.ads", line 21, characters 0-0 + (not + (= (bool_eq3 o3 (to_rep (first o4)) (to_rep (last o4)) b2 + (to_rep (first (mk (to_rep b__first) (to_rep b__last)))) + (to_rep (last (mk (to_rep b__first) (to_rep b__last))))) true))) +(check-sat) + -- 2.30.2