merge with unstable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_util.py

@@ -640,7 +640,7 @@ def is_CXX_gpp():
 
 def is_clang_in_gpp_form(cc):
     version_string = subprocess.check_output([cc, '--version'])
-    return version_string.find('clang') != -1
+    return str(version_string).find('clang') != -1
 
 def is_CXX_clangpp():
     if is_compiler(CXX, 'g++'):
@@ -1198,7 +1198,7 @@ class JavaDLLComponent(Component):
                 deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile)
             out.write(deps)
             out.write('\n')
-            if IS_WINDOWS:
+            #if IS_WINDOWS:
             JAVAC = '"%s"' % JAVAC
             JAR = '"%s"' % JAR
             t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
@@ -1508,7 +1508,7 @@ def mk_config():
                 SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
                 CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
             else:
-                print "FAILED\n"
+                print("FAILED\n")
                 FOCI2 = False
         if GIT_HASH:
             CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)

scripts/update_api.py

@@ -523,7 +523,7 @@ def mk_java():
     java_native.write('  public static class LongPtr { public long value; }\n')
     java_native.write('  public static class StringPtr { public String value; }\n')
     java_native.write('  public static native void setInternalErrorHandler(long ctx);\n\n')
-    if IS_WINDOWS:
+    if IS_WINDOWS or os.uname()[0]=="CYGWIN":
         java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name)
     else:
         java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
@@ -588,6 +588,9 @@ def mk_java():
     java_wrapper = open(java_wrapperf, 'w')
     pkg_str = get_component('java').package_name.replace('.', '_')
     java_wrapper.write('// Automatically generated file\n')
+    java_wrapper.write('#ifdef _CYGWIN\n')
+    java_wrapper.write('typedef long long __int64;\n')
+    java_wrapper.write('#endif\n')
     java_wrapper.write('#include<jni.h>\n')
     java_wrapper.write('#include<stdlib.h>\n')
     java_wrapper.write('#include"z3.h"\n')

src/ast/ast_smt2_pp.cpp

@@ -478,6 +478,25 @@ class smt2_printer {
     ast_manager & m() const { return m_manager; }
     ast_manager & fm() const { return format_ns::fm(m()); }
 
+    std::string ensure_quote(symbol const& s) {
+        std::string str;
+        if (is_smt2_quoted_symbol(s))
+            str = mk_smt2_quoted_symbol(s);
+        else
+            str = s.str();
+        return str;
+    }
+
+    symbol ensure_quote_sym(symbol const& s) {
+        if (is_smt2_quoted_symbol(s)) {
+            std::string str;
+            str = mk_smt2_quoted_symbol(s);
+            return symbol(str.c_str());
+        }
+        else
+            return s;
+    }
+
     void pp_var(var * v) {
         format * f;
         if (v->get_idx() < m_var_names.size()) {
@@ -507,11 +526,7 @@ class smt2_printer {
     }
 
     format * pp_simple_attribute(char const * attr, symbol const & s) {
-        std::string str;
+        std::string str = ensure_quote(s);
-        if (is_smt2_quoted_symbol(s))
-            str = mk_smt2_quoted_symbol(s);
-        else
-            str = s.str();
         return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
     }
 
@@ -779,7 +794,7 @@ class smt2_printer {
     void register_var_names(quantifier * q) {
         unsigned num_decls = q->get_num_decls();
         for (unsigned i = 0; i < num_decls; i++) {
-            symbol name = q->get_decl_name(i);
+            symbol name = ensure_quote_sym(q->get_decl_name(i));            
             if (name.is_numerical()) {
                 unsigned idx = 1;
                 name = next_name("x", idx);
@@ -1003,6 +1018,7 @@ public:
         unsigned idx = 1;
         for (unsigned i = 0; i < num; i++) {
             symbol name = next_name(var_prefix, idx);
+            name = ensure_quote_sym(name);
             var_names.push_back(name);
             m_var_names_set.insert(name);
             m_var_names.push_back(name);

src/ast/rewriter/arith_rewriter.cpp

@@ -753,12 +753,7 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
     }
     else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
         if (is_add(arg1) || is_mul(arg1)) {
-            ptr_buffer<expr> new_args;
+            return BR_FAILED;
-            unsigned num_args = to_app(arg1)->get_num_args();
-            for (unsigned i = 0; i < num_args; i++)
-                new_args.push_back(m_util.mk_rem(to_app(arg1)->get_arg(i), arg2));
-            result = m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr());
-            return BR_REWRITE2;
         }
         else {
             if (v2.is_neg()) {

src/cmd_context/check_logic.cpp

@@ -310,6 +310,8 @@ struct check_logic::imp {
                     return false;
                 non_numeral = arg;
             }
+            if (non_numeral == 0) 
+                return true; 
             if (is_diff_var(non_numeral))
                 return true;
             if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))

src/cmd_context/pdecl.cpp

@@ -515,6 +515,25 @@ bool pdatatype_decl::has_missing_refs(symbol & missing) const {
     return false;
 }
 
+bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
+    hashtable<symbol, symbol_hash_proc, symbol_eq_proc> names;
+    ptr_vector<pconstructor_decl>::const_iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
+    for (; it != end; ++it) {
+        ptr_vector<paccessor_decl> const& acc = (*it)->m_accessors;
+        for (unsigned i = 0; i < acc.size(); ++i) {
+            symbol const& name = acc[i]->get_name();
+            if (names.contains(name)) {
+                duplicated = name;
+                return true;
+            }
+            names.insert(name);
+        }
+    }
+    return false;
+}
+
+
 bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
     ptr_vector<pconstructor_decl>::iterator it  = m_constructors.begin();
     ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();

src/cmd_context/pdecl.h

@@ -169,6 +169,7 @@ public:
 class paccessor_decl : public pdecl {
     friend class pdecl_manager;
     friend class pconstructor_decl;
+    friend class pdatatype_decl;
     symbol   m_name;
     ptype    m_type;
     paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r);
@@ -222,6 +223,7 @@ public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
     virtual void display(std::ostream & out) const;
     bool has_missing_refs(symbol & missing) const;
+    bool has_duplicate_accessors(symbol & repeated) const;
 };
 
 /**

src/duality/duality.h

@@ -25,7 +25,7 @@ Revision History:
 #include <map>
 
 // make hash_map and hash_set available
-#ifndef WIN32
+#ifndef _WINDOWS
 using namespace stl_ext;
 #endif
 
@@ -782,7 +782,7 @@ protected:
       };
 
       
-#ifdef WIN32
+#ifdef _WINDOWS
        __declspec(dllexport)
 #endif
        void FromClauses(const std::vector<Term> &clauses);
@@ -1184,7 +1184,13 @@ namespace Duality {
       hash_map<Edge *, Edge *> EdgeCloneMap;
       std::vector<expr> alit_stack;
       std::vector<unsigned> alit_stack_sizes;
-      hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
+
+      // to let us use one solver per edge
+      struct edge_solver {
+	hash_map<ast,expr> AssumptionLits;
+	uptr<solver> slvr;
+      };
+      hash_map<Edge *, edge_solver > edge_solvers;
       
 #ifdef LIMIT_STACK_WEIGHT
       struct weight_counter {
@@ -1236,19 +1242,23 @@ namespace Duality {
 
       void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
 
-      LogicSolver *SolverForEdge(Edge *edge, bool models);
+      edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms);
 
   public:
       struct scoped_solver_for_edge {
-	LogicSolver *orig_ls;
+	solver *orig_slvr;
 	RPFP_caching *rpfp;
-	scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
+	edge_solver *es;
+	scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
 	  rpfp = _rpfp;
-	  orig_ls = rpfp->ls;
+	  orig_slvr = rpfp->ls->slvr;
-	  rpfp->ls = rpfp->SolverForEdge(edge,models);
+	  es = &(rpfp->SolverForEdge(edge,models,axioms)); 
+	  rpfp->ls->slvr = es->slvr.get();
+	  rpfp->AssumptionLits.swap(es->AssumptionLits);
 	}
 	~scoped_solver_for_edge(){
-	  rpfp->ls = orig_ls;
+	  rpfp->ls->slvr = orig_slvr;
+	  rpfp->AssumptionLits.swap(es->AssumptionLits);
 	}
       };
 

src/duality/duality_rpfp.cpp

@@ -2711,10 +2711,12 @@ namespace Duality {
       const std::vector<expr> &theory = ls->get_axioms();
       for(unsigned i = 0; i < theory.size(); i++)
 	s.add(theory[i]);
-      if(s.check(lits.size(),&lits[0]) != unsat)
+      for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
+	if(s.check(lits.size(),&lits[0]) == unsat)
+	  goto is_unsat;
       throw "should be unsat";
     }
-    
+  is_unsat:
     for(unsigned i = 0; i < conjuncts.size(); ){
       std::swap(conjuncts[i],conjuncts.back());
       std::swap(lits[i],lits.back());
@@ -2747,8 +2749,20 @@ namespace Duality {
     
     // verify
     check_result res = CheckCore(lits,full_core);
-    if(res != unsat)
+    if(res != unsat){
+      // add the axioms in the off chance they are useful
+      const std::vector<expr> &theory = ls->get_axioms();
+      for(unsigned i = 0; i < theory.size(); i++)
+	GetAssumptionLits(theory[i],assumps);
+      lits = assumps; 
+      std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
+      
+      for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
+	if((res = CheckCore(lits,full_core)) == unsat)
+	  goto is_unsat;
       throw "should be unsat";
+    }
+  is_unsat:
     FilterCore(core,full_core);
     
     std::vector<expr> dummy;
@@ -2889,13 +2903,20 @@ namespace Duality {
     timer_stop("Generalize");
   }
 
-  RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){
+  RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){
-    uptr<LogicSolver> &p = edge_solvers[edge];
+    edge_solver &es = edge_solvers[edge];
+    uptr<solver> &p = es.slvr;
     if(!p.get()){
       scoped_no_proof no_proofs_please(ctx.m()); // no proofs
-      p.set(new iZ3LogicSolver(ctx,models)); // no models
+      p.set(new solver(ctx,true,models)); // no models
+      if(axioms){
+	RPFP::LogicSolver *ls = edge->owner->ls;
+	const std::vector<expr> &axs = ls->get_axioms();
+	for(unsigned i = 0; i < axs.size(); i++)
+	  p.get()->add(axs[i]);
       }
-    return p.get();
+    }
+    return es;
   }
 
 
@@ -3362,6 +3383,8 @@ namespace Duality {
       }
     }
 
+    bool some_labels = false;
+
     // create the edges
 
     for(unsigned i = 0; i < clauses.size(); i++){
@@ -3397,17 +3420,23 @@ namespace Duality {
       Term labeled = body;
       std::vector<label_struct > lbls;  // TODO: throw this away for now
       body = RemoveLabels(body,lbls);
+      if(!eq(labeled,body))
+	some_labels = true; // remember if there are labels, as we then can't do qe_lite
       // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this.
       body = body.simplify();
 
 #ifdef USE_QE_LITE
       std::set<int> idxs;
+      if(!some_labels){ // can't do qe_lite if we have to reconstruct labels
 	for(unsigned j = 0; j < Indparams.size(); j++)
 	  if(Indparams[j].is_var())
 	    idxs.insert(Indparams[j].get_index_value());
 	body = body.qe_lite(idxs,false);
+      }
       hash_map<int,hash_map<ast,Term> > sb_memo;
       body = SubstBoundRec(sb_memo,substs[i],0,body);
+      if(some_labels)
+	labeled = SubstBoundRec(sb_memo,substs[i],0,labeled);
       for(unsigned j = 0; j < Indparams.size(); j++)
 	Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
 #endif

src/duality/duality_solver.cpp

@@ -51,12 +51,17 @@ Revision History:
 // #define TOP_DOWN
 // #define EFFORT_BOUNDED_STRAT
 #define SKIP_UNDERAPPROX_NODES
-#define USE_RPFP_CLONE
 // #define KEEP_EXPANSIONS
 // #define USE_CACHING_RPFP
 // #define PROPAGATE_BEFORE_CHECK
+
+#define USE_RPFP_CLONE
 #define USE_NEW_GEN_CANDS
 
+//#define NO_PROPAGATE
+//#define NO_GENERALIZE
+//#define NO_DECISIONS
+
 namespace Duality {
 
   // TODO: must be a better place for this...
@@ -129,13 +134,11 @@ namespace Duality {
       {
 	scoped_no_proof no_proofs_please(ctx.m());
 #ifdef USE_RPFP_CLONE
-	clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one
+      clone_rpfp = new RPFP_caching(rpfp->ls);
-      clone_rpfp = new RPFP_caching(clone_ls);
       clone_rpfp->Clone(rpfp);
 #endif      
 #ifdef USE_NEW_GEN_CANDS
-      gen_cands_ls = new RPFP::iZ3LogicSolver(ctx);
+      gen_cands_rpfp = new RPFP_caching(rpfp->ls);
-      gen_cands_rpfp = new RPFP_caching(gen_cands_ls);
       gen_cands_rpfp->Clone(rpfp);
 #endif      
       }
@@ -144,20 +147,16 @@ namespace Duality {
     ~Duality(){
 #ifdef USE_RPFP_CLONE
       delete clone_rpfp;
-      delete clone_ls;
 #endif      
 #ifdef USE_NEW_GEN_CANDS
       delete gen_cands_rpfp;
-      delete gen_cands_ls;
 #endif
     }
 
 #ifdef USE_RPFP_CLONE
-    RPFP::LogicSolver *clone_ls;
     RPFP_caching *clone_rpfp;
 #endif      
 #ifdef USE_NEW_GEN_CANDS
-    RPFP::LogicSolver *gen_cands_ls;
     RPFP_caching *gen_cands_rpfp;
 #endif      
 
@@ -1255,7 +1254,7 @@ namespace Duality {
 	slvr.pop(1);
 	delete checker;
 #else
-	RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
+	RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
 	gen_cands_rpfp->Push();
 	Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
 	if(gen_cands_rpfp->Check(root) != unsat){
@@ -1940,11 +1939,15 @@ namespace Duality {
 	      for(unsigned i = 0; i < expansions.size(); i++){
 		Node *node = expansions[i];
 		tree->SolveSingleNode(top,node);
+#ifdef NO_GENERALIZE
+		node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+#else
 		if(expansions.size() == 1 && NodeTooComplicated(node))
 		  SimplifyNode(node);
 		else
 		  node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
 		Generalize(node);
+#endif
 		if(RecordUpdate(node))
 		  update_count++;
 		else
@@ -1984,7 +1987,9 @@ namespace Duality {
 	      if(stack.size() == 1)break;
 	      if(prev_level_used){
 		Node *node = stack.back().expansions[0];
+#ifndef NO_PROPAGATE
 		if(!Propagate(node)) break;
+#endif
 		if(!RecordUpdate(node)) break; // shouldn't happen!
 		RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
 		propagated = true;
@@ -2008,9 +2013,11 @@ namespace Duality {
 	    was_sat = true;
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
+#ifndef NO_DECISIONS
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
+#endif
 #if 0
 	    if(tree->slvr().check() == unsat)
 	      throw "help!";

src/duality/duality_wrapper.h

@@ -1402,7 +1402,7 @@ namespace hash_space {
 }
 
 // to make Duality::ast hashable in windows
-#ifdef WIN32 
+#ifdef _WINDOWS 
 template <> inline
 size_t stdext::hash_value<Duality::ast >(const Duality::ast& s)
 {	
@@ -1446,7 +1446,7 @@ namespace hash_space {
 }
 
 // to make Duality::func_decl hashable in windows
-#ifdef WIN32 
+#ifdef _WINDOWS 
 template <> inline
 size_t stdext::hash_value<Duality::func_decl >(const Duality::func_decl& s)
 {	

src/interp/iz3hash.h

@@ -42,7 +42,7 @@ Revision History:
 #include <ext/hash_map>
 #include <ext/hash_set>
 #else
-#ifdef WIN32
+#ifdef _WINDOWS
 #define stl_ext stdext
 #define hash_space std
 #include <hash_map>
@@ -61,7 +61,7 @@ Revision History:
 
 // stupid STL doesn't include hash function for class string
 
-#ifndef WIN32 
+#ifndef _WINDOWS 
 
 namespace stl_ext {
   template <>
@@ -86,7 +86,7 @@ namespace hash_space {
   };
 }
 
-#ifdef WIN32 
+#ifdef _WINDOWS 
 template <> inline
 size_t stdext::hash_value<std::pair<int,int> >(const std::pair<int,int>& p)
 {	// hash _Keyval to size_t value one-to-one
@@ -112,7 +112,7 @@ size_t stdext::hash_value<std::pair<T *, T *> >(const std::pair<T *, T *>& p)
 }
 #endif
 
-#ifdef WIN32
+#ifdef _WINDOWS
 
 namespace std {
     template <>
@@ -139,7 +139,7 @@ namespace std {
 #endif
 
 
-#ifndef WIN32
+#ifndef _WINDOWS
 
 #if 0
 namespace stl_ext {
@@ -155,7 +155,7 @@ namespace stl_ext {
 
 #endif
 
-#ifdef WIN32
+#ifdef _WINDOWS
 
 
 

src/interp/iz3mgr.cpp

@@ -249,6 +249,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
 
 
 void iz3mgr::show(ast t){
+  if(t.null()){
+    std::cout  << "(null)" << std::endl;
+  }
   params_ref p;
   p.set_bool("flat_assoc",false);
   std::cout  << mk_pp(t.raw(), m(), p) << std::endl;
@@ -693,10 +696,13 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
       throw "not an inequality";
     }
   }
-  Qrhs = make(Times,c,Qrhs);
+  bool pstrict = op(P) == Lt;
-  bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+  if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
-  if(pstrict && qstrict && round_off)
     Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+    qstrict = false;
+  }
+  Qrhs = make(Times,c,Qrhs);
+  bool strict = pstrict || qstrict;
   if(strict)
     P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
   else
@@ -881,3 +887,14 @@ iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
   std::vector<ast> bvs; bvs.push_back(var);
   return make_quant(quantifier,bvs,e);
 }
+
+#if 0
+void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast &e, const ast &var, std::vector<ast> &substs){
+  std::pair<ast,bool> foo(e,false);
+  std::pair<hash_map<ast,bool>::iterator,bool> bar = memo.insert(foo);
+  if(bar.second){
+    if(op(e) == 
+  }
+ 
+}
+#endif

src/interp/iz3mgr.h

@@ -127,7 +127,7 @@ namespace hash_space {
 }
 
 // to make ast_r hashable in windows
-#ifdef WIN32 
+#ifdef _WINDOWS 
 template <> inline
 size_t stdext::hash_value<ast_r >(const ast_r& s)
 {	

src/interp/iz3proof_itp.cpp

@@ -579,18 +579,36 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return is_ineq(ineq);
   }
 
+  ast destruct_cond_ineq(const ast &ineq, ast &Aproves, ast &Bproves){
+    ast res = ineq;
+    opr o = op(res);
+    if(o == And){
+      Aproves = my_and(Aproves,arg(res,0));
+      res = arg(res,1);
+      o = op(res);
+    }
+    if(o == Implies){
+      Bproves = my_and(Bproves,arg(res,0));
+      res = arg(res,1);
+    }
+    return res;
+  }
+
   ast simplify_sum(std::vector<ast> &args){
     ast Aproves = mk_true(), Bproves = mk_true();
-    ast ineq = args[0];
+    ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
     if(!is_normal_ineq(ineq)) throw cannot_simplify();
     sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
     return my_and(Aproves,my_implies(Bproves,ineq));
   }
 
   ast simplify_rotate_sum(const ast &pl, const ast &pf){
-    ast cond = mk_true();
+    ast Aproves = mk_true(), Bproves = mk_true();
     ast ineq = make(Leq,make_int("0"),make_int("0"));
-    return rotate_sum_rec(pl,pf,cond,ineq);
+    ineq = rotate_sum_rec(pl,pf,Aproves,Bproves,ineq);
+    if(is_true(Aproves) && is_true(Bproves))
+      return ineq;
+    return my_and(Aproves,my_implies(Bproves,ineq));
   }
 
   bool is_rewrite_chain(const ast &chain){
@@ -623,7 +641,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
 
   void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
     opr o = op(ineq2);
-    if(o == Implies){
+    if(o == And){
+      sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
+      Aproves = my_and(Aproves,arg(ineq2,0));
+    }
+    else if(o == Implies){
       sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
       Bproves = my_and(Bproves,arg(ineq2,0));
     }
@@ -683,23 +705,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
   }
   
-  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
+  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Aproves, ast &Bproves, ast &ineq){
-    if(pf == pl)
+    if(pf == pl){
-      return my_implies(Bproves,simplify_ineq(ineq));
+      if(sym(ineq) == normal)
+	return ineq;
+      return simplify_ineq(ineq);
+    }
     if(op(pf) == Uninterpreted && sym(pf) == sum){
       if(arg(pf,2) == pl){
-	ast Aproves = mk_true();
 	sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
-	if(!is_true(Aproves))
-	  throw "help!";
 	ineq = idiv_ineq(ineq,arg(pf,1));
-	return my_implies(Bproves,ineq);
+	return ineq;
       }
-      ast Aproves = mk_true();
       sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
-      if(!is_true(Aproves))
+      return rotate_sum_rec(pl,arg(pf,0),Aproves,Bproves,ineq);
-	throw "help!";
-      return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
     }
     throw cannot_simplify();
   }
@@ -749,6 +768,28 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return res;
   }
 
+  ast unmixed_eq2ineq(const ast &lhs, const ast &rhs, opr comp_op, const ast &equa, ast &cond){
+    ast ineqs= chain_ineqs(comp_op,LitA,equa,lhs,rhs); // chain must be from lhs to rhs
+    cond = my_and(cond,chain_conditions(LitA,equa)); 
+    ast Bconds = z3_simplify(chain_conditions(LitB,equa)); 
+    if(is_true(Bconds) && op(ineqs) != And)
+      return my_implies(cond,ineqs);
+    if(op(ineqs) != And)
+      return my_and(Bconds,my_implies(cond,ineqs));
+    throw "help!";
+  }
+
+  ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){
+    if(is_true(equa))
+      return itp;
+     std::vector<ast> args(3);
+     args[0] = itp;
+     args[1] = make_int("1");
+     ast ineq = make(Leq,make_int(rational(0)),make_int(rational(0)));
+     args[2] = make_normal(ineq,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
+     return simplify_sum(args);
+  }
+
   ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
     if(pl == arg(pf,1)){
       ast cond = mk_true();
@@ -756,20 +797,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
       if(is_equivrel_chain(equa)){
 	ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
 	LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
-	if(lhst != LitMixed && rhst != LitMixed){
+	if(lhst != LitMixed && rhst != LitMixed)
-	  ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs
+	  return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
-	  cond = my_and(cond,chain_conditions(LitA,equa)); 
-	  ast Bconds = z3_simplify(chain_conditions(LitB,equa)); 
-	  if(is_true(Bconds) && op(ineqs) != And)
-	    return my_implies(cond,ineqs);
-	}
 	else {
-	  ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
+	  ast left, left_term, middle, right_term, right;
-	  return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
+	  left = get_left_movers(equa,lhs,middle,left_term);
+	  middle = get_right_movers(middle,rhs,right,right_term);
+	  ast itp = unmixed_eq2ineq(left_term, right_term, op(arg(neg_equality,0)), middle, cond);
+	  // itp = my_implies(cond,itp);
+	  itp = add_mixed_eq2ineq(lhs, left_term, left, itp);
+	  itp = add_mixed_eq2ineq(right_term, rhs, right, itp);
+	  return itp;
 	}
       }
     }
-    throw cannot_simplify();
+    throw "help!";
   }
 
   void reverse_modpon(std::vector<ast> &args){
@@ -836,6 +878,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast equa = sep_cond(args[0],cond);
     if(is_equivrel_chain(equa))
       return my_implies(cond,reverse_chain(equa));
+    if(is_negation_chain(equa))
+      return commute_negation_chain(equa);
     throw cannot_simplify();
   }
 
@@ -909,7 +953,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
     get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
     ast itp;
     if(is_rewrite_side(LitA,head)){
-      itp = ineq1;
+      itp = make(Leq,make_int("0"),make_int("0"));
+      linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form
+      //itp = ineq1;
       ast mc = z3_simplify(chain_side_proves(LitB,pref));
       Bproves = my_and(Bproves,mc);
     }
@@ -951,7 +997,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
   ast simplify_modpon(const std::vector<ast> &args){
     ast Aproves = mk_true(), Bproves = mk_true();
     ast chain = simplify_modpon_fwd(args,Bproves);
-    ast Q2 = sep_cond(args[2],Bproves);
+    ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
     ast interp;
     if(is_normal_ineq(Q2)){ // inequalities are special
       ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
@@ -1450,6 +1496,50 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return is_negation_chain(rest);
   }
 
+  ast commute_negation_chain(const ast &chain){
+    if(is_true(chain))
+      return chain;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    if(is_true(rest)){
+      ast old = rewrite_rhs(last);
+      if(!(op(old) == Not))
+	throw "bad negative equality chain";
+      ast equ = arg(old,0);
+      if(!is_equivrel(equ))
+	throw "bad negative equality chain";
+      last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True));
+      return chain_cons(rest,last);
+    }
+    ast pos = rewrite_pos(last);
+    if(pos == top_pos)
+      throw "bad negative equality chain";
+    int idx = pos_arg(pos);
+    if(idx != 0)
+      throw "bad negative equality chain";
+    pos = arg(pos,1);
+    if(pos == top_pos){
+      ast lhs = rewrite_lhs(last);
+      ast rhs = rewrite_rhs(last);
+      if(op(lhs) != Equal || op(rhs) != Equal)
+	throw "bad negative equality chain";
+      last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last),
+			  make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0))));
+    }
+    else {
+      idx = pos_arg(pos);
+      if(idx == 0)
+	idx = 1;
+      else if(idx == 1)
+	idx = 0;
+      else
+	throw "bad negative equality chain";
+      pos = pos_add(0,pos_add(idx,arg(pos,1)));
+      last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last));
+    }
+    return chain_cons(commute_negation_chain(rest),last);
+  }
+
   // split a rewrite chain into head and tail at last top-level rewrite
   ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){
     ast last = chain_last(chain);
@@ -1466,6 +1556,47 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return head;
   }
 
+  // split a rewrite chain into head and tail at last non-mixed term
+  ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
+    if(is_true(chain) || get_term_type(rhs) != LitMixed){
+      mid = rhs;
+      tail = mk_true();
+      return chain;
+    }
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast mm = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
+    ast res = get_right_movers(rest,mm,tail,mid);
+    tail = chain_cons(tail,last);
+    return res;
+  }
+  
+  // split a rewrite chain into head and tail at first non-mixed term
+  ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
+    if(is_true(chain)){
+      mid = lhs; 
+      if(get_term_type(lhs) != LitMixed){
+	tail = mk_true();
+	return chain;
+      }
+      return ast();
+    }
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast res = get_left_movers(rest,lhs,tail,mid);
+    if(res.null()){
+      mid = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last));
+      if(get_term_type(mid) != LitMixed){
+	tail = mk_true();
+	return chain;
+      }
+      return ast();
+    }      
+    tail = chain_cons(tail,last);
+    return res;
+  }
+
+
   struct cannot_split {};
 
   /** Split a chain of rewrites two chains, operating on positions 0 and 1.
@@ -1668,11 +1799,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
   ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
+    LitType lhst = get_term_type(lhs);
     LitType rhst = get_term_type(rhs);
-    if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
+    if(lhst == LitMixed && (rhst != LitMixed || ast_id(lhs) < ast_id(rhs)))
       return make_normal_step(lhs,rhs,proof);
-    else
+    if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs)))
       return make_normal_step(rhs,lhs,reverse_chain(proof));
+    throw "help!";
   }
 
   ast chain_side_proves(LitType side, const ast &chain){
@@ -1692,8 +1825,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast lhs2 = normal_lhs(f2);
     int id1 = ast_id(lhs1);
     int id2 = ast_id(lhs2);
-    if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
+    if(id1 < id2)
-    if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
+      return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
+    if(id2 < id1)
+      return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
     ast rhs1 = normal_rhs(f1);
     ast rhs2 = normal_rhs(f2);
     LitType t1 = get_term_type(rhs1);
@@ -1719,9 +1854,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
       Aproves = my_and(Aproves,mcB);
       ast rep = apply_rewrite_chain(rhs1,Aproof);
       new_proof = concat_rewrite_chain(pf1,Aproof);
-      new_normal = make_normal_step(rhs1,rep,new_proof);
+      new_normal = make_normal_step(lhs1,rep,new_proof);
+      ast A_normal = make_normal_step(rhs1,rep,Aproof);
+      ast res = cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves));
+      res = merge_normal_chains_rec(res,cons_normal(A_normal,make(True)),trans,Aproves,Bproves);
+      return res;
     }
-    else if(t1 == LitA && t2 == LitB)
+    else if(t1 == LitB && t2 == LitA)
       return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
     else if(t1 == LitA) {
       ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
@@ -1743,17 +1882,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
       return chain;
     ast f = normal_first(chain);
     ast r = normal_rest(chain);
+    r = trans_normal_chain(r,trans);
     ast rhs = normal_rhs(f);
     hash_map<ast,ast>::iterator it = trans.find(rhs);
     ast new_normal;
-    if(it != trans.end()){
+    if(it != trans.end() && get_term_type(normal_lhs(f)) == LitMixed){
       const ast &f2 = it->second;
       ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
       new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
     }
     else
       new_normal = f;
-    return cons_normal(new_normal,trans_normal_chain(r,trans));
+    if(get_term_type(normal_lhs(f)) == LitMixed)
+      trans[normal_lhs(f)] = new_normal;
+    return cons_normal(new_normal,r);
   }
 
   ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){
@@ -2011,8 +2153,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
   /** Make a Reflexivity node. This rule produces |- x = x */
   
   virtual node make_reflexivity(ast con){
-    throw proof_error();
+    if(get_term_type(con) == LitA)
-}
+      return mk_false();
+    if(get_term_type(con) == LitB)
+      return mk_true();
+    ast itp = make(And,make(contra,no_proof,mk_false()),
+		   make(contra,mk_true(),mk_not(con)));
+    return itp;
+  }
   
   /** Make a Symmetry node. This takes a derivation of |- x = y and
       produces | y = x. Ditto for ~(x=y) */
@@ -2247,10 +2395,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	throw proof_error();
       }
     }
-    Qrhs = make(Times,c,Qrhs);
+#if 0
     bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
     if(pstrict && qstrict && round_off)
       Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+#else
+    bool pstrict = op(P) == Lt;
+    if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
+      Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+      qstrict = false;
+    }
+    Qrhs = make(Times,c,Qrhs);
+    bool strict = pstrict || qstrict;
+#endif
     if(strict)
       P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
     else
@@ -2269,8 +2426,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
       itp =  mk_true();
       break;
     default: { // mixed equality
-      if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed)
+      if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){
-	std::cerr << "WARNING: mixed term in leq2eq\n"; 
+	// std::cerr << "WARNING: mixed term in leq2eq\n"; 
+	std::vector<ast> lits;
+	lits.push_back(con);
+	lits.push_back(make(Not,xleqy));
+	lits.push_back(make(Not,yleqx));
+	return make_axiom(lits);
+      }
       std::vector<ast> conjs; conjs.resize(3);
       conjs[0] = mk_not(con);
       conjs[1] = xleqy;
@@ -2405,7 +2568,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	    frng = srng; // this term will be localized
 	}
 	else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
-	  frng = erng; // this term will be localized
+	  // std::cout << "WARNING: non-local arithmetic\n";
+	  //	  frng = erng; // this term will be localized
+	}
+	else if(o == Select){ // treat the array term like a function symbol
+	  prover::range srng = pv->ast_scope(arg(e,0)); 
+	  if(!(srng.lo > srng.hi) &&  pv->ranges_intersect(srng,rng)) // localize to desired range if possible
+	    frng = pv->range_glb(srng,rng);
+	  else
+	    frng = srng; // this term will be localized
 	}
 	std::vector<ast> largs(nargs);
 	std::vector<ast> eqs;
@@ -2434,7 +2605,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       return e; // this term occurs in range, so it's O.K.
 
     if(is_array_type(get_type(e)))
-      throw "help!";
+      std::cerr << "WARNING: array quantifier\n";
 
     // choose a frame for the constraint that is close to range
     int frame = pv->range_near(pv->ast_scope(e),rng);

src/interp/iz3translate.cpp

@@ -188,6 +188,15 @@ public:
       get_Z3_lits(con, lits);
       iproof->make_axiom(lits);
     }
+#ifdef LOCALIZATION_KLUDGE
+    else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST
+	    && get_locality_rec(prem(proof,1)) == INT_MAX){
+      std::vector<ast> lits;
+      ast con = conc(proof);
+      get_Z3_lits(con, lits);
+      iproof->make_axiom(lits);
+    }
+#endif
     else {
       unsigned nprems = num_prems(proof);
       for(unsigned i = 0; i < nprems; i++){
@@ -1271,6 +1280,84 @@ public:
     return make(Plus,args);
   }
 
+
+  ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
+    if(op(t) == Plus){
+      int nargs = num_args(t);
+      std::vector<ast> args(nargs);
+      for(int i = 0; i < nargs; i++)
+	args[i] = replace_summands_with_fresh_vars(arg(t,i),map);
+      return make(Plus,args);
+    }
+    if(op(t) == Times)
+      return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map));
+    if(map.find(t) == map.end())
+      map[t] =  mk_fresh_constant("@s",get_type(t));
+    return map[t];
+  }
+
+  ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
+    ast res = normalize_inequality(ineq);
+    ast lhs = arg(res,0);
+    lhs = replace_summands_with_fresh_vars(lhs,map);
+    res = make(op(res),SortSum(lhs),arg(res,1));
+    return res;
+  }
+
+  Iproof::node painfully_reconstruct_farkas(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
+    int nprems = prems.size();
+    std::vector<ast> pcons(nprems),npcons(nprems);
+    hash_map<ast,ast> pcon_to_pf, npcon_to_pcon, pain_map;
+    for(int i = 0; i < nprems; i++){
+      pcons[i] = conc(prems[i]);
+      npcons[i] = painfully_normalize_ineq(pcons[i],pain_map);
+      pcon_to_pf[npcons[i]] = pfs[i];
+      npcon_to_pcon[npcons[i]] = pcons[i];
+    }
+    // ast leq = make(Leq,arg(con,0),arg(con,1));
+    ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
+    pcons.push_back(mk_not(con));
+    npcons.push_back(ncon);
+    // ast assumps = make(And,pcons);
+    ast new_proof;
+    if(is_sat(npcons,new_proof))
+      throw "Proof error!";
+    pfrule dk = pr(new_proof);
+    int nnp = num_prems(new_proof);
+    std::vector<Iproof::node> my_prems;
+    std::vector<ast> farkas_coeffs, my_pcons;
+
+    if(dk == PR_TH_LEMMA 
+       && get_theory_lemma_theory(new_proof) == ArithTheory
+       && get_theory_lemma_kind(new_proof) == FarkasKind)
+      get_farkas_coeffs(new_proof,farkas_coeffs);
+    else if(dk == PR_UNIT_RESOLUTION && nnp == 2){
+      for(int i = 0; i < nprems; i++)
+	farkas_coeffs.push_back(make_int(rational(1)));
+    }
+    else
+      throw "cannot reconstruct farkas proof";
+
+    for(int i = 0; i < nnp; i++){
+      ast p = conc(prem(new_proof,i));
+      p = really_normalize_ineq(p);
+      if(pcon_to_pf.find(p) != pcon_to_pf.end()){
+	my_prems.push_back(pcon_to_pf[p]);
+	my_pcons.push_back(npcon_to_pcon[p]);
+      }
+      else if(p == ncon){
+	my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
+	my_pcons.push_back(mk_not(con));
+      }
+      else
+	throw "cannot reconstruct farkas proof";
+    }
+    Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
+    return res;
+  }
+
+
+
   ast really_normalize_ineq(const ast &ineq){
     ast res = normalize_inequality(ineq);
     res = make(op(res),SortSum(arg(res,0)),arg(res,1));
@@ -1309,7 +1396,7 @@ public:
 	farkas_coeffs.push_back(make_int(rational(1)));
     }
     else
-      throw "cannot reconstruct farkas proof";
+      return painfully_reconstruct_farkas(prems,pfs,con);
 
     for(int i = 0; i < nnp; i++){
       ast p = conc(prem(new_proof,i));
@@ -1452,10 +1539,12 @@ public:
 	lits.push_back(from_ast(con));
 
       // pattern match some idioms
-      if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) {
+      if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){
+	if(get_locality_rec(prem(proof,1)) == INT_MAX) {
 	  res = iproof->make_axiom(lits);
 	  return res;
 	}
+      }
       if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
 	Iproof::node clause = translate_main(prem(proof,0),true);
 	res = RewriteClause(clause,prem(proof,1));
@@ -1465,12 +1554,20 @@ public:
       if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
 	std::cout << "foo!\n";
 
+#if 0
       if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
 	Iproof::node clause = translate_main(prem(proof,0),true);
 	res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
 	return res;
       }
       
+      if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){
+	Iproof::node clause = translate_main(prem(proof,1),true);
+	res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast.
+	return res;
+      }
+#endif
+
       if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
 	try {
 	  res = CombineEqPropagate(proof);
@@ -1627,9 +1724,10 @@ public:
 	  break;
 	case ArrayTheory: {// nothing fancy for this
 	  ast store_array;
-	  if(!get_store_array(con,store_array))
+	  if(get_store_array(con,store_array))
-	    throw unsupported();
 	    res = iproof->make_axiom(lits,ast_scope(store_array));
+	  else
+	    res = iproof->make_axiom(lits); // for array extensionality axiom
 	  break;
 	}
 	default:
@@ -1653,6 +1751,12 @@ public:
 	res = args[0];
 	break;
       }
+      case PR_COMMUTATIVITY: {
+	ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
+	ast pf = iproof->make_reflexivity(comm_equiv);
+	res = make(commute,pf,comm_equiv);
+	break;
+      }
       default:
 	assert(0 && "translate_main: unsupported proof rule");
 	throw unsupported();

src/muz/bmc/dl_bmc_engine.cpp

@@ -1465,6 +1465,10 @@ namespace datalog {
         if (m_rules.get_num_rules() == 0) {
             return l_false;
         }
+        if (m_rules.get_predicate_rules(m_query_pred).empty()) {
+            return l_false;
+        }
+
 
         if (is_linear()) {
             if (m_ctx.get_engine() == QBMC_ENGINE) {

src/parsers/smt2/smt2parser.cpp

@@ -850,6 +850,13 @@ namespace smt2 {
             for (unsigned i = 0; i < sz; i++) {
                 pdatatype_decl * d = new_dt_decls[i];
                 SASSERT(d != 0);
+                symbol duplicated;
+                if (d->has_duplicate_accessors(duplicated)) {
+                    std::string err_msg = "invalid datatype declaration, repeated accessor identifier '";
+                    err_msg += duplicated.str();
+                    err_msg += "'";
+                    throw parser_exception(err_msg, line, pos);
+                }
                 m_ctx.insert(d);
                 if (d->get_num_params() == 0) {
                     // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors...
@@ -2070,6 +2077,7 @@ namespace smt2 {
 
         void parse_option_value() {
             switch (curr()) {
+            case scanner::BV_TOKEN:
             case scanner::INT_TOKEN:
             case scanner::FLOAT_TOKEN:
                 m_curr_cmd->set_next_arg(m_ctx, m_scanner.get_number());

src/shell/main.cpp

@@ -87,7 +87,7 @@ void display_usage() {
     std::cout << "\nResources:\n";
     // timeout and memout are now available on Linux and OSX too.
     std::cout << "  -T:timeout  set the timeout (in seconds).\n";
-    std::cout << "  -t:timeout  set the soft timeout (in seconds). It only kills the current query.\n";
+    std::cout << "  -t:timeout  set the soft timeout (in milli seconds). It only kills the current query.\n";
     std::cout << "  -memory:Megabytes  set a limit for virtual memory consumption.\n";
     // 
     std::cout << "\nOutput:\n";

src/smt/params/theory_arith_params.h

@@ -28,7 +28,6 @@ enum arith_solver_id {
     AS_ARITH,
     AS_DENSE_DIFF_LOGIC,
     AS_UTVPI,
-    AS_HORN,
     AS_OPTINF
 };
 

src/smt/smt_quantifier.cpp

@@ -441,10 +441,10 @@ namespace smt {
         virtual bool mbqi_enabled(quantifier *q) const { 
             if(!m_fparams->m_mbqi_id) return true;
             const symbol &s = q->get_qid();
-            unsigned len = strlen(m_fparams->m_mbqi_id);
+            size_t len = strlen(m_fparams->m_mbqi_id);
             if(s == symbol::null || s.is_numerical())
                 return len == 0;
-            return strncmp(s.bare_str(),m_fparams->m_mbqi_id,static_cast<unsigned>(len)) == 0;
+            return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
 	}
 
       /* Quantifier id's must begin with the prefix specified by

src/smt/smt_setup.cpp

@@ -22,7 +22,6 @@ Revision History:
 #include"theory_arith.h"
 #include"theory_dense_diff_logic.h"
 #include"theory_diff_logic.h"
-#include"theory_horn_ineq.h"
 #include"theory_utvpi.h"
 #include"theory_array.h"
 #include"theory_array_full.h"
@@ -731,12 +730,6 @@ namespace smt {
                     m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
             }
             break;
-        case AS_HORN:
-            if (m_params.m_arith_int_only)
-                m_context.register_plugin(alloc(smt::theory_ihi, m_manager));
-            else
-                m_context.register_plugin(alloc(smt::theory_rhi, m_manager));          
-            break;
         case AS_UTVPI:
             if (m_params.m_arith_int_only)
                 m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -139,22 +139,32 @@ protected:
         SASSERT(g.is_well_sorted());        
     }
 
+    struct expr_pos {
+        unsigned m_parent;
+        unsigned m_self;
+        unsigned m_idx;
+        expr*    m_expr;
+        expr_pos(unsigned p, unsigned s, unsigned i, expr* e):
+            m_parent(p), m_self(s), m_idx(i), m_expr(e)
+        {}
+        expr_pos():
+            m_parent(0), m_self(0), m_idx(0), m_expr(0)
+        {}
+    };
+
     void reduce(expr_ref& result){
         SASSERT(m.is_bool(result));
-        ptr_vector<expr> todo;
         ptr_vector<expr> names;
-        svector<bool>    is_checked;
+        svector<expr_pos> todo;
-        svector<unsigned> parent_ids, self_ids;
         expr_ref_vector fresh_vars(m), trail(m);
         expr_ref res(m), tmp(m);
-        obj_map<expr,std::pair<unsigned, expr*> > cache;        
+        obj_map<expr, expr_pos> cache;        
-        unsigned id = 1;
+        unsigned id = 1, child_id = 0;
         expr_ref n2(m), fml(m);
-        unsigned path_id = 0, self_pos = 0;
+        unsigned parent_pos = 0, self_pos = 0, self_idx = 0;
         app * a;
         unsigned sz;
-        std::pair<unsigned,expr*> path_r;
+        expr_pos path_r;
-        ptr_vector<expr> found;
         expr_ref_vector args(m);
         expr_ref n = mk_fresh(id, m.mk_bool_sort());
         trail.push_back(n);        
@@ -163,26 +173,25 @@ protected:
         tmp = m.mk_not(m.mk_iff(fml, n));
         m_solver.assert_expr(tmp);
 
-        todo.push_back(fml);
+        todo.push_back(expr_pos(0,0,0,fml));
         names.push_back(n);
-        is_checked.push_back(false);
-        parent_ids.push_back(0);
-        self_ids.push_back(0);        
         m_solver.push();
 
         while (!todo.empty() && !m_cancel) {            
             expr_ref res(m);
             args.reset();
-            expr* e = todo.back();
+            expr* e    = todo.back().m_expr;
-            unsigned pos = parent_ids.back();
+            self_pos   = todo.back().m_self;
+            parent_pos = todo.back().m_parent;
+            self_idx   = todo.back().m_idx;
             n = names.back();
-            bool checked = is_checked.back();
             
             if (cache.contains(e)) {
                 goto done;
             }
-            if (m.is_bool(e) && !checked && simplify_bool(n, res)) {
+            if (m.is_bool(e) && simplify_bool(n, res)) {
-                TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);                
+                TRACE("ctx_solver_simplify_tactic", 
+                      tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
                 goto done;
             }
             if (!is_app(e)) {
@@ -191,49 +200,31 @@ protected:
             }
             
             a = to_app(e);
-            if (!is_checked.back()) {
-                self_ids.back() = ++path_id;
-                is_checked.back() = true;
-            }
-            self_pos = self_ids.back();
             sz = a->get_num_args();            
-            
             n2 = 0;
 
-            found.reset(); // arguments already simplified.
             for (unsigned i = 0; i < sz; ++i) {
                 expr* arg = a->get_arg(i);
-                if (cache.find(arg, path_r) && !found.contains(arg)) {
+                if (cache.find(arg, path_r)) {
                     //
                     // This is a single traversal version of the context
                     // simplifier. It simplifies only the first occurrence of 
                     // a sub-term with respect to the context.
                     //
                                         
-                    found.push_back(arg);
+                    if (path_r.m_parent == self_pos && path_r.m_idx == i) {
-                    if (path_r.first == self_pos) {
+                        args.push_back(path_r.m_expr);
-                        TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";);
-                        args.push_back(path_r.second);
-                    }
-                    else if (m.is_bool(arg)) {
-                        res = local_simplify(a, n, id, i);
-                        TRACE("ctx_solver_simplify_tactic", 
-                              tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
-                        args.push_back(res);
                     }
                     else {
                         args.push_back(arg);
                     }
                 }
-                else if (!n2 && !found.contains(arg)) {                
+                else if (!n2) {
                     n2 = mk_fresh(id, m.get_sort(arg));
                     trail.push_back(n2);
-                    todo.push_back(arg);
+                    todo.push_back(expr_pos(self_pos, child_id++, i, arg));
-                    parent_ids.push_back(self_pos);
-                    self_ids.push_back(0);
                     names.push_back(n2);
                     args.push_back(n2);
-                    is_checked.push_back(false);
                 }
                 else {
                     args.push_back(arg);
@@ -251,22 +242,16 @@ protected:
         
         done:
             if (res) {
-                cache.insert(e, std::make_pair(pos, res));
+                cache.insert(e, expr_pos(parent_pos, self_pos, self_idx, res));
             }            
             
-            TRACE("ctx_solver_simplify_tactic",
-                  tout << mk_pp(e, m) << " checked: " << checked << " cached: " << mk_pp(res?res.get():e, m) << "\n";);
-            
             todo.pop_back();
-            parent_ids.pop_back();
-            self_ids.pop_back();
             names.pop_back();
-            is_checked.pop_back();
             m_solver.pop(1);
         }
         if (!m_cancel) {
             VERIFY(cache.find(fml, path_r));
-            result = path_r.second;
+            result = path_r.m_expr;
         }
     }
 
@@ -307,32 +292,6 @@ protected:
         return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m);
     }
     
-
-    expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) {
-        SASSERT(index < a->get_num_args());
-        SASSERT(m.is_bool(a->get_arg(index)));
-        expr_ref n2(m), result(m), tmp(m);
-        n2 = mk_fresh(id, m.get_sort(a->get_arg(index)));
-        ptr_buffer<expr> args;
-        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            if (i == index) {
-                args.push_back(n2);
-            }
-            else {
-                args.push_back(a->get_arg(i));
-            }
-        }
-        m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result);
-        m_solver.push();
-        tmp = m.mk_eq(result, n);
-        m_solver.assert_expr(tmp);
-        if (!simplify_bool(n2, result)) {
-            result = a->get_arg(index);
-        }
-        m_solver.pop(1);
-        return result;
-    }
-    
 };
 
 tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p) {

src/smt/theory_horn_ineq.cpp

@@ -1,236 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    theory_horn_ineq.h
-    
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2013-04-18
-
-Revision History:
-
-    The implementaton is derived from theory_diff_logic.
-
---*/
-#include "theory_horn_ineq.h"
-#include "theory_horn_ineq_def.h"
-
-namespace smt {
-
-    template class theory_horn_ineq<ihi_ext>;
-    template class theory_horn_ineq<rhi_ext>;
-
-    // similar to test_diff_logic:
-
-    horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {}
-
-    bool horn_ineq_tester::operator()(expr* e) {
-        m_todo.reset();
-        m_pols.reset();
-        pos_mark.reset();
-        neg_mark.reset();
-        m_todo.push_back(e);
-        m_pols.push_back(l_true);
-        while (!m_todo.empty()) {
-            expr* e = m_todo.back();
-            lbool  p = m_pols.back();
-            m_todo.pop_back();
-            m_pols.pop_back();
-            switch (p) {
-            case l_true:
-                if (pos_mark.is_marked(e)) {
-                    continue;
-                }
-                pos_mark.mark(e, true);
-                break;
-            case l_false:
-                if (neg_mark.is_marked(e)) {
-                    continue;
-                }
-                neg_mark.mark(e, true);
-                break;
-            case l_undef:
-                if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) {
-                    continue;
-                }
-                pos_mark.mark(e, true);
-                neg_mark.mark(e, true);
-                break;
-            }
-            if (!test_expr(p, e)) {
-                return false;
-            }
-        }
-        return true;
-    }
-
-    vector<std::pair<expr*,rational> > const& horn_ineq_tester::get_linearization() const {
-        return m_terms;
-    }
-
-    bool horn_ineq_tester::test_expr(lbool p, expr* e) {
-        expr* e1, *e2, *e3;
-        if (is_var(e)) {
-            return true;
-        }
-        if (!is_app(e)) {
-            return false;
-        }
-        app* ap = to_app(e);
-        if (m.is_and(ap) || m.is_or(ap)) {
-            for (unsigned i = 0; i < ap->get_num_args(); ++i) {
-                m_todo.push_back(ap->get_arg(i));
-                m_pols.push_back(p);
-            }
-        }
-        else if (m.is_not(e, e1)) {
-            m_todo.push_back(e);
-            m_pols.push_back(~p);
-        }
-        else if (m.is_ite(e, e1, e2, e3)) {
-            m_todo.push_back(e1);
-            m_pols.push_back(l_undef);
-            m_todo.push_back(e2);
-            m_pols.push_back(p);
-            m_todo.push_back(e3);
-            m_pols.push_back(p);
-        }
-        else if (m.is_iff(e, e1, e2)) {
-            m_todo.push_back(e1);
-            m_pols.push_back(l_undef);
-            m_todo.push_back(e2);
-            m_pols.push_back(l_undef);
-            m_todo.push_back(e2);
-        }
-        else if (m.is_implies(e, e1, e2)) {
-            m_todo.push_back(e1);
-            m_pols.push_back(~p);
-            m_todo.push_back(e2);
-            m_pols.push_back(p);
-        }
-        else if (m.is_eq(e, e1, e2)) {
-            return linearize(e1, e2) == diff;
-        }
-        else if (m.is_true(e) || m.is_false(e)) {
-            // no-op
-        }
-        else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) || 
-                 a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
-            if (p == l_false) {
-                std::swap(e2, e1);
-            }
-            classify_t cl = linearize(e1, e2);
-            switch(p) {
-            case l_undef:
-                return cl == diff;
-            case l_true:
-            case l_false:
-                return cl == horn || cl == diff;
-            }
-        }
-        else if (!is_uninterp_const(e)) {
-            return false;
-        }
-        return true;
-    }
-    
-    bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) {
-        for (unsigned i = 0; i < num_fmls; ++i) {
-            if (!(*this)(fmls[i])) {
-                return false;
-            }
-        }
-        return true;
-    }
-
-    horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) {
-        m_terms.reset();
-        m_terms.push_back(std::make_pair(e, rational(1)));
-        return linearize();
-    }
-
-    horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) {
-        m_terms.reset();
-        m_terms.push_back(std::make_pair(e1, rational(1)));
-        m_terms.push_back(std::make_pair(e2, rational(-1)));
-        return linearize();
-    }
-
-    horn_ineq_tester::classify_t horn_ineq_tester::linearize() {
-
-        m_weight.reset();
-        m_coeff_map.reset();
-
-        while (!m_terms.empty()) {
-            expr* e1, *e2;
-            rational num;
-            rational mul = m_terms.back().second;
-            expr* e = m_terms.back().first;
-            m_terms.pop_back();
-            if (a.is_add(e)) {
-                for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
-                    m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
-                }
-            }
-            else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
-                m_terms.push_back(std::make_pair(e2, mul*num));
-            }
-            else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
-                m_terms.push_back(std::make_pair(e2, mul*num));
-            }
-            else if (a.is_sub(e, e1, e2)) {
-                m_terms.push_back(std::make_pair(e1, mul));
-                m_terms.push_back(std::make_pair(e2, -mul));                
-            }
-            else if (a.is_uminus(e, e1)) {
-                m_terms.push_back(std::make_pair(e1, -mul));
-            }
-            else if (a.is_numeral(e, num)) {
-                m_weight += num*mul;
-            }
-            else if (a.is_to_real(e, e1)) {
-                m_terms.push_back(std::make_pair(e1, mul));
-            }
-            else if (!is_uninterp_const(e)) {
-                return non_horn;
-            }
-            else {
-                m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
-            }
-        }
-        unsigned num_negative = 0;
-        unsigned num_positive = 0;
-        bool is_unit_pos = true, is_unit_neg = true;
-        obj_map<expr, rational>::iterator it  = m_coeff_map.begin();
-        obj_map<expr, rational>::iterator end = m_coeff_map.end();
-        for (; it != end; ++it) {
-            rational r = it->m_value;
-            if (r.is_zero()) {
-                continue;
-            }
-            m_terms.push_back(std::make_pair(it->m_key, r));
-            if (r.is_pos()) {
-                is_unit_pos = is_unit_pos && r.is_one();
-                num_positive++;
-            }
-            else {
-                is_unit_neg = is_unit_neg && r.is_minus_one();
-                num_negative++;
-            }
-        }
-        if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) {
-            return diff;
-        }
-        if (num_positive <= 1 && is_unit_pos) {
-            return horn;
-        }
-        if (num_negative <= 1 && is_unit_neg) {
-            return co_horn;
-        }
-        return non_horn;
-    }
-
-
-}

src/smt/theory_horn_ineq.h

@@ -1,328 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    theory_horn_ineq.h
-
-Abstract:
-    
-    A*x <= weight + D*x, coefficients to A and D are non-negative, 
-    D is a diagonal matrix.
-    Coefficients to weight may have both signs.
-   
-    Label variables by weight.
-    Select inequality that is not satisfied.
-    Set delta(LHS) := 0
-    Set delta(RHS(x)) := weight(x) - b
-    Propagate weight increment through inequalities.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2013-04-18
-
-Revision History:
-
-    The implementaton is derived from theory_diff_logic.
-
---*/
-
-#ifndef _THEORY_HORN_INEQ_H_
-#define _THEORY_HORN_INEQ_H_
-
-#include"rational.h"
-#include"inf_rational.h"
-#include"inf_int_rational.h"
-#include"inf_eps_rational.h"
-#include"smt_theory.h"
-#include"arith_decl_plugin.h"
-#include"smt_justification.h"
-#include"map.h"
-#include"smt_params.h"
-#include"arith_eq_adapter.h"
-#include"smt_model_generator.h"
-#include"numeral_factory.h"
-#include"smt_clause.h"
-
-namespace smt {
-
-    class horn_ineq_tester {
-        ast_manager&      m;
-        arith_util        a;
-        ptr_vector<expr>  m_todo;
-        svector<lbool>    m_pols;
-        ast_mark pos_mark, neg_mark;
-        obj_map<expr, rational>               m_coeff_map;
-        rational                              m_weight;
-        vector<std::pair<expr*, rational> >   m_terms;
-
-    public:
-        enum classify_t {
-            co_horn,
-            horn,
-            diff,
-            non_horn
-        };
-        horn_ineq_tester(ast_manager& m);
-
-        // test if formula is in the Horn inequality fragment:
-        bool operator()(expr* fml);
-        bool operator()(unsigned num_fmls, expr* const* fmls);
-
-        // linearize inequality/equality
-        classify_t linearize(expr* e);
-        classify_t linearize(expr* e1, expr* e2);
-
-        // retrieve linearization
-        vector<std::pair<expr*,rational> > const& get_linearization() const;        
-        rational const& get_weight() const { return m_weight; }
-    private:
-        bool test_expr(lbool p, expr* e);
-        classify_t linearize();
-    };
-
-    template<typename Ext>
-    class theory_horn_ineq : public theory, private Ext {
-        
-        typedef typename Ext::numeral numeral;
-        typedef typename Ext::inf_numeral inf_numeral;
-        typedef literal explanation;
-        typedef theory_var th_var;
-        typedef svector<th_var> th_var_vector;
-        typedef unsigned clause_id;
-        typedef vector<std::pair<th_var, rational> >  coeffs;
-
-        class clause;
-        class graph;
-        class assignment_trail;
-        class parent_trail;
-
-        class atom {
-        protected:
-            bool_var m_bvar;
-            bool     m_true;
-            int      m_pos;
-            int      m_neg;
-        public:
-            atom(bool_var bv, int pos, int neg) : 
-                m_bvar(bv), m_true(false),
-                m_pos(pos), m_neg(neg) {}
-            ~atom() {}
-            bool_var get_bool_var() const { return m_bvar; }
-            bool is_true() const { return m_true; }
-            void assign_eh(bool is_true) { m_true = is_true; }
-            int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
-            int get_pos() const { return m_pos; }
-            int get_neg() const { return m_neg; }
-            std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const;
-        };
-        typedef svector<atom> atoms;
-        
-        struct scope {
-            unsigned   m_atoms_lim;
-            unsigned   m_asserted_atoms_lim;
-            unsigned   m_asserted_qhead_old;
-        };
-
-        struct stats {
-            unsigned   m_num_conflicts;
-            unsigned   m_num_assertions;
-            unsigned   m_num_core2th_eqs;
-            unsigned   m_num_core2th_diseqs;
-
-            void reset() {
-                memset(this, 0, sizeof(*this));
-            }
-
-            stats() {
-                reset();
-            }
-        };
-
-        stats                   m_stats;        
-        smt_params              m_params;
-        arith_util              a;
-        arith_eq_adapter        m_arith_eq_adapter;
-        th_var                  m_zero_int; // cache the variable representing the zero variable.
-        th_var                  m_zero_real; // cache the variable representing the zero variable.
-
-        graph*                  m_graph;
-        atoms                   m_atoms;
-        unsigned_vector         m_asserted_atoms;   // set of asserted atoms
-        unsigned                m_asserted_qhead;   
-        u_map<unsigned>         m_bool_var2atom;
-        svector<scope>          m_scopes;
-
-        double                  m_agility;
-        bool                    m_lia;
-        bool                    m_lra;
-        bool                    m_non_horn_ineq_exprs;
-
-        horn_ineq_tester        m_test;
-
-
-        arith_factory *         m_factory;
-        rational                m_delta;
-        rational                m_lambda;
-        
-
-        // Set a conflict due to a negative cycle.
-        void set_neg_cycle_conflict();
-               
-        // Create a new theory variable.
-        virtual th_var mk_var(enode* n);
-
-        virtual th_var mk_var(expr* n);
-                                
-        void compute_delta();
-
-        void found_non_horn_ineq_expr(expr * n);
-
-        bool is_interpreted(app* n) const {
-            return n->get_family_id() == get_family_id();
-        }
-
-    public:    
-        theory_horn_ineq(ast_manager& m);
-
-        virtual ~theory_horn_ineq();
-
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); }
-
-        virtual char const * get_name() const { return "horn-inequality-logic"; }
-
-        /**
-           \brief See comment in theory::mk_eq_atom
-        */
-        virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); }
-
-        virtual void init(context * ctx);
-
-        virtual bool internalize_atom(app * atom, bool gate_ctx);
-                                                     
-        virtual bool internalize_term(app * term);
-
-        virtual void internalize_eq_eh(app * atom, bool_var v);
-
-        virtual void assign_eh(bool_var v, bool is_true);
-
-        virtual void new_eq_eh(th_var v1, th_var v2) {
-            m_arith_eq_adapter.new_eq_eh(v1, v2);
-        }
-
-        virtual bool use_diseqs() const { return true; }
-
-        virtual void new_diseq_eh(th_var v1, th_var v2) {
-            m_arith_eq_adapter.new_diseq_eh(v1, v2);
-        }
-
-        virtual void push_scope_eh();
-
-        virtual void pop_scope_eh(unsigned num_scopes);
-
-        virtual void restart_eh() {
-            m_arith_eq_adapter.restart_eh();
-        }
-
-        virtual void relevant_eh(app* e) {}
-
-        virtual void init_search_eh() {
-            m_arith_eq_adapter.init_search_eh();
-        }
-
-        virtual final_check_status final_check_eh();
-
-        virtual bool is_shared(th_var v) const {
-            return false;
-        }
-    
-        virtual bool can_propagate() {
-            SASSERT(m_asserted_qhead <= m_asserted_atoms.size());
-            return m_asserted_qhead != m_asserted_atoms.size();
-        }
-        
-        virtual void propagate();
-        
-        virtual justification * why_is_diseq(th_var v1, th_var v2) {
-            UNREACHABLE();
-            return 0;
-        }
-
-        virtual void reset_eh();
-
-        virtual void init_model(model_generator & m);
-        
-        virtual model_value_proc * mk_value(enode * n, model_generator & mg);
-
-        virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const {
-            return true;
-        }
-                
-        virtual void display(std::ostream & out) const;
-        
-        virtual void collect_statistics(::statistics & st) const;
-
-    private:        
-
-        virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
-            m_stats.m_num_core2th_eqs++;
-            new_eq_or_diseq(true, v1, v2, j);
-        }
-
-        virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) {
-            m_stats.m_num_core2th_diseqs++;
-            new_eq_or_diseq(false, v1, v2, j);    
-        }
-
-        void negate(coeffs& coeffs, rational& weight);
-        numeral mk_weight(bool is_real, bool is_strict, rational const& w) const;
-        void mk_coeffs(vector<std::pair<expr*,rational> >const& terms, coeffs& coeffs, rational& w);
-
-        void del_atoms(unsigned old_size);
-
-        void propagate_core();
-
-        bool propagate_atom(atom const& a);
-
-        th_var mk_term(app* n);
-
-        th_var mk_num(app* n, rational const& r);
-
-        bool is_consistent() const;
-
-        th_var expand(bool pos, th_var v, rational & k);
-
-        void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
-        
-        th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
-
-        th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
-
-        void inc_conflicts();
-
-    };
-
-    struct rhi_ext {
-        typedef inf_rational inf_numeral;
-        typedef inf_eps_rational<inf_rational> numeral;
-        numeral     m_epsilon;
-        numeral     m_minus_infty;
-        rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {}
-    };
-
-    struct ihi_ext {
-        typedef rational inf_numeral;
-        typedef inf_eps_rational<rational> numeral;
-        numeral     m_epsilon;
-        numeral     m_minus_infty;
-        ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {}
-    };
-
-    typedef theory_horn_ineq<rhi_ext>  theory_rhi;
-    typedef theory_horn_ineq<ihi_ext>  theory_ihi;
-};
-
-
-
-
-#endif /* _THEORY_HORN_INEQ_H_ */

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include"bv_decl_plugin.h"
 #include"expr_replacer.h"
 #include"extension_model_converter.h"
+#include"filter_model_converter.h"
 #include"ast_smt2_pp.h"
 
 class bv_size_reduction_tactic : public tactic {
@@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp {
     obj_map<app, numeral>     m_unsigned_lowers;
     obj_map<app, numeral>     m_unsigned_uppers;
     ref<bv_size_reduction_mc> m_mc;
+    ref<filter_model_converter> m_fmc;
     scoped_ptr<expr_replacer> m_replacer;
     bool                      m_produce_models;
     volatile bool             m_cancel;
@@ -155,6 +157,7 @@ struct bv_size_reduction_tactic::imp {
                     else update_signed_lower(to_app(rhs), val);
                 }
             }
+            
 #if 0
             else if (m_util.is_bv_ule(f, lhs, rhs)) {
                 if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
@@ -215,6 +218,7 @@ struct bv_size_reduction_tactic::imp {
                         numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
                         TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
                         expr * new_def = 0;
+                        app  * new_const = 0;
                         if (l > u) {
                             g.assert_expr(m.mk_false());
                             return;
@@ -227,15 +231,19 @@ struct bv_size_reduction_tactic::imp {
                             if (l.is_neg()) {
                                 unsigned i_nb = (u - l).get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
-                                if (i_nb < v_nb)
+                                if (i_nb < v_nb) {
-                                    new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb)));
+                                    new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                    new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
+                                }
                             }
                             else {
                                 // 0 <= l <= v <= u
                                 unsigned u_nb = u.get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
-                                if (u_nb < v_nb)
+                                if (u_nb < v_nb) {
-                                    new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
+                                    new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
+                                    new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
+                                }
                             }
                         }
                     
@@ -245,6 +253,10 @@ struct bv_size_reduction_tactic::imp {
                                 if (!m_mc) 
                                     m_mc = alloc(bv_size_reduction_mc, m);
                                 m_mc->insert(v->get_decl(), new_def);
+                                if (!m_fmc && new_const) 
+                                    m_fmc = alloc(filter_model_converter, m);
+                                if (new_const) 
+                                    m_fmc->insert(new_const->get_decl());
                             }
                             num_reduced++;
                         }
@@ -283,6 +295,7 @@ struct bv_size_reduction_tactic::imp {
 
                     TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
                     expr * new_def = 0;
+                    app * new_const = 0;
                     if (l > u) {
                         g.assert_expr(m.mk_false());
                         return;
@@ -294,8 +307,10 @@ struct bv_size_reduction_tactic::imp {
                         // 0 <= l <= v <= u
                         unsigned u_nb = u.get_num_bits();
                         unsigned v_nb = m_util.get_bv_size(v);
-                        if (u_nb < v_nb)
+                        if (u_nb < v_nb) {
-                            new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
+                            new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
+                            new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
+                        }
                     }
                     
                     if (new_def) {
@@ -304,6 +319,10 @@ struct bv_size_reduction_tactic::imp {
                             if (!m_mc) 
                                 m_mc = alloc(bv_size_reduction_mc, m);
                             m_mc->insert(v->get_decl(), new_def);
+                            if (!m_fmc && new_const) 
+                                m_fmc = alloc(filter_model_converter, m);
+                            if (new_const) 
+                                m_fmc->insert(new_const->get_decl());
                         }
                         num_reduced++;
                         TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
@@ -328,7 +347,11 @@ struct bv_size_reduction_tactic::imp {
                 g.update(i, new_f);
             }
             mc   = m_mc.get();
+            if (m_fmc) {
+                mc = concat(m_fmc.get(), mc.get());
+            }
             m_mc = 0;
+            m_fmc = 0;
         }
         report_tactic_progress(":bv-reduced", num_reduced);
         TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1368,7 +1368,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
     not_f_sgn = m_bv_util.mk_bv_not(f_sgn);
     not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
-    res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv);
+    res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv);
     res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv);
     res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
     expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };   

src/tactic/fpa/qffpa_tactic.cpp

@@ -42,7 +42,7 @@ struct is_non_qffpa_predicate {
     ast_manager & m;
     float_util    u;
 
-    is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {}
+    is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {}
 
     void operator()(var *) { throw found(); }
 
@@ -50,7 +50,7 @@ struct is_non_qffpa_predicate {
 
     void operator()(app * n) {
         sort * s = get_sort(n);
-        if (!(m.is_bool(s) || u.is_float(s) || u.is_rm(s)))
+        if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s))
             throw found();
         family_id fid = n->get_family_id();
         if (fid == m.get_basic_family_id())
@@ -70,7 +70,7 @@ struct is_non_qffpabv_predicate {
     bv_util       bu;
     float_util    fu;
 
-    is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {}
+    is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {}
 
     void operator()(var *) { throw found(); }