Merge branch 'master' of https://github.com/Z3Prover/z3

examples/c++/example.cpp

@@ -294,7 +294,7 @@ void error_example() {
 
     // Error using the C API can be detected using Z3_get_error_code.
     // The next call fails because x is a constant.
-    Z3_ast arg = Z3_get_app_arg(c, x, 0);
+    //Z3_ast arg = Z3_get_app_arg(c, x, 0);
     if (Z3_get_error_code(c) != Z3_OK) {
         std::cout << "last call failed.\n";
     }
@@ -999,7 +999,6 @@ void opt_example() {
     opt.add(x + y <= 11);
     optimize::handle h1 = opt.maximize(x);
     optimize::handle h2 = opt.maximize(y);
-    check_result r = sat;
     while (true) {
         if (sat == opt.check()) {
             std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";

examples/c/test_capi.c

@@ -2610,7 +2610,7 @@ void fpa_example() {
     Z3_context ctx;
     Z3_sort double_sort, rm_sort;
     Z3_symbol s_rm, s_x, s_y, s_x_plus_y;
-    Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5, c6;
+    Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5;
 	Z3_ast args[2], args2[2], and_args[3], args3[3];
 
     printf("\nFPA-example\n");

examples/interp/iz3.cpp

@@ -42,7 +42,7 @@ int main(int argc, const char **argv) {
 
   Z3_config cfg = Z3_mk_config();
   // Z3_interpolation_options options = Z3_mk_interpolation_options();
-  Z3_params options = 0;
+  // Z3_params options = 0;
 
   /* Parse the command line */
   int argn = 1;
@@ -104,7 +104,7 @@ int main(int argc, const char **argv) {
   unsigned num_theory;
   Z3_ast *theory;
 
-  ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory);
+  ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0;
 
   /* If parse failed, print the error message */
 
@@ -124,7 +124,7 @@ int main(int argc, const char **argv) {
 	std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
 	num = nconjs;
 	constraints = new Z3_ast[num];
-	for(int k = 0; k < num; k++)
+	for(unsigned k = 0; k < num; k++)
 	  constraints[k] = Z3_get_app_arg(ctx,app,k);
       }
     }
@@ -163,12 +163,12 @@ int main(int argc, const char **argv) {
     std::vector<Z3_ast> asserted(num);
 
     /* We start with nothing asserted. */
-    for(int i = 0; i < num; i++)
+    for(unsigned i = 0; i < num; i++)
       asserted[i] = Z3_mk_true(ctx);
 
     /* Now we assert the constrints one at a time until UNSAT. */
 
-    for(int i = 0; i < num; i++){
+    for(unsigned i = 0; i < num; i++){
       asserted[i] = constraints[i];
       Z3_assert_cnstr(ctx,constraints[i]);  // assert one constraint
       result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents,  options, interpolants, &model, 0, true, 0, 0);
@@ -190,7 +190,7 @@ int main(int argc, const char **argv) {
     printf("unsat\n");
     if(output_file.empty()){
       printf("interpolant:\n");
-      for(int i = 0; i < num-1; i++)
+      for(unsigned i = 0; i < num-1; i++)
         printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
     }
     else {
@@ -203,7 +203,7 @@ int main(int argc, const char **argv) {
     if(check_mode){
       std::cout << "Checking interpolant...\n";
       bool chk;
-      chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory);  
+      chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0;
       if(chk)
 	std::cout << "Interpolant is correct\n";
       else {

examples/maxsat/maxsat.c

@@ -598,7 +598,7 @@ int smtlib_maxsat(char * file_name, int approach)
     Z3_context ctx;
     unsigned num_hard_cnstrs, num_soft_cnstrs;
     Z3_ast * hard_cnstrs, * soft_cnstrs;
-    unsigned result;
+    unsigned result = 0;
     ctx = mk_context();
     Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
     hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);

examples/tptp/tptp5.cpp

@@ -261,7 +261,7 @@ class env {
         parse(inc_name.c_str(), fmls);
         while (name_list) {
             return mk_error(name_list, "name list (not handled)");
-            char const* name = name_list->child(0)->symbol();
+            //char const* name = name_list->child(0)->symbol();
             name_list = name_list->child(2);            
         }
     }
@@ -614,7 +614,7 @@ class env {
 
     void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) {
         char const* name = t->symbol();
-        char const* id = 0;
+        //char const* id = 0;
         if (!strcmp(name,"tff_top_level_type")) {
             mk_mapping_sort(t->child(0), domain, s);
         }
@@ -1832,7 +1832,7 @@ public:
     }
 
     z3::expr get_proof_formula(z3::expr proof) {
-        unsigned na = proof.num_args();
+        // unsigned na = proof.num_args();
         z3::expr result = proof.arg(proof.num_args()-1);
         std::vector<z3::sort> vars;
         get_free_vars(result, vars);
@@ -2119,7 +2119,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
     int i = 1;
     while (i < argc) {
         char* arg = argv[i];
-        char * eq = 0;
+        //char * eq = 0;
         char * opt_arg = 0;
         if (arg[0] == '-' || arg[0] == '/') {
             ++arg;
@@ -2467,7 +2467,7 @@ static void prove_tptp() {
 
 int main(int argc, char** argv) {
 
-    std::ostream* out = &std::cout;
+    //std::ostream* out = &std::cout;
     g_start_time = static_cast<double>(clock());
     signal(SIGINT, on_ctrl_c);
 

examples/tptp/tptp5.tab.c

@@ -139,7 +139,7 @@ pTree pToken(char* token, int symbolIndex) {
 
     //char pTokenBuf[8240];
     pTree ss;
-    char* symbol = tptp_lval[symbolIndex];
+    //char* symbol = tptp_lval[symbolIndex];
     char* safeSym = 0;
 
     //strncpy(pTokenBuf, token, 39);

scripts/mk_unix_dist.py

@@ -191,7 +191,7 @@ def mk_zip():
         os.chdir(DIST_DIR)
         zfname = '%s.zip' % dist_path
         ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
-        os.path.walk(dist_path, mk_zip_visitor, '*')
+        os.walk(dist_path, mk_zip_visitor, '*')
         if is_verbose():
             print("Generated '%s'" % zfname)
     except:

scripts/mk_util.py

@@ -90,7 +90,7 @@ FPMATH="Default"
 FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
 
 def check_output(cmd):
-    return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n')
+    return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n')
 
 def git_hash():
     try:
@@ -512,7 +512,7 @@ def dos2unix_tree_core(pattern, dir, files):
                 dos2unix(fname)
 
 def dos2unix_tree():
-    os.path.walk('src', dos2unix_tree_core, '*')
+    os.walk('src', dos2unix_tree_core, '*')
 
 def check_eol():
     if not IS_WINDOWS:
@@ -1578,20 +1578,22 @@ class CppExampleComponent(ExampleComponent):
     def mk_makefile(self, out):
         dll_name = get_component(Z3_DLL_COMPONENT).dll_name
         dll = '%s$(SO_EXT)' % dll_name
+
+        objfiles = ''
+        for cppfile in self.src_files():
+            objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')])
+            objfiles = objfiles + ('%s ' % objfile)
+            out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile)));
+            out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile))
+            # Add include dir components
+            out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
+            out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
+            out.write(' %s' % os.path.join(self.to_ex_dir, cppfile))
+            out.write('\n')            
+        
         exefile = '%s$(EXE_EXT)' % self.name
-        out.write('%s: %s' % (exefile, dll))
+        out.write('%s: %s %s\n' % (exefile, dll, objfiles))
-        for cppfile in self.src_files():
+        out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles))
-            out.write(' ')
-            out.write(os.path.join(self.to_ex_dir, cppfile))
-        out.write('\n')
-        out.write('\t%s $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile))
-        # Add include dir components
-        out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir)
-        out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir)
-        for cppfile in self.src_files():
-            out.write(' ')
-            out.write(os.path.join(self.to_ex_dir, cppfile))
-        out.write(' ')
         if IS_WINDOWS:
             out.write('%s.lib' % dll_name)
         else:

scripts/mk_win_dist.py

@@ -206,7 +206,7 @@ def mk_zip_core(x64):
         os.chdir(DIST_DIR)
         zfname = '%s.zip' % dist_path
         ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
-        os.path.walk(dist_path, mk_zip_visitor, '*')
+        os.walk(dist_path, mk_zip_visitor, '*')
         if is_verbose():
             print("Generated '%s'" % zfname)
     except:
@@ -245,10 +245,10 @@ def cp_vs_runtime_core(x64):
         
     else:
         platform = "x86"
-    vcdir = subprocess.check_output(['echo', '%VCINSTALLDIR%'], shell=True).rstrip('\r\n')
+    vcdir = os.environ['VCINSTALLDIR']
     path  = '%sredist\\%s' % (vcdir, platform)
     VS_RUNTIME_FILES = []
-    os.path.walk(path, cp_vs_runtime_visitor, '*.dll')
+    os.walk(path, cp_vs_runtime_visitor, '*.dll')
     bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin')
     for f in VS_RUNTIME_FILES:
         shutil.copy(f, bin_dist_path)

src/api/api_interp.cpp

@@ -255,6 +255,14 @@ extern "C" {
         scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
         m_solver.get()->updt_params(_p); // why do we have to do this?
 
+
+        // some boilerplate stolen from Z3_solver_check
+        unsigned timeout     =  to_params(p)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      =  to_params(p)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  =  to_params(p)->m_params.get_bool("ctrl_c", false);
+        cancel_eh<solver> eh(*m_solver.get());
+        api::context::set_interruptable si(*(mk_c(c)), eh);
+
         ast *_pat = to_ast(pat);
 
         ptr_vector<ast> interp;
@@ -263,14 +271,27 @@ extern "C" {
         ast_manager &_m = mk_c(c)->m();
 
         model_ref m;
-        lbool _status = iz3interpolate(_m,
+        lbool _status;
-                                       *(m_solver.get()),
+
-                                       _pat,
+        {
-                                       cnsts,
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
-                                       interp,
+            scoped_timer timer(timeout, &eh);
-                                       m,
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
-                                       0 // ignore params for now
+            try {
-                                       );
+                _status = iz3interpolate(_m,
+                                         *(m_solver.get()),
+                                         _pat,
+                                         cnsts,
+                                         interp,
+                                         m,
+                                         0 // ignore params for now
+                                         );
+            }
+            catch (z3_exception & ex) {
+                mk_c(c)->handle_exception(ex);
+                return Z3_L_UNDEF;
+            }
+        }
 
         for (unsigned i = 0; i < cnsts.size(); i++)
             _m.dec_ref(cnsts[i]);
@@ -292,10 +313,12 @@ extern "C" {
         else {
             model_ref mr;
             m_solver.get()->get_model(mr);
-            Z3_model_ref *tmp_val = alloc(Z3_model_ref);
+            if(mr.get()){
-            tmp_val->m_model = mr.get();
+                Z3_model_ref *tmp_val = alloc(Z3_model_ref);
-            mk_c(c)->save_object(tmp_val);
+                tmp_val->m_model = mr.get();
-            *model = of_model(tmp_val);
+                mk_c(c)->save_object(tmp_val);
+                *model = of_model(tmp_val);
+            }
         }
 
         *out_interp = of_ast_vector(v);

src/api/dotnet/Properties/AssemblyInfo

@@ -1,4 +1,4 @@
-using System;
+using System;
 using System.Reflection;
 using System.Runtime.CompilerServices;
 using System.Runtime.InteropServices;

src/api/python/z3.py

@@ -7598,6 +7598,10 @@ def tree_interpolant(pat,p=None,ctx=None):
     If pat is satisfiable, raises an object of class ModelRef
     that represents a model of pat.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
@@ -7623,7 +7627,9 @@ def tree_interpolant(pat,p=None,ctx=None):
     res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
     if res == Z3_L_FALSE:
         return AstVector(ptr[0],ctx)
-    raise ModelRef(mptr[0], ctx)
+    if mptr[0]:
+        raise ModelRef(mptr[0], ctx)
+    return None
 
 def binary_interpolant(a,b,p=None,ctx=None):
     """Compute an interpolant for a binary conjunction.
@@ -7638,6 +7644,10 @@ def binary_interpolant(a,b,p=None,ctx=None):
     If a & b is satisfiable, raises an object of class ModelRef
     that represents a model of a &b.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
@@ -7646,7 +7656,8 @@ def binary_interpolant(a,b,p=None,ctx=None):
     Not(x >= 0)
     """
     f = And(Interpolant(a),b)
-    return tree_interpolant(f,p,ctx)[0]
+    ti = tree_interpolant(f,p,ctx)
+    return ti[0] if ti != None else None
 
 def sequence_interpolant(v,p=None,ctx=None):
     """Compute interpolant for a sequence of formulas.
@@ -7664,6 +7675,10 @@ def sequence_interpolant(v,p=None,ctx=None):
     If a & b is satisfiable, raises an object of class ModelRef
     that represents a model of a & b.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 

src/ast/rewriter/fpa_rewriter.cpp

@@ -33,7 +33,7 @@ void fpa_rewriter::updt_params(params_ref const & _p) {
     fpa_rewriter_params p(_p);
     m_hi_fp_unspecified = p.hi_fp_unspecified();
 }
- 
+
 void fpa_rewriter::get_param_descrs(param_descrs & r) {
 }
 
@@ -72,7 +72,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_SQRT:      SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
     case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;
 
-    case OP_FPA_EQ:        SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; 
+    case OP_FPA_EQ:        SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break;
     case OP_FPA_LT:        SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
     case OP_FPA_GT:        SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break;
     case OP_FPA_LE:        SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
@@ -83,29 +83,29 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
     case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
     case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
-    case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;    
+    case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
 
-    case OP_FPA_FP:        SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;    
+    case OP_FPA_FP:        SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
     case OP_FPA_TO_FP:     st = mk_to_fp(f, num_args, args, result); break;
     case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break;
     case OP_FPA_TO_UBV:    SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break;
     case OP_FPA_TO_SBV:    SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break;
     case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
-    case OP_FPA_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;    
+    case OP_FPA_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
 
     case OP_FPA_INTERNAL_MIN_I:
-    case OP_FPA_INTERNAL_MAX_I:        
+    case OP_FPA_INTERNAL_MAX_I:
-    case OP_FPA_INTERNAL_MIN_UNSPECIFIED:        
+    case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
-    case OP_FPA_INTERNAL_MAX_UNSPECIFIED: 
+    case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
         SASSERT(num_args == 2); st = BR_FAILED; break;
 
     case OP_FPA_INTERNAL_RM:
         SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
-    case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: 
+    case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
         SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break;
     case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
         SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break;
-    case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: 
+    case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
         SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break;
 
     case OP_FPA_INTERNAL_BVWRAP:
@@ -113,7 +113,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         st = BR_FAILED;
         break;
 
-    default: 
+    default:
         NOT_IMPLEMENTED_YET();
     }
     return st;
@@ -171,7 +171,7 @@ br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
     else
         result = m_util.mk_internal_to_real_unspecified();
 
-    return BR_DONE;    
+    return BR_DONE;
 }
 
 br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@@ -186,7 +186,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
     unsigned ebits = f->get_parameter(0).get_int();
     unsigned sbits = f->get_parameter(1).get_int();
 
-    if (num_args == 1) {                
+    if (num_args == 1) {
         if (bu.is_numeral(args[0], r1, bvs1)) {
             // BV -> float
             SASSERT(bvs1 == sbits + ebits);
@@ -196,13 +196,13 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
 
             const mpz & sm1 = m_fm.m_powers2(sbits - 1);
             const mpz & em1 = m_fm.m_powers2(ebits);
-            
+
             scoped_mpq q(mpqm);
             mpqm.set(q, r1.to_mpq());
             SASSERT(mpzm.is_one(q.get().denominator()));
             scoped_mpz z(mpzm);
             z = q.get().numerator();
-            
+
             mpzm.rem(z, sm1, sig);
             mpzm.div(z, sm1, z);
 
@@ -214,7 +214,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
             mpf_exp = m_fm.unbias_exp(ebits, mpf_exp);
 
             m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp);
-            TRACE("fp_rewriter", 
+            TRACE("fp_rewriter",
                   tout << "sgn: " << !mpzm.is_zero(z) << std::endl;
                   tout << "sig: " << mpzm.to_string(sig) << std::endl;
                   tout << "exp: " << mpf_exp << std::endl;
@@ -227,9 +227,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
     else if (num_args == 2) {
         if (!m_util.is_rm_numeral(args[0], rmv))
             return BR_FAILED;
-        
+
-        if (m_util.au().is_numeral(args[1], r1)) {            
+        if (m_util.au().is_numeral(args[1], r1)) {
-            // rm + real -> float            
+            // rm + real -> float
             TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;);
             scoped_mpf v(m_fm);
             m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
@@ -246,7 +246,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
             // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
             return BR_DONE;
         }
-        else if (bu.is_numeral(args[1], r1, bvs1)) {            
+        else if (bu.is_numeral(args[1], r1, bvs1)) {
             // rm + signed bv -> float
             TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;);
             r1 = bu.norm(r1, bvs1, true);
@@ -256,7 +256,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
             return BR_DONE;
         }
     }
-    else if (num_args == 3) {        
+    else if (num_args == 3) {
         if (m_util.is_rm_numeral(args[0], rmv) &&
             m_util.au().is_real(args[1]) &&
             m_util.au().is_int(args[2])) {
@@ -286,7 +286,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
             TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;);
             result = m_util.mk_value(v);
             return BR_DONE;
-        }        
+        }
     }
 
     return BR_FAILED;
@@ -296,13 +296,13 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
     SASSERT(f->get_num_parameters() == 2);
     SASSERT(f->get_parameter(0).is_int());
     SASSERT(f->get_parameter(1).is_int());
-    bv_util bu(m());    
+    bv_util bu(m());
     unsigned ebits = f->get_parameter(0).get_int();
     unsigned sbits = f->get_parameter(1).get_int();
     mpf_rounding_mode rmv;
     rational r;
     unsigned bvs;
-    
+
     if (m_util.is_rm_numeral(arg1, rmv) &&
         bu.is_numeral(arg2, r, bvs)) {
         scoped_mpf v(m_fm);
@@ -314,7 +314,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
     return BR_FAILED;
 }
 
-br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     mpf_rounding_mode rm;
     if (m_util.is_rm_numeral(arg1, rm)) {
         scoped_mpf v2(m_fm), v3(m_fm);
@@ -335,7 +335,7 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref &
     return BR_REWRITE2;
 }
 
-br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     mpf_rounding_mode rm;
     if (m_util.is_rm_numeral(arg1, rm)) {
         scoped_mpf v2(m_fm), v3(m_fm);
@@ -386,7 +386,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) {
         result = to_app(arg1)->get_arg(0);
         return BR_DONE;
     }
-    
+
     scoped_mpf v1(m_fm);
     if (m_util.is_numeral(arg1, v1)) {
         m_fm.neg(v1);
@@ -414,14 +414,14 @@ br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) {
         result = arg1;
         return BR_DONE;
     }
-    
+
     scoped_mpf v(m_fm);
     if (m_util.is_numeral(arg1, v)) {
         if (m_fm.is_neg(v)) m_fm.neg(v);
         result = m_util.mk_value(v);
         return BR_DONE;
     }
-    
+
     return BR_FAILED;
 }
 
@@ -434,7 +434,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
         result = arg1;
         return BR_DONE;
     }
-    
+
     scoped_mpf v1(m_fm), v2(m_fm);
     if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
         if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
@@ -543,6 +543,7 @@ br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref
 // This the floating point theory ==
 br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) {
     scoped_mpf v1(m_fm), v2(m_fm);
+
     if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
         result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
@@ -745,22 +746,22 @@ br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) {
         case BV_RM_TO_ZERO:
         default: result = m_util.mk_round_toward_zero();
         }
-        
+
         return BR_DONE;
     }
 
     return BR_FAILED;
 }
 
-br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
     bv_util bu(m());
     rational r1, r2, r3;
-    unsigned bvs1, bvs2, bvs3;    
+    unsigned bvs1, bvs2, bvs3;
 
-    if (bu.is_numeral(arg1, r1, bvs1) && 
+    if (bu.is_numeral(arg1, r1, bvs1) &&
-        bu.is_numeral(arg2, r2, bvs2) && 
+        bu.is_numeral(arg2, r2, bvs2) &&
-        bu.is_numeral(arg3, r3, bvs3)) {        
+        bu.is_numeral(arg3, r3, bvs3)) {
         SASSERT(mpzm.is_one(r2.to_mpq().denominator()));
         SASSERT(mpzm.is_one(r3.to_mpq().denominator()));
         SASSERT(mpzm.is_int64(r3.to_mpq().numerator()));
@@ -769,7 +770,7 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref &
         m_fm.set(v, bvs2, bvs3 + 1,
                         r1.is_one(),
                         r3.to_mpq().numerator(),
-                        m_fm.unbias_exp(bvs2, biased_exp));        
+                        m_fm.unbias_exp(bvs2, biased_exp));
         TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;);
         result = m_util.mk_value(v);
         return BR_DONE;
@@ -780,24 +781,24 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref &
 
 br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
     SASSERT(f->get_num_parameters() == 1);
-    SASSERT(f->get_parameter(0).is_int());    
+    SASSERT(f->get_parameter(0).is_int());
     int bv_sz = f->get_parameter(0).get_int();
     mpf_rounding_mode rmv;
     scoped_mpf v(m_fm);
 
     if (m_util.is_rm_numeral(arg1, rmv) &&
-        m_util.is_numeral(arg2, v)) {        
+        m_util.is_numeral(arg2, v)) {
 
         if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
             mk_to_ubv_unspecified(f, result);
             return BR_REWRITE_FULL;
-        } 
+        }
 
         bv_util bu(m());
-        scoped_mpq q(m_fm.mpq_manager());        
+        scoped_mpq q(m_fm.mpq_manager());
         m_fm.to_sbv_mpq(rmv, v, q);
-        
+
-        rational r(q);        
+        rational r(q);
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz);
         ll = rational(0);
@@ -813,7 +814,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
 
 br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
     SASSERT(f->get_num_parameters() == 1);
-    SASSERT(f->get_parameter(0).is_int());    
+    SASSERT(f->get_parameter(0).is_int());
     int bv_sz = f->get_parameter(0).get_int();
     mpf_rounding_mode rmv;
     scoped_mpf v(m_fm);
@@ -829,8 +830,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
         m_fm.to_sbv_mpq(rmv, v, q);
-        
+
-        rational r(q);        
+        rational r(q);
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz - 1);
         ll = - m_fm.m_powers2(bv_sz - 1);
@@ -853,7 +854,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
             mk_to_ieee_bv_unspecified(f, result);
             return BR_REWRITE_FULL;
         }
-        
+
         bv_util bu(m());
         scoped_mpz rz(m_fm.mpq_manager());
         m_fm.to_ieee_bv_mpz(v, rz);
@@ -866,7 +867,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
 
 br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
     scoped_mpf v(m_fm);
-    
+
     if (m_util.is_numeral(arg, v)) {
         if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
             result = m_util.mk_internal_to_real_unspecified();

src/ast/rewriter/fpa_rewriter.h

@@ -39,13 +39,13 @@ public:
 
     ast_manager & m() const { return m_util.m(); }
     family_id get_fid() const { return m_util.get_fid(); }
-    
+
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
-    
+
     br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
@@ -77,7 +77,7 @@ public:
 
     br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
-    
+
     br_status mk_rm(expr * arg, expr_ref & result);
     br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);

src/smt/theory_fpa.cpp

@@ -29,7 +29,7 @@ namespace smt {
         obj_map<expr, expr*> & m_conversions;
         expr * m_e;
     public:
-        fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) : 
+        fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
             m(m), m_conversions(c), m_e(e) {}
         virtual ~fpa2bv_conversion_trail_elem() {}
         virtual void undo(theory_fpa & th) {
@@ -63,7 +63,7 @@ namespace smt {
             m.inc_ref(f);
             m.inc_ref(result);
         }
-    }        
+    }
 
     void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
         SASSERT(f->get_family_id() == null_family_id);
@@ -89,12 +89,12 @@ namespace smt {
     }
 
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
-        // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.        
+        // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
         unsigned ebits = m_util.get_ebits(f->get_range());
         unsigned sbits = m_util.get_sbits(f->get_range());
         unsigned bv_sz = ebits + sbits;
         expr_ref res(m);
-        
+
         expr * args[] = { x, y };
         func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range());
         expr_ref a(m), wrapped(m);
@@ -110,7 +110,7 @@ namespace smt {
         m_extra_assertions.push_back(sc);
         return res;
     }
-    
+
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
         // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
         unsigned ebits = m_util.get_ebits(f->get_range());
@@ -118,7 +118,7 @@ namespace smt {
         unsigned bv_sz = ebits + sbits;
         expr_ref res(m);
 
-        expr * args[] = { x, y };        
+        expr * args[] = { x, y };
         func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range());
         expr_ref a(m), wrapped(m);
         a = m.mk_app(w, x, y);
@@ -154,15 +154,15 @@ namespace smt {
         ast_manager & m = get_manager();
         dec_ref_map_values(m, m_conversions);
         dec_ref_map_values(m, m_wraps);
-        dec_ref_map_values(m, m_unwraps);          
+        dec_ref_map_values(m, m_unwraps);
     }
 
     app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
-        ast_manager & m = m_th.get_manager();        
+        ast_manager & m = m_th.get_manager();
 
         TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
                                   tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
-        
+
         mpf_manager & mpfm = m_fu.fm();
         unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         app * result;
@@ -195,7 +195,7 @@ namespace smt {
 
             mpzm.set(sig_z, all_z);
         }
-        else if (values.size() == 3) {            
+        else if (values.size() == 3) {
             rational sgn_r(0), exp_r(0), sig_r(0);
 
             bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz);
@@ -204,7 +204,7 @@ namespace smt {
             SASSERT(r && bv_sz == m_ebits);
             r = m_bu.is_numeral(values[2], sig_r, bv_sz);
             SASSERT(r && bv_sz == m_sbits - 1);
-            
+
             SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
             SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
             SASSERT(mpzm.is_one(sig_r.to_mpq().denominator()));
@@ -228,25 +228,25 @@ namespace smt {
                        mpzm.to_string(exp_z) << "," <<
                        mpzm.to_string(sig_z) << "] --> " <<
                        mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
-        
+
         return result;
     }
 
     app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == 1);
         ast_manager & m = m_th.get_manager();
-        
+
         TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
               tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
 
-        app * result = 0;        
+        app * result = 0;
         unsigned bv_sz;
 
         rational val(0);
         bool r = m_bu.is_numeral(values[0], val, bv_sz);
         SASSERT(r);
         SASSERT(bv_sz == 3);
-            
+
         switch (val.get_uint64())
         {
         case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
@@ -257,7 +257,7 @@ namespace smt {
         default: result = m_fu.mk_round_toward_zero();
         }
 
-        TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << 
+        TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
                                mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
 
         return result;
@@ -272,7 +272,7 @@ namespace smt {
 
         if (!m_wraps.find(e_srt, w)) {
             SASSERT(!m_wraps.contains(e_srt));
-            
+
             sort * bv_srt;
             if (m_converter.is_rm(e_srt))
                 bv_srt = m_bv_util.mk_sort(3);
@@ -280,9 +280,9 @@ namespace smt {
                 SASSERT(m_converter.is_float(e_srt));
                 unsigned ebits = m_fpa_util.get_ebits(e_srt);
                 unsigned sbits = m_fpa_util.get_sbits(e_srt);
-                bv_srt = m_bv_util.mk_sort(ebits + sbits);                
+                bv_srt = m_bv_util.mk_sort(ebits + sbits);
             }
-                       
+
             w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
             m_wraps.insert(e_srt, w);
             m.inc_ref(w);
@@ -295,7 +295,7 @@ namespace smt {
 
     app_ref theory_fpa::unwrap(expr * e, sort * s) {
         SASSERT(!m_fpa_util.is_unwrap(e));
-        ast_manager & m = get_manager();        
+        ast_manager & m = get_manager();
         sort * bv_srt = m.get_sort(e);
 
         func_decl *u;
@@ -311,7 +311,7 @@ namespace smt {
         res = m.mk_app(u, e);
         return res;
     }
-    
+
     expr_ref theory_fpa::convert_atom(expr * e) {
         ast_manager & m = get_manager();
         TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";);
@@ -320,7 +320,7 @@ namespace smt {
         m_rw(e, res);
         m_th_rw(res, res);
         SASSERT(is_app(res));
-        SASSERT(m.is_bool(res));        
+        SASSERT(m.is_bool(res));
         return res;
     }
 
@@ -331,12 +331,12 @@ namespace smt {
         expr_ref e_conv(m), res(m);
         proof_ref pr(m);
         m_rw(e, e_conv);
-        
+
-        if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {            
+        if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
             if (!m_fpa_util.is_float(e_conv))
                 m_th_rw(e_conv, res);
             else {
-                expr_ref bv(m);            
+                expr_ref bv(m);
                 bv = wrap(e_conv);
                 unsigned bv_sz = m_bv_util.get_bv_size(bv);
                 unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
@@ -365,7 +365,7 @@ namespace smt {
             m_converter.mk_fp(sgn, exp, sig, res);
         }
         else
-            UNREACHABLE();        
+            UNREACHABLE();
 
         SASSERT(res.get() != 0);
         return res;
@@ -426,7 +426,7 @@ namespace smt {
 
     expr_ref theory_fpa::convert_conversion_term(expr * e) {
         /* This is for the conversion functions fp.to_* */
-        ast_manager & m = get_manager();        
+        ast_manager & m = get_manager();
         expr_ref res(m);
         proof_ref pr(m);
 
@@ -480,7 +480,7 @@ namespace smt {
             else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
                 res = convert_term(e);
             else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
-                res = convert_conversion_term(e);            
+                res = convert_conversion_term(e);
             else
                 UNREACHABLE();
 
@@ -492,7 +492,7 @@ namespace smt {
             m.inc_ref(res);
             m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
         }
-        
+
         return res;
     }
 
@@ -501,7 +501,7 @@ namespace smt {
         ast_manager & m = get_manager();
         context & ctx = get_context();
         simplifier & simp = ctx.get_simplifier();
-        
+
         expr_ref res(m), t(m);
         proof_ref t_pr(m);
         res = m.mk_true();
@@ -515,21 +515,21 @@ namespace smt {
         m_converter.m_extra_assertions.reset();
 
         m_th_rw(res);
-        
+
         CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
         return res;
     }
 
     void theory_fpa::assert_cnstr(expr * e) {
         if (get_manager().is_true(e)) return;
-        TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);        
+        TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
         context & ctx = get_context();
         ctx.internalize(e, false);
         literal lit(ctx.get_literal(e));
         ctx.mark_as_relevant(lit);
-        ctx.mk_th_axiom(get_id(), 1, &lit);        
+        ctx.mk_th_axiom(get_id(), 1, &lit);
         TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
-    }    
+    }
 
     void theory_fpa::attach_new_th_var(enode * n) {
         context & ctx = get_context();
@@ -556,10 +556,10 @@ namespace smt {
         ctx.set_var_theory(l.var(), get_id());
 
         expr_ref bv_atom(m);
-        bv_atom = convert_atom(atom);        
+        bv_atom = convert_atom(atom);
         SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
         bv_atom = m.mk_and(bv_atom, mk_side_conditions());
-        
+
         assert_cnstr(m.mk_iff(atom, bv_atom));
         return true;
     }
@@ -569,29 +569,29 @@ namespace smt {
         context & ctx = get_context();
         TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
         SASSERT(term->get_family_id() == get_family_id());
-        SASSERT(!ctx.e_internalized(term));        
+        SASSERT(!ctx.e_internalized(term));
 
         unsigned num_args = term->get_num_args();
         for (unsigned i = 0; i < num_args; i++)
             ctx.internalize(term->get_arg(i), false);
-        
+
         enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
                                                  ctx.mk_enode(term, false, false, true);
-        
+
         if (is_attached_to_var(e))
             return false;
 
         attach_new_th_var(e);
 
         // The conversion operators fp.to_* appear in non-FP constraints.
-        // The corresponding constraints will not be translated and added 
+        // The corresponding constraints will not be translated and added
         // via convert(...) and assert_cnstr(...) in initialize_atom(...).
         // Therefore, we translate and assert them here.
         fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
         switch (k) {
         case OP_FPA_TO_UBV:
         case OP_FPA_TO_SBV:
-        case OP_FPA_TO_REAL: 
+        case OP_FPA_TO_REAL:
         case OP_FPA_TO_IEEE_BV: {
             expr_ref conv(m);
             conv = convert(term);
@@ -599,32 +599,32 @@ namespace smt {
             assert_cnstr(mk_side_conditions());
             break;
         }
-        default: /* ignore */;            
+        default: /* ignore */;
         }
 
         return true;
-    }    
+    }
 
     void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {
         TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
         SASSERT(s->get_family_id() == get_family_id());
-        
+
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        
+
         app_ref owner(m);
         owner = n->get_owner();
-        
+
         SASSERT(owner->get_decl()->get_range() == s);
 
-        if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&        
+        if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&
             !is_attached_to_var(n)) {
-            
+
-            attach_new_th_var(n);            
+            attach_new_th_var(n);
 
             if (m_fpa_util.is_rm(s)) {
                 // For every RM term, we need to make sure that it's
-                // associated bit-vector is within the valid range.            
+                // associated bit-vector is within the valid range.
                 if (!m_fpa_util.is_unwrap(owner)) {
                     expr_ref valid(m), limit(m);
                     limit = m_bv_util.mk_numeral(4, 3);
@@ -638,7 +638,7 @@ namespace smt {
         }
     }
 
-    void theory_fpa::new_eq_eh(theory_var x, theory_var y) {        
+    void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
         ast_manager & m = get_manager();
         enode * e_x = get_enode(x);
         enode * e_y = get_enode(y);
@@ -646,7 +646,7 @@ namespace smt {
         TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
         TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " <<
                                       mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
-        
+
         fpa_util & fu = m_fpa_util;
 
         expr_ref xe(m), ye(m);
@@ -664,13 +664,13 @@ namespace smt {
                                       "yc = " << mk_ismt2_pp(yc, m) << std::endl;);
 
         expr_ref c(m);
-        
+
         if ((fu.is_float(xe) && fu.is_float(ye)) ||
             (fu.is_rm(xe) && fu.is_rm(ye)))
             m_converter.mk_eq(xc, yc, c);
-        else 
+        else
             c = m.mk_eq(xc, yc);
-        
+
         m_th_rw(c);
         assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
         assert_cnstr(mk_side_conditions());
@@ -722,33 +722,33 @@ namespace smt {
         m_trail_stack.push_scope();
     }
 
-    void theory_fpa::pop_scope_eh(unsigned num_scopes) {                
+    void theory_fpa::pop_scope_eh(unsigned num_scopes) {
         m_trail_stack.pop_scope(num_scopes);
         TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
-        // unsigned num_old_vars = get_old_num_vars(num_scopes);        
+        // unsigned num_old_vars = get_old_num_vars(num_scopes);
         theory::pop_scope_eh(num_scopes);
-    }    
+    }
 
     void theory_fpa::assign_eh(bool_var v, bool is_true) {
         ast_manager & m = get_manager();
         context & ctx = get_context();
         expr * e = ctx.bool_var2expr(v);
-        
+
         TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
-        
+
         expr_ref converted(m);
         converted = m.mk_and(convert(e), mk_side_conditions());
         if (is_true)
             assert_cnstr(m.mk_implies(e, converted));
-        else 
+        else
-            assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));        
+            assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
     }
 
     void theory_fpa::relevant_eh(app * n) {
         ast_manager & m = get_manager();
         TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";);
 
-        mpf_manager & mpfm = m_fpa_util.fm();        
+        mpf_manager & mpfm = m_fpa_util.fm();
 
         if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
             if (!m_fpa_util.is_unwrap(n)) {
@@ -757,7 +757,7 @@ namespace smt {
                 mpf_rounding_mode rm;
                 scoped_mpf val(mpfm);
                 if (m_fpa_util.is_rm_numeral(n, rm)) {
-                    c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));                    
+                    c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
                     assert_cnstr(c);
                 }
                 else if (m_fpa_util.is_numeral(n, val)) {
@@ -772,7 +772,7 @@ namespace smt {
                     assert_cnstr(c);
                 }
                 else {
-                    c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);                    
+                    c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
                     assert_cnstr(c);
                 }
             }
@@ -803,7 +803,7 @@ namespace smt {
     final_check_status theory_fpa::final_check_eh() {
         TRACE("t_fpa", tout << "final_check_eh\n";);
         SASSERT(m_converter.m_extra_assertions.empty());
-        return FC_DONE; 
+        return FC_DONE;
     }
 
     void theory_fpa::init_model(model_generator & mg) {
@@ -813,7 +813,7 @@ namespace smt {
     }
 
     model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
-        TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << 
+        TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
                             " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
 
         ast_manager & m = get_manager();
@@ -821,14 +821,14 @@ namespace smt {
         app_ref owner(m);
         owner = n->get_owner();
 
-        // If the owner is not internalized, it doesn't have an enode associated.        
+        // If the owner is not internalized, it doesn't have an enode associated.
         SASSERT(ctx.e_internalized(owner));
-        
+
         if (m_fpa_util.is_rm_numeral(owner) ||
             m_fpa_util.is_numeral(owner)) {
             return alloc(expr_wrapper_proc, owner);
         }
-        
+
         model_value_proc * res = 0;
 
         app_ref wrapped(m);
@@ -849,7 +849,7 @@ namespace smt {
             a2 = to_app(owner->get_arg(2));
             unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
             unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
-            fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);            
+            fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
             vp->add_dependency(ctx.get_enode(a0));
             vp->add_dependency(ctx.get_enode(a1));
             vp->add_dependency(ctx.get_enode(a2));
@@ -891,8 +891,8 @@ namespace smt {
     {
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        
+
-        out << "fpa theory variables:" << std::endl;        
+        out << "fpa theory variables:" << std::endl;
         ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
         ptr_vector<enode>::const_iterator end = ctx.end_enodes();
         for (; it != end; it++) {
@@ -907,7 +907,7 @@ namespace smt {
         for (; it != end; it++) {
             theory_var v = (*it)->get_th_var(m_bv_util.get_family_id());
             if (v != -1) out << v << " -> " <<
-                mk_ismt2_pp((*it)->get_owner(), m) << std::endl;            
+                mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
         }
 
         out << "arith theory variables:" << std::endl;

src/smt/theory_fpa.h

@@ -84,13 +84,13 @@ namespace smt {
             virtual void mk_const(func_decl * f, expr_ref & result);
             virtual void mk_rm_const(func_decl * f, expr_ref & result);
             virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-            
+
             virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
             virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
         };
-        
+
         class fpa_value_proc : public model_value_proc {
-        protected:            
+        protected:
             theory_fpa  & m_th;
             ast_manager & m;
             fpa_util    & m_fu;
@@ -100,10 +100,10 @@ namespace smt {
             unsigned m_sbits;
 
         public:
-            fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : 
+            fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
                 m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
                 m_ebits(ebits), m_sbits(sbits) {}
-            
+
             virtual ~fpa_value_proc() {}
 
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
@@ -123,7 +123,7 @@ namespace smt {
             buffer<model_value_dependency> m_deps;
 
         public:
-            fpa_rm_value_proc(theory_fpa * th) : 
+            fpa_rm_value_proc(theory_fpa * th) :
                 m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
 
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
@@ -135,7 +135,7 @@ namespace smt {
             virtual ~fpa_rm_value_proc() {}
             virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
         };
-    
+
     protected:
         fpa2bv_converter_wrapped  m_converter;
         fpa2bv_rewriter           m_rw;
@@ -159,10 +159,10 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual void reset_eh();
         virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
-        virtual char const * get_name() const { return "fpa"; }        
+        virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
-        
+
         void assign_eh(bool_var v, bool is_true);
         virtual void relevant_eh(app * n);
         virtual void init_model(model_generator & m);
@@ -181,14 +181,14 @@ namespace smt {
         expr_ref convert_term(expr * e);
         expr_ref convert_conversion_term(expr * e);
         expr_ref convert_unwrap(expr * e);
-        
+
         void add_trail(ast * a);
 
         void attach_new_th_var(enode * n);
         void assert_cnstr(expr * e);
 
         app_ref wrap(expr * e);
-        app_ref unwrap(expr * e, sort * s);        
+        app_ref unwrap(expr * e, sort * s);
     };
 
 };