From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Jul 2016 20:11:28 +0000 (-0500)
Subject: Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not... 
X-Git-Tag: cvc5-1.0.0~6040^2~56
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=967747b7b279256bd9368e2d392ae71dec1bb1c1;p=cvc5.git

Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).
---

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 && ( score<max_score || max_score<0 ) ){
+              max_score = score;
+              max_trigger = itt->first;
+            } 
+          }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)
+