mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-05-31 18:35:52 +01:00
commit 596652ed36
42 changed files with 336 additions and 941 deletions
Download patch file Download diff file Expand all files Collapse all files

29
CMakeLists.txt
View file

@ -274,18 +274,6 @@ else()
message(STATUS "Not using libgmp")
endif()
################################################################################
# FOCI2 support
################################################################################
# FIXME: What is this?
option(USE_FOCI2 "Use FOCI2" OFF)
if (USE_FOCI2)
message(FATAL_ERROR "TODO")
message(STATUS "Using FOCI2")
else()
message(STATUS "Not using FOCI2")
endif()
################################################################################
# OpenMP support
################################################################################
@ -318,6 +306,23 @@ else()
set(USE_OPENMP OFF CACHE BOOL "Use OpenMP" FORCE)
endif()
################################################################################
# API Log sync
################################################################################
option(API_LOG_SYNC
"Use locking when logging Z3 API calls (experimental)"
OFF
)
if (API_LOG_SYNC)
if (NOT USE_OPENMP)
message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP")
endif()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
message(STATUS "Using API_LOG_SYNC")
else()
message(STATUS "Not using API_LOG_SYNC")
endif()
################################################################################
# FP math
################################################################################

3
README-CMake.md
View file

@ -1,4 +1,4 @@
# Z3's CMake build system
# Z3's CMake build system
[CMake](https://cmake.org/) is a "meta build system" that reads a description
of the project written in the ``CMakeLists.txt`` files and emits a build
@ -293,6 +293,7 @@ The following useful options can be passed to CMake whilst configuring.
* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
* ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.

1
contrib/cmake/src/ast/rewriter/CMakeLists.txt
View file

@ -8,6 +8,7 @@ z3_add_component(rewriter
bv_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp
dl_rewriter.cpp
enum2bv_rewriter.cpp
expr_replacer.cpp

1
contrib/cmake/src/ast/simplifier/CMakeLists.txt
View file

@ -10,7 +10,6 @@ z3_add_component(simplifier
bv_simplifier_params.cpp
bv_simplifier_plugin.cpp
datatype_simplifier_plugin.cpp
distribute_forall.cpp
elim_bounds.cpp
fpa_simplifier_plugin.cpp
inj_axiom.cpp

1
contrib/cmake/src/interp/CMakeLists.txt
View file

@ -2,7 +2,6 @@ z3_add_component(interp
SOURCES
iz3base.cpp
iz3checker.cpp
iz3foci.cpp
iz3interp.cpp
iz3mgr.cpp
iz3pp.cpp

29
scripts/mk_util.py
View file

@ -96,8 +96,6 @@ VER_BUILD=None
VER_REVISION=None
PREFIX=sys.prefix
GMP=False
FOCI2=False
FOCI2LIB=''
VS_PAR=False
VS_PAR_NUM=8
GPROF=False
@ -257,13 +255,6 @@ def test_gmp(cc):
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
def test_foci2(cc,foci2lib):
if is_verbose():
print("Testing FOCI2...")
t = TempFile('tstfoci2.cpp')
t.add('#include<foci2.h>\nint main() { foci2 *f = foci2::create("lia"); return 0; }\n')
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, '-Isrc/interp', 'tstfoci2.cpp', LDFLAGS, foci2lib]) == 0
def test_openmp(cc):
if not USE_OMP:
@ -650,7 +641,6 @@ def display_help(exit_code):
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
print(" -f <path> --foci2=<path> use foci2 library at path")
print(" --noomp disable OpenMP and all features that require it.")
print(" --log-sync synchronize access to API log files to enable multi-thread API logging.")
print("")
@ -678,13 +668,13 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof',
'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync'])
except:
print("ERROR: Invalid command line option")
@ -735,9 +725,6 @@ def parse_options():
VS_PAR_NUM = int(arg)
elif opt in ('-g', '--gmp'):
GMP = True
elif opt in ('-f', '--foci2'):
FOCI2 = True
FOCI2LIB = arg
elif opt in ('-j', '--java'):
JAVA_ENABLED = True
elif opt == '--gprof':
@ -1181,7 +1168,6 @@ class ExeComponent(Component):
for dep in deps:
c_dep = get_component(dep)
out.write(' ' + c_dep.get_link_name())
out.write(' ' + FOCI2LIB)
out.write(' $(LINK_EXTRA_FLAGS)\n')
out.write('%s: %s\n\n' % (self.name, exefile))
@ -1307,7 +1293,6 @@ class DLLComponent(Component):
if dep not in self.reexports:
c_dep = get_component(dep)
out.write(' ' + c_dep.get_link_name())
out.write(' ' + FOCI2LIB)
out.write(' $(SLINK_EXTRA_FLAGS)')
if IS_WINDOWS:
out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name))
@ -2307,7 +2292,7 @@ def mk_config():
if ONLY_MAKEFILES:
return
config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC
if IS_WINDOWS:
config.write(
'CC=cl\n'
@ -2417,14 +2402,6 @@ def mk_config():
SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
else:
CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
if FOCI2:
if test_foci2(CXX,FOCI2LIB):
LDFLAGS = '%s %s' % (LDFLAGS,FOCI2LIB)
SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
else:
print("FAILED\n")
FOCI2 = False
if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
CXXFLAGS = '%s -std=c++11' % CXXFLAGS

2
src/api/java/Expr.java
View file

@ -126,7 +126,7 @@ public class Expr extends AST
if (isApp() && args.length != getNumArgs()) {
throw new Z3Exception("Number of arguments does not match");
}
return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
args.length, Expr.arrayToNative(args)));
}

6
src/api/python/z3/z3.py
View file

@ -1300,8 +1300,10 @@ class BoolSortRef(SortRef):
if isinstance(val, bool):
return BoolVal(val, self.ctx)
if __debug__:
_z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
if not is_expr(val):
_z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
if not self.eq(val.sort()):
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
return val
def subsort(self, other):

7
src/ast/ast_pp_util.cpp
View file

@ -44,8 +44,11 @@ void ast_pp_util::display_decls(std::ostream& out) {
}
n = coll.get_num_decls();
for (unsigned i = 0; i < n; ++i) {
ast_smt2_pp(out, coll.get_func_decls()[i], env);
out << "\n";
func_decl* f = coll.get_func_decls()[i];
if (f->get_family_id() == null_family_id) {
ast_smt2_pp(out, f, env);
out << "\n";
}
}
}

2
src/ast/pb_decl_plugin.cpp
View file

@ -91,7 +91,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null || logic == "QF_FD") {
if (logic == symbol::null || logic == "QF_FD" || logic == "ALL") {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));

13
src/ast/simplifier/distribute_forall.cpp → src/ast/rewriter/distribute_forall.cpp
View file

@ -20,12 +20,12 @@ Revision History:
--*/
#include"var_subst.h"
#include"ast_ll_pp.h"
#include"ast_util.h"
#include"distribute_forall.h"
#include"bool_rewriter.h"
distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) :
distribute_forall::distribute_forall(ast_manager & m) :
m_manager(m),
m_bsimp(p),
m_cache(m) {
}
@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
expr * e = get_cached(q->get_expr());
if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) {
bool_rewriter br(m_manager);
// found target for simplification
// (forall X (not (or F1 ... Fn)))
// -->
@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = or_e->get_arg(i);
expr_ref not_arg(m_manager);
// m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a.
m_bsimp.mk_not(arg, not_arg);
br.mk_not(arg, not_arg);
quantifier_ref tmp_q(m_manager);
tmp_q = m_manager.update_quantifier(q, not_arg);
expr_ref new_q(m_manager);
@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
expr_ref result(m_manager);
// m_bsimp.mk_and actually constructs a (not (or ...)) formula,
// it will also apply basic simplifications.
m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result);
br.mk_and(new_args.size(), new_args.c_ptr(), result);
cache_result(q, result);
}
else {

4
src/ast/simplifier/distribute_forall.h → src/ast/rewriter/distribute_forall.h
View file

@ -22,7 +22,6 @@ Revision History:
#define DISTRIBUTE_FORALL_H_
#include"ast.h"
#include"basic_simplifier_plugin.h"
#include"act_cache.h"
/**
@ -47,7 +46,6 @@ Revision History:
class distribute_forall {
typedef act_cache expr_map;
ast_manager & m_manager;
basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form.
ptr_vector<expr> m_todo;
expr_map m_cache;
ptr_vector<expr> m_new_args;
@ -57,7 +55,7 @@ class distribute_forall {
public:
distribute_forall(ast_manager & m, basic_simplifier_plugin & p);
distribute_forall(ast_manager & m);
/**
\brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f.

8
src/cmd_context/basic_cmds.cpp
View file

@ -622,7 +622,7 @@ public:
m_status(":status"),
m_reason_unknown(":reason-unknown"),
m_all_statistics(":all-statistics"),
m_assertion_stack_levels("assertion-stack-levels") {
m_assertion_stack_levels(":assertion-stack-levels") {
}
virtual char const * get_usage() const { return "<keyword>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "get information."; }
@ -652,7 +652,7 @@ public:
ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;
}
else if (opt == m_reason_unknown) {
ctx.regular_stream() << "(:reason-unknown \"" << ctx.reason_unknown() << "\")" << std::endl;
ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown().c_str()) << "\")" << std::endl;
}
else if (opt == m_all_statistics) {
ctx.display_statistics();
@ -852,9 +852,7 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))"));
ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals"));
// ctx.insert(alloc(builtin_cmd, "define-fun-rec", "hfun-defi", "define a function satisfying recursive equations"));
// ctx.insert(alloc(builtin_cmd, "define-funs-rec", "( hfun_decin+1 ) ( htermin+1 )", "define multiple mutually recursive functions"));
// ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(reset_assertions_cmd));
}

40
src/cmd_context/cmd_context.cpp
View file

@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_processing_pareto(false),
m_manager(m),
m_own_manager(m == 0),
m_manager_initialized(false),
@ -529,10 +530,6 @@ bool cmd_context::logic_has_fpa() const {
return !has_logic() || smt_logics::logic_has_fpa(m_logic);
}
bool cmd_context::logic_has_str() const {
return !has_logic() || m_logic == "QF_S";
}
bool cmd_context::logic_has_array() const {
return !has_logic() || smt_logics::logic_has_array(m_logic);
}
@ -637,7 +634,7 @@ bool cmd_context::set_logic(symbol const & s) {
std::string cmd_context::reason_unknown() const {
if (m_check_sat_result.get() == 0)
throw cmd_exception("state of the most recent check-sat command is not known");
return "state of the most recent check-sat command is not known";
return m_check_sat_result->reason_unknown();
}
@ -1130,6 +1127,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
}
void cmd_context::reset(bool finalize) {
m_processing_pareto = false;
m_logic = symbol::null;
m_check_sat_result = 0;
m_numeral_as_real = false;
@ -1174,6 +1172,7 @@ void cmd_context::reset(bool finalize) {
}
void cmd_context::assert_expr(expr * t) {
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
m_check_sat_result = 0;
@ -1186,6 +1185,7 @@ void cmd_context::assert_expr(expr * t) {
}
void cmd_context::assert_expr(symbol const & name, expr * t) {
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
if (!produce_unsat_cores() || name == symbol::null) {
@ -1286,6 +1286,7 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
}
void cmd_context::restore_assertions(unsigned old_sz) {
m_processing_pareto = false;
if (!has_manager()) {
// restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
SASSERT(old_sz == m_assertions.size());
@ -1303,6 +1304,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
void cmd_context::pop(unsigned n) {
m_check_sat_result = 0;
m_processing_pareto = false;
if (n == 0)
return;
unsigned lvl = m_scopes.size();
@ -1333,7 +1335,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
unsigned rlimit = m_params.m_rlimit;
scoped_watch sw(*this);
lbool r;
bool was_pareto = false, was_opt = false;
bool was_opt = false;
if (m_opt && !m_opt->empty()) {
was_opt = true;
@ -1342,21 +1344,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
scoped_ctrl_c ctrlc(eh);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(m().limit(), rlimit);
ptr_vector<expr> cnstr(m_assertions);
cnstr.append(num_assumptions, assumptions);
get_opt()->set_hard_constraints(cnstr);
if (!m_processing_pareto) {
ptr_vector<expr> cnstr(m_assertions);
cnstr.append(num_assumptions, assumptions);
get_opt()->set_hard_constraints(cnstr);
}
try {
r = get_opt()->optimize();
while (r == l_true && get_opt()->is_pareto()) {
was_pareto = true;
get_opt()->display_assignment(regular_stream());
regular_stream() << "\n";
if (get_opt()->print_model()) {
model_ref mdl;
get_opt()->get_model(mdl);
display_model(mdl);
}
r = get_opt()->optimize();
if (r == l_true && get_opt()->is_pareto()) {
m_processing_pareto = true;
}
}
catch (z3_error & ex) {
@ -1366,8 +1362,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg());
}
if (was_pareto && r == l_false) {
r = l_true;
if (m_processing_pareto && r != l_true) {
m_processing_pareto = false;
}
get_opt()->set_status(r);
}
@ -1400,7 +1396,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
validate_model();
}
validate_check_sat_result(r);
if (was_opt && r != l_false && !was_pareto) {
if (was_opt && r != l_false && !m_processing_pareto) {
get_opt()->display_assignment(regular_stream());
}

3
src/cmd_context/cmd_context.h
View file

@ -123,7 +123,6 @@ public:
virtual void display_assignment(std::ostream& out) = 0;
virtual bool is_pareto() = 0;
virtual void set_logic(symbol const& s) = 0;
virtual bool print_model() const = 0;
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
virtual void updt_params(params_ref const& p) = 0;
};
@ -161,6 +160,7 @@ protected:
status m_status;
bool m_numeral_as_real;
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_processing_pareto; // used when re-entering check-sat for pareto front.
bool m_exit_on_error;
static std::ostringstream g_error_stream;
@ -257,7 +257,6 @@ protected:
bool logic_has_array() const;
bool logic_has_datatype() const;
bool logic_has_fpa() const;
bool logic_has_str() const;
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}

75
src/interp/foci2.h
View file

@ -1,75 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
foci2.h
Abstract:
An interface class for foci2.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef FOCI2_H
#define FOCI2_H
#include <vector>
#include <string>
#ifdef _WINDOWS
#define FOCI2_EXPORT __declspec(dllexport)
#else
#define FOCI2_EXPORT __attribute__ ((visibility ("default")))
#endif
class foci2 {
public:
virtual ~foci2(){}
typedef int ast;
typedef int symb;
/** Built-in operators */
enum ops {
And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp
};
virtual symb mk_func(const std::string &s) = 0;
virtual symb mk_pred(const std::string &s) = 0;
virtual ast mk_op(ops op, const std::vector<ast> args) = 0;
virtual ast mk_op(ops op, ast) = 0;
virtual ast mk_op(ops op, ast, ast) = 0;
virtual ast mk_op(ops op, ast, ast, ast) = 0;
virtual ast mk_int(const std::string &) = 0;
virtual ast mk_rat(const std::string &) = 0;
virtual ast mk_true() = 0;
virtual ast mk_false() = 0;
virtual ast mk_app(symb,const std::vector<ast> args) = 0;
virtual bool get_func(ast, symb &) = 0;
virtual bool get_pred(ast, symb &) = 0;
virtual bool get_op(ast, ops &) = 0;
virtual bool get_true(ast id) = 0;
virtual bool get_false(ast id) = 0;
virtual bool get_int(ast id, std::string &res) = 0;
virtual bool get_rat(ast id, std::string &res) = 0;
virtual const std::string &get_symb(symb) = 0;
virtual int get_num_args(ast) = 0;
virtual ast get_arg(ast, int) = 0;
virtual void show_ast(ast) = 0;
virtual bool interpolate(const std::vector<ast> &frames, std::vector<ast> &itps, std::vector<int> parents) = 0;
FOCI2_EXPORT static foci2 *create(const std::string &);
};
#endif

25
src/interp/foci2stub/foci2.cpp
View file

@ -1,25 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
foci2.cpp
Abstract:
Fake foci2, to be replaced
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#include "foci2.h"
FOCI2_EXPORT foci2 *foci2::create(const std::string &){
return 0;
}

75
src/interp/foci2stub/foci2.h
View file

@ -1,75 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
foci2.h
Abstract:
An interface class for foci2.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef FOCI2_H
#define FOCI2_H
#include <vector>
#include <string>
#ifdef WIN32
#define FOCI2_EXPORT __declspec(dllexport)
#else
#define FOCI2_EXPORT __attribute__ ((visibility ("default")))
#endif
class foci2 {
public:
virtual ~foci2(){}
typedef int ast;
typedef int symb;
/** Built-in operators */
enum ops {
And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp
};
virtual symb mk_func(const std::string &s) = 0;
virtual symb mk_pred(const std::string &s) = 0;
virtual ast mk_op(ops op, const std::vector<ast> args) = 0;
virtual ast mk_op(ops op, ast) = 0;
virtual ast mk_op(ops op, ast, ast) = 0;
virtual ast mk_op(ops op, ast, ast, ast) = 0;
virtual ast mk_int(const std::string &) = 0;
virtual ast mk_rat(const std::string &) = 0;
virtual ast mk_true() = 0;
virtual ast mk_false() = 0;
virtual ast mk_app(symb,const std::vector<ast> args) = 0;
virtual bool get_func(ast, symb &) = 0;
virtual bool get_pred(ast, symb &) = 0;
virtual bool get_op(ast, ops &) = 0;
virtual bool get_true(ast id) = 0;
virtual bool get_false(ast id) = 0;
virtual bool get_int(ast id, std::string &res) = 0;
virtual bool get_rat(ast id, std::string &res) = 0;
virtual const std::string &get_symb(symb) = 0;
virtual int get_num_args(ast) = 0;
virtual ast get_arg(ast, int) = 0;
virtual void show_ast(ast) = 0;
virtual bool interpolate(const std::vector<ast> &frames, std::vector<ast> &itps, std::vector<int> parents) = 0;
FOCI2_EXPORT static foci2 *create(const std::string &);
};
#endif

356
src/interp/iz3foci.cpp
View file

@ -1,356 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3foci.cpp
Abstract:
Implements a secondary solver using foci2.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#include <sstream>
#include <iostream>
#include "iz3hash.h"
#include "foci2.h"
#include "iz3foci.h"
using namespace stl_ext;
class iz3foci_impl : public iz3secondary {
int frames;
int *parents;
foci2 *foci;
foci2::symb select_op;
foci2::symb store_op;
foci2::symb mod_op;
public:
iz3foci_impl(iz3mgr *mgr, int _frames, int *_parents) : iz3secondary(*mgr) {
frames = _frames;
parents = _parents;
foci = 0;
}
typedef hash_map<ast,foci2::ast> AstToNode;
AstToNode ast_to_node; // maps Z3 ast's to foci expressions
typedef hash_map<foci2::ast,ast> NodeToAst;
NodeToAst node_to_ast; // maps Z3 ast's to foci expressions
// We only use this for FuncDeclToSymbol, which has no range destructor
struct symb_hash {
size_t operator()(const symb &s) const {
return (size_t) s;
}
};
typedef hash_map<symb,foci2::symb> FuncDeclToSymbol;
FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols
typedef hash_map<foci2::symb,symb> SymbolToFuncDecl;
SymbolToFuncDecl symbol_to_func_decl; // maps symbols to Z3 func decls
int from_symb(symb func){
std::string name = string_of_symbol(func);
bool is_bool = is_bool_type(get_range_type(func));
foci2::symb f;
if(is_bool)
f = foci->mk_pred(name);
else
f = foci->mk_func(name);
symbol_to_func_decl[f] = func;
func_decl_to_symbol[func] = f;
return f;
}
// create a symbol corresponding to a DeBruijn index of a particular type
// the type has to be encoded into the name because the same index can
// occur with different types
foci2::symb make_deBruijn_symbol(int index, type ty){
std::ostringstream s;
// s << "#" << index << "#" << type;
return foci->mk_func(s.str());
}
int from_Z3_ast(ast t){
std::pair<ast,foci2::ast> foo(t,0);
std::pair<AstToNode::iterator, bool> bar = ast_to_node.insert(foo);
int &res = bar.first->second;
if(!bar.second) return res;
int nargs = num_args(t);
std::vector<foci2::ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = from_Z3_ast(arg(t,i));
switch(op(t)){
case True:
res = foci->mk_true(); break;
case False:
res = foci->mk_false(); break;
case And:
res = foci->mk_op(foci2::And,args); break;
case Or:
res = foci->mk_op(foci2::Or,args); break;
case Not:
res = foci->mk_op(foci2::Not,args[0]); break;
case Iff:
res = foci->mk_op(foci2::Iff,args); break;
case OP_OEQ: // bit of a mystery, this one...
if(args[0] == args[1]) res = foci->mk_true();
else res = foci->mk_op(foci2::Iff,args);
break;
case Ite:
if(is_bool_type(get_type(t)))
res = foci->mk_op(foci2::And,foci->mk_op(foci2::Or,foci->mk_op(foci2::Not,args[0]),args[1]),foci->mk_op(foci2::Or,args[0],args[2]));
else
res = foci->mk_op(foci2::Ite,args);
break;
case Equal:
res = foci->mk_op(foci2::Equal,args); break;
case Implies:
args[0] = foci->mk_op(foci2::Not,args[0]); res = foci->mk_op(foci2::Or,args); break;
case Xor:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Iff,args)); break;
case Leq:
res = foci->mk_op(foci2::Leq,args); break;
case Geq:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Leq,args); break;
case Gt:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Lt:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Plus:
res = foci->mk_op(foci2::Plus,args); break;
case Sub:
args[1] = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[1]); res = foci->mk_op(foci2::Plus,args); break;
case Uminus:
res = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[0]); break;
case Times:
res = foci->mk_op(foci2::Times,args); break;
case Idiv:
res = foci->mk_op(foci2::Div,args); break;
case Mod:
res = foci->mk_app(mod_op,args); break;
case Select:
res = foci->mk_app(select_op,args); break;
case Store:
res = foci->mk_app(store_op,args); break;
case Distinct:
res = foci->mk_op(foci2::Distinct,args); break;
case Uninterpreted: {
symb func = sym(t);
FuncDeclToSymbol::iterator it = func_decl_to_symbol.find(func);
foci2::symb f = (it == func_decl_to_symbol.end()) ? from_symb(func) : it->second;
if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==1) // HACK to handle Z3 labels
res = args[0];
else if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==0) // HACK to handle Z3 labels
res = foci->mk_true();
else res = foci->mk_app(f,args);
break;
}
case Numeral: {
std::string s = string_of_numeral(t);
res = foci->mk_int(s);
break;
}
case Forall:
case Exists: {
bool is_forall = op(t) == Forall;
foci2::ops qop = is_forall ? foci2::Forall : foci2::Exists;
int bvs = get_quantifier_num_bound(t);
std::vector<int> foci_bvs(bvs);
for(int i = 0; i < bvs; i++){
std::string name = get_quantifier_bound_name(t,i);
//Z3_string name = Z3_get_symbol_string(ctx,sym);
// type ty = get_quantifier_bound_type(t,i);
foci2::symb f = foci->mk_func(name);
foci2::ast v = foci->mk_app(f,std::vector<foci2::ast>());
foci_bvs[i] = v;
}
foci2::ast body = from_Z3_ast(get_quantifier_body(t));
foci_bvs.push_back(body);
res = foci->mk_op(qop,foci_bvs);
node_to_ast[res] = t; // desperate
break;
}
case Variable: { // a deBruijn index
int index = get_variable_index_value(t);
type ty = get_type(t);
foci2::symb symbol = make_deBruijn_symbol(index,ty);
res = foci->mk_app(symbol,std::vector<foci2::ast>());
break;
}
default:
{
std::cerr << "iZ3: unsupported Z3 operator in expression\n ";
print_expr(std::cerr,t);
std::cerr << "\n";
SASSERT(0 && "iZ3: unsupported Z3 operator");
}
}
return res;
}
// convert an expr to Z3 ast
ast to_Z3_ast(foci2::ast i){
std::pair<foci2::ast,ast> foo(i,ast());
std::pair<NodeToAst::iterator,bool> bar = node_to_ast.insert(foo);
if(!bar.second) return bar.first->second;
ast &res = bar.first->second;
if(i < 0){
res = mk_not(to_Z3_ast(-i));
return res;
}
// get the arguments
unsigned n = foci->get_num_args(i);
std::vector<ast> args(n);
for(unsigned j = 0; j < n; j++)
args[j] = to_Z3_ast(foci->get_arg(i,j));
// handle operators
foci2::ops o;
foci2::symb f;
std::string nval;
if(foci->get_true(i))
res = mk_true();
else if(foci->get_false(i))
res = mk_false();
else if(foci->get_op(i,o)){
switch(o){
case foci2::And:
res = make(And,args); break;
case foci2::Or:
res = make(Or,args); break;
case foci2::Not:
res = mk_not(args[0]); break;
case foci2::Iff:
res = make(Iff,args[0],args[1]); break;
case foci2::Ite:
res = make(Ite,args[0],args[1],args[2]); break;
case foci2::Equal:
res = make(Equal,args[0],args[1]); break;
case foci2::Plus:
res = make(Plus,args); break;
case foci2::Times:
res = make(Times,args); break;
case foci2::Div:
res = make(Idiv,args[0],args[1]); break;
case foci2::Leq:
res = make(Leq,args[0],args[1]); break;
case foci2::Distinct:
res = make(Distinct,args);
break;
case foci2::Tsym:
res = mk_true();
break;
case foci2::Fsym:
res = mk_false();
break;
case foci2::Forall:
case foci2::Exists:
{
int nargs = n;
std::vector<ast> bounds(nargs-1);
for(int i = 0; i < nargs-1; i++)
bounds[i] = args[i];
opr oz = o == foci2::Forall ? Forall : Exists;
res = make_quant(oz,bounds,args[nargs-1]);
}
break;
default:
SASSERT(false && "unknown built-in op");
}
}
else if(foci->get_int(i,nval)){
res = make_int(nval);
}
else if(foci->get_func(i,f)){
if(f == select_op){
SASSERT(n == 2);
res = make(Select,args[0],args[1]);
}
else if(f == store_op){
SASSERT(n == 3);
res = make(Store,args[0],args[1],args[2]);
}
else if(f == mod_op){
SASSERT(n == 2);
res = make(Mod,args[0],args[1]);
}
else {
std::pair<int,symb> foo(f,(symb)0);
std::pair<SymbolToFuncDecl::iterator,bool> bar = symbol_to_func_decl.insert(foo);
symb &func_decl = bar.first->second;
if(bar.second){
std::cout << "unknown function symbol:\n";
foci->show_ast(i);
SASSERT(0);
}
res = make(func_decl,args);
}
}
else {
std::cerr << "iZ3: unknown FOCI expression kind\n";
SASSERT(0 && "iZ3: unknown FOCI expression kind");
}
return res;
}
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
SASSERT((int)cnsts.size() == frames);
std::string lia("lia");
#ifdef _FOCI2
foci = foci2::create(lia);
#else
foci = 0;
#endif
if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n";
SASSERT(0);
}
select_op = foci->mk_func("select");
store_op = foci->mk_func("store");
mod_op = foci->mk_func("mod");
std::vector<foci2::ast> foci_cnsts(frames), foci_itps(frames-1), foci_parents;
if(parents)
foci_parents.resize(frames);
for(int i = 0; i < frames; i++){
foci_cnsts[i] = from_Z3_ast(cnsts[i]);
if(parents)
foci_parents[i] = parents[i];
}
int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents);
if(res == 0){
SASSERT((int)foci_itps.size() == frames-1);
itps.resize(frames-1);
for(int i = 0; i < frames-1; i++){
// foci->show_ast(foci_itps[i]);
itps[i] = to_Z3_ast(foci_itps[i]);
}
}
ast_to_node.clear();
node_to_ast.clear();
func_decl_to_symbol.clear();
symbol_to_func_decl.clear();
delete foci;
return res;
}
};
iz3secondary *iz3foci::create(iz3mgr *mgr, int num, int *parents){
return new iz3foci_impl(mgr,num,parents);
}

32
src/interp/iz3foci.h
View file

@ -1,32 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3foci.h
Abstract:
Implements a secondary solver using foci2.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3FOCI_H
#define IZ3FOCI_H
#include "iz3secondary.h"
/** Secondary prover based on Cadence FOCI. */
class iz3foci {
public:
static iz3secondary *create(iz3mgr *mgr, int num, int *parents);
};
#endif

30
src/interp/iz3interp.cpp
View file

@ -35,7 +35,6 @@
#include "iz3profiling.h"
#include "iz3translate.h"
#include "iz3foci.h"
#include "iz3proof.h"
#include "iz3hash.h"
#include "iz3interp.h"
@ -167,22 +166,6 @@ struct frame_reducer {
#endif
#if 0
static lbool test_secondary(context ctx,
int num,
ast *cnsts,
ast *interps,
int *parents = 0
){
iz3secondary *sp = iz3foci::create(ctx,num,parents);
std::vector<ast> frames(num), interpolants(num-1);
std::copy(cnsts,cnsts+num,frames.begin());
int res = sp->interpolate(frames,interpolants);
if(res == 0)
std::copy(interpolants.begin(),interpolants.end(),interps);
return res ? L_TRUE : L_FALSE;
}
#endif
template<class T>
struct killme {
@ -213,11 +196,7 @@ public:
const std::vector<int> &parents,
std::vector<ast> &interps
){
int num = cnsts.size();
iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0]));
int res = sp->interpolate(cnsts, interps);
if(res != 0)
throw iz3_exception("secondary failed");
throw iz3_exception("secondary interpolating prover not supported");
}
void proof_to_interpolant(z3pf proof,
@ -248,10 +227,9 @@ public:
if(is_linear(parents_vec))
parents_vec.clear();
// create a secondary prover
iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]);
sp_killer.set(sp); // kill this on exit
// secondary prover no longer supported
iz3secondary *sp = NULL;
#define BINARY_INTERPOLATION
#ifndef BINARY_INTERPOLATION
// create a translator

6
src/interp/iz3translate.h
View file

@ -53,12 +53,8 @@ class iz3translation : public iz3base {
: iz3base(mgr,_cnsts,_parents,_theory) {}
};
//#define IZ3_TRANSLATE_DIRECT2
#ifdef _FOCI2
#define IZ3_TRANSLATE_DIRECT
#else
// To use a secondary prover, define IZ3_TRANSLATE_DIRECT instead of this
#define IZ3_TRANSLATE_FULL
#endif
#endif

8
src/interp/iz3translate_direct.cpp
View file

@ -332,7 +332,7 @@ public:
}
}
// get the lits of a Z3 clause as foci terms
// get the lits of a Z3 clause as secondary prover terms
void get_Z3_lits(ast t, std::vector<ast> &lits){
opr dk = op(t);
if(dk == False)
@ -666,9 +666,9 @@ public:
#endif
// interpolate using secondary prover
profiling::timer_start("foci");
profiling::timer_start("secondary prover");
int sat = secondary->interpolate(preds,itps);
profiling::timer_stop("foci");
profiling::timer_stop("secondary prover");
std::cout << "lemma done" << std::endl;
@ -1495,7 +1495,7 @@ public:
return find_nll(new_proofs);
}
// translate a Z3 proof term into a foci proof term
// translate a Z3 proof term into a secondary prover proof term
Iproof::node translate_main(ast proof, non_local_lits *nll, bool expect_clause = true){
non_local_lits *old_nll = nll;

3
src/muz/base/rule_properties.cpp
View file

@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) {
}
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
sort_size sz = d->get_num_elements();
if (!sz.is_finite()) {
m_inf_sort.push_back(m_rule);
}
}

5
src/opt/opt_context.cpp
View file

@ -319,11 +319,6 @@ namespace opt {
return r;
}
bool context::print_model() const {
opt_params optp(m_params);
return optp.print_model();
}
void context::get_base_model(model_ref& mdl) {
mdl = m_model;
}

1
src/opt/opt_context.h
View file

@ -183,7 +183,6 @@ namespace opt {
virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;
virtual void set_model(model_ref& _m) { m_model = _m; }
virtual void get_model(model_ref& _m);
virtual void get_box_model(model_ref& _m, unsigned index);

1
src/opt/opt_params.pyg
View file

@ -7,7 +7,6 @@ def_module_params('opt',
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('print_model', BOOL, False, 'display model for satisfiable constraints'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),

35
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -130,13 +130,36 @@ public:
m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
}
bool is_literal(expr* e) const {
return
is_uninterp_const(e) ||
(m.is_not(e, e) && is_uninterp_const(e));
}
virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
m_solver.pop_to_base_level();
expr_ref_vector _assumptions(m);
obj_map<expr, expr*> asm2fml;
for (unsigned i = 0; i < sz; ++i) {
if (!is_literal(assumptions[i])) {
expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
expr_ref fml(m.mk_eq(a, assumptions[i]), m);
assert_expr(fml);
_assumptions.push_back(a);
asm2fml.insert(a, assumptions[i]);
}
else {
_assumptions.push_back(assumptions[i]);
asm2fml.insert(assumptions[i], assumptions[i]);
}
}
TRACE("sat", tout << _assumptions << "\n";);
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm);
r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@ -150,7 +173,7 @@ public:
case l_false:
// TBD: expr_dependency core is not accounted for.
if (!m_asms.empty()) {
extract_core(dep2asm);
extract_core(dep2asm, asm2fml);
}
break;
default:
@ -241,6 +264,7 @@ public:
sat::bool_var_vector bvars;
vector<sat::literal_vector> lconseq;
dep2asm_t dep2asm;
obj_map<expr, expr*> asm2fml;
m_solver.pop_to_base_level();
lbool r = internalize_formulas();
if (r != l_true) return r;
@ -251,7 +275,7 @@ public:
r = m_solver.get_consequences(m_asms, bvars, lconseq);
if (r == l_false) {
if (!m_asms.empty()) {
extract_core(dep2asm);
extract_core(dep2asm, asm2fml);
}
return r;
}
@ -569,7 +593,7 @@ private:
}
}
void extract_core(dep2asm_t& dep2asm) {
void extract_core(dep2asm_t& dep2asm, obj_map<expr, expr*> const& asm2fml) {
u_map<expr*> asm2dep;
extract_asm2dep(dep2asm, asm2dep);
sat::literal_vector const& core = m_solver.get_core();
@ -590,6 +614,9 @@ private:
for (unsigned i = 0; i < core.size(); ++i) {
expr* e = 0;
VERIFY(asm2dep.find(core[i].index(), e));
if (asm2fml.contains(e)) {
e = asm2fml.find(e);
}
m_core.push_back(e);
}
}

390
src/smt/asserted_formulas.cpp
View file

@ -43,7 +43,7 @@ Revision History:
#include"quasi_macros.h"
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_manager(m),
m(m),
m_params(p),
m_pre_simplifier(m),
m_simplifier(m),
@ -63,7 +63,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp);
SASSERT(m_bsimp != 0);
SASSERT(arith_simp != 0);
m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager);
m_macro_finder = alloc(macro_finder, m, m_macro_manager);
basic_simplifier_plugin * basic_simp = 0;
bv_simplifier_plugin * bv_simp = 0;
@ -90,16 +90,16 @@ void asserted_formulas::setup() {
}
void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) {
bsimp = alloc(basic_simplifier_plugin, m_manager);
bsimp = alloc(basic_simplifier_plugin, m);
s.register_plugin(bsimp);
asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, m_params);
asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params);
s.register_plugin(asimp);
s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params);
s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params);
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp));
}
void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {
@ -108,7 +108,7 @@ void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, pro
SASSERT(!m_inconsistent);
SASSERT(m_scopes.empty());
m_asserted_formulas.append(num_formulas, formulas);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
m_asserted_formula_prs.append(num_formulas, prs);
}
@ -125,9 +125,9 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & r
SASSERT(!result.empty());
return;
}
if (m_manager.is_false(e))
if (m.is_false(e))
m_inconsistent = true;
::push_assertion(m_manager, e, pr, result, result_prs);
::push_assertion(m, e, pr, result, result_prs);
}
void asserted_formulas::set_eliminate_and(bool flag) {
@ -145,13 +145,13 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs);
return;
}
proof_ref in_pr(_in_pr, m_manager);
expr_ref r1(m_manager);
proof_ref pr1(m_manager);
expr_ref r2(m_manager);
proof_ref pr2(m_manager);
TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";);
TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";);
proof_ref in_pr(_in_pr, m);
expr_ref r1(m);
proof_ref pr1(m);
expr_ref r2(m);
proof_ref pr2(m);
TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";);
TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";);
if (m_params.m_pre_simplifier) {
m_pre_simplifier(e, r1, pr1);
}
@ -161,14 +161,14 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
}
set_eliminate_and(false); // do not eliminate and before nnf.
m_simplifier(r1, r2, pr2);
TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";);
if (m_manager.proofs_enabled()) {
TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";);
if (m.proofs_enabled()) {
if (e == r2)
pr2 = in_pr;
else
pr2 = m_manager.mk_modus_ponens(in_pr, m_manager.mk_transitivity(pr1, pr2));
pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2));
}
TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m_manager) << "\n";);
TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";);
push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs);
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
}
@ -176,7 +176,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
void asserted_formulas::assert_expr(expr * e) {
if (inconsistent())
return;
assert_expr(e, m_manager.mk_asserted(e));
assert_expr(e, m.mk_asserted(e));
}
void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
}
void asserted_formulas::push_scope() {
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled());
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled());
TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
m_scopes.push_back(scope());
m_macro_manager.push_scope();
scope & s = m_scopes.back();
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled());
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled());
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push();
m_bv_sharing.push_scope();
@ -206,7 +206,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
m_inconsistent = s.m_inconsistent_old;
m_defined_names.pop(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
m_asserted_qhead = s.m_asserted_formulas_lim;
m_scopes.shrink(new_lvl);
@ -228,7 +228,7 @@ void asserted_formulas::reset() {
#ifdef Z3DEBUG
bool asserted_formulas::check_well_sorted() const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (!is_well_sorted(m_manager, m_asserted_formulas.get(i))) return false;
if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false;
}
return true;
}
@ -322,7 +322,7 @@ void asserted_formulas::display(std::ostream & out) const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (i == m_asserted_qhead)
out << "[HEAD] ==>\n";
out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n";
out << mk_pp(m_asserted_formulas.get(i), m) << "\n";
}
out << "inconsistent: " << inconsistent() << "\n";
}
@ -331,7 +331,7 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co
if (!m_asserted_formulas.empty()) {
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++)
ast_def_ll_pp(out, m_manager, m_asserted_formulas.get(i), pp_visited, true, false);
ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false);
out << "asserted formulas:\n";
for (unsigned i = 0; i < sz; i++)
out << "#" << m_asserted_formulas[i]->get_id() << " ";
@ -346,23 +346,23 @@ void asserted_formulas::reduce_asserted_formulas() {
if (inconsistent()) {
return;
}
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz && !inconsistent(); i++) {
expr * n = m_asserted_formulas.get(i);
SASSERT(n != 0);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_simplifier(n, new_n, new_pr);
TRACE("reduce_asserted_formulas", tout << mk_pp(n, m_manager) << " -> " << mk_pp(new_n, m_manager) << "\n";);
TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
if (canceled()) {
@ -376,15 +376,15 @@ void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proo
SASSERT(!inconsistent() || !new_exprs.empty());
m_asserted_formulas.shrink(m_asserted_qhead);
m_asserted_formulas.append(new_exprs);
if (m_manager.proofs_enabled()) {
if (m.proofs_enabled()) {
m_asserted_formula_prs.shrink(m_asserted_qhead);
m_asserted_formula_prs.append(new_prs);
}
}
void asserted_formulas::find_macros_core() {
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned sz = m_asserted_formulas.size();
m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
@ -407,9 +407,9 @@ void asserted_formulas::expand_macros() {
void asserted_formulas::apply_quasi_macros() {
IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
TRACE("before_quasi_macros", display(tout););
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
quasi_macros proc(m_manager, m_macro_manager, m_simplifier);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
quasi_macros proc(m, m_macro_manager, m_simplifier);
while (proc(m_asserted_formulas.size() - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
@ -424,27 +424,27 @@ void asserted_formulas::apply_quasi_macros() {
void asserted_formulas::nnf_cnf() {
IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";);
nnf apply_nnf(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector push_todo(m_manager);
proof_ref_vector push_todo_prs(m_manager);
nnf apply_nnf(m, m_defined_names);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
expr_ref_vector push_todo(m);
proof_ref_vector push_todo_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";);
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref r1(m_manager);
proof_ref pr1(m_manager);
CASSERT("well_sorted",is_well_sorted(m_manager, n));
expr_ref r1(m);
proof_ref pr1(m);
CASSERT("well_sorted",is_well_sorted(m, n));
push_todo.reset();
push_todo_prs.reset();
apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
CASSERT("well_sorted",is_well_sorted(m_manager, r1));
pr = m_manager.mk_modus_ponens(pr, pr1);
CASSERT("well_sorted",is_well_sorted(m, r1));
pr = m.mk_modus_ponens(pr, pr1);
push_todo.push_back(r1);
push_todo_prs.push_back(pr);
@ -456,13 +456,13 @@ void asserted_formulas::nnf_cnf() {
expr * n = push_todo.get(k);
proof * pr = 0;
m_simplifier(n, r1, pr1);
CASSERT("well_sorted",is_well_sorted(m_manager, r1));
CASSERT("well_sorted",is_well_sorted(m, r1));
if (canceled()) {
return;
}
if (m_manager.proofs_enabled())
pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1);
if (m.proofs_enabled())
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
else
pr = 0;
push_assertion(r1, pr, new_exprs, new_prs);
@ -476,23 +476,23 @@ void asserted_formulas::NAME() {
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(LABEL, tout << "before:\n"; display(tout);); \
FUNCTOR_DEF; \
expr_ref_vector new_exprs(m_manager); \
proof_ref_vector new_prs(m_manager); \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
expr_ref new_n(m); \
functor(n, new_n); \
TRACE("simplifier_simple_step", tout << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); \
TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m_manager.proofs_enabled()) { \
proof_ref new_pr(m_manager); \
new_pr = m_manager.mk_rewrite_star(n, new_n, 0, 0); \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
else if (m.proofs_enabled()) { \
proof_ref new_pr(m); \
new_pr = m.mk_rewrite_star(n, new_n, 0, 0); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
@ -505,7 +505,7 @@ void asserted_formulas::NAME() {
TRACE(LABEL, display(tout);); \
}
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall");
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall");
void asserted_formulas::reduce_and_solve() {
IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
@ -516,22 +516,22 @@ void asserted_formulas::reduce_and_solve() {
void asserted_formulas::infer_patterns() {
IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
TRACE("before_pattern_inference", display(tout););
pattern_inference infer(m_manager, m_params);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
pattern_inference infer(m, m_params);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
infer(n, new_n, new_pr);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
else if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
else {
@ -554,16 +554,16 @@ void asserted_formulas::commit(unsigned new_qhead) {
void asserted_formulas::eliminate_term_ite() {
IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";);
TRACE("before_elim_term_ite", display(tout););
elim_term_ite elim(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
elim_term_ite elim(m, m_defined_names);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
elim(n, new_exprs, new_prs, new_n, new_pr);
SASSERT(new_n.get() != 0);
DEBUG_CODE({
@ -574,8 +574,8 @@ void asserted_formulas::eliminate_term_ite() {
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
else if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
else {
@ -602,31 +602,31 @@ void asserted_formulas::propagate_values() {
// - new_exprs2 is the set R
//
// The loop also updates the m_cache. It adds the entries x -> n to it.
expr_ref_vector new_exprs1(m_manager);
proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager);
expr_ref_vector new_exprs1(m);
proof_ref_vector new_prs1(m);
expr_ref_vector new_exprs2(m);
proof_ref_vector new_prs2(m);
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++) {
expr_ref n(m_asserted_formulas.get(i), m_manager);
proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager);
TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
expr_ref n(m_asserted_formulas.get(i), m);
proof_ref pr(m_asserted_formula_prs.get(i, 0), m);
TRACE("simplifier", tout << mk_pp(n, m) << "\n";);
expr* lhs, *rhs;
if (m_manager.is_eq(n, lhs, rhs) &&
(m_manager.is_value(lhs) || m_manager.is_value(rhs))) {
if (m_manager.is_value(lhs)) {
if (m.is_eq(n, lhs, rhs) &&
(m.is_value(lhs) || m.is_value(rhs))) {
if (m.is_value(lhs)) {
std::swap(lhs, rhs);
n = m_manager.mk_eq(lhs, rhs);
pr = m_manager.mk_symmetry(pr);
n = m.mk_eq(lhs, rhs);
pr = m.mk_symmetry(pr);
}
if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (i >= m_asserted_qhead) {
new_exprs1.push_back(n);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
new_prs1.push_back(pr);
}
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n";
if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";);
m_simplifier.cache_result(lhs, rhs, pr);
found = true;
continue;
@ -634,7 +634,7 @@ void asserted_formulas::propagate_values() {
}
if (i >= m_asserted_qhead) {
new_exprs2.push_back(n);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
new_prs2.push_back(pr);
}
}
@ -646,14 +646,14 @@ void asserted_formulas::propagate_values() {
for (unsigned i = 0; i < sz; i++) {
expr * n = new_exprs2.get(i);
proof * pr = new_prs2.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_simplifier(n, new_n, new_pr);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs1, new_prs1);
}
else {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs1, new_prs1);
}
}
@ -677,25 +677,25 @@ void asserted_formulas::propagate_booleans() {
cont = false;
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m_manager.proofs_enabled()) { \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m_manager.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m_manager.mk_false(), m_manager.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m_manager.mk_true(), m_manager.mk_iff_true(new_pr)); \
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \
}
for (; i < sz; i++) {
PROCESS();
@ -715,57 +715,57 @@ void asserted_formulas::propagate_booleans() {
}
#define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \
bool asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m_manager); \
proof_ref_vector new_prs(m_manager); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m_manager.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m_manager.mk_rewrite(n, new_n); \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
bool asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
proof * asserted_formulas::get_inconsistency_proof() const {
if (!inconsistent())
return 0;
if (!m_manager.proofs_enabled())
if (!m.proofs_enabled())
return 0;
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = m_asserted_formulas.get(i);
if (m_manager.is_false(f))
if (m.is_false(f))
return m_asserted_formula_prs.get(i);
}
UNREACHABLE();
@ -780,14 +780,14 @@ void asserted_formulas::refine_inj_axiom() {
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
if (is_quantifier(n) && simplify_inj_axiom(m_manager, to_quantifier(n), new_n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";);
expr_ref new_n(m);
if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);
m_asserted_formulas.set(i, new_n);
if (m_manager.proofs_enabled()) {
proof_ref new_pr(m_manager);
new_pr = m_manager.mk_rewrite(n, new_n);
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
if (m.proofs_enabled()) {
proof_ref new_pr(m);
new_pr = m.mk_rewrite(n, new_n);
new_pr = m.mk_modus_ponens(pr, new_pr);
m_asserted_formula_prs.set(i, new_pr);
}
}
@ -797,36 +797,36 @@ void asserted_formulas::refine_inj_axiom() {
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \
IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m_manager.proofs_enabled()) { \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \
IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite");
LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite");
@ -848,12 +848,12 @@ void asserted_formulas::max_bv_sharing() {
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_bv_sharing(n, new_n, new_pr);
m_asserted_formulas.set(i, new_n);
if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
m_asserted_formula_prs.set(i, new_pr);
}
}

6
src/smt/asserted_formulas.h
View file

@ -35,7 +35,7 @@ class arith_simplifier_plugin;
class bv_simplifier_plugin;
class asserted_formulas {
ast_manager & m_manager;
ast_manager & m;
smt_params & m_params;
simplifier m_pre_simplifier;
simplifier m_simplifier;
@ -94,7 +94,7 @@ class asserted_formulas {
unsigned get_total_size() const;
bool has_bv() const;
void max_bv_sharing();
bool canceled() { return m_manager.canceled(); }
bool canceled() { return m.canceled(); }
public:
asserted_formulas(ast_manager & m, smt_params & p);
@ -115,7 +115,7 @@ public:
void commit();
void commit(unsigned new_qhead);
expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);

1
src/smt/params/smt_params_helper.pyg
View file

@ -44,6 +44,7 @@ def_module_params(module_name='smt',
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),

3
src/smt/params/theory_arith_params.cpp
View file

@ -35,6 +35,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_ignore_int = p.arith_ignore_int();
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
}
@ -85,4 +86,4 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_arith_euclidean_solver);
}
}

2
src/smt/theory_lra.cpp
View file

@ -487,7 +487,7 @@ namespace smt {
result = m_theory_var2var_index[v];
}
if (result == UINT_MAX) {
result = m_solver->add_var(v);
result = m_solver->add_var(v); // TBD: is_int(v);
m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v);

8
src/smt/theory_str.cpp
View file

@ -494,6 +494,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const(name.c_str(), string_sort);
m_trail.push_back(a);
TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
<< "this->get_family_id() = " << this->get_family_id() << std::endl;);
@ -507,7 +508,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
m_trail.push_back(a);
variable_set.insert(a);
internal_variable_set.insert(a);
track_variable_scope(a);
@ -521,6 +521,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const("regex", string_sort);
m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
@ -529,7 +530,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
m_trail.push_back(a);
variable_set.insert(a);
//internal_variable_set.insert(a);
regex_variable_set.insert(a);
@ -7304,7 +7304,7 @@ namespace smt {
TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
}
}
} else if (ex_sort == bool_sort) {
} else if (ex_sort == bool_sort && !is_quantifier(ex)) {
TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of sort Bool" << std::endl;);
// set up axioms for boolean terms
@ -7351,7 +7351,7 @@ namespace smt {
// if expr is an application, recursively inspect all arguments
if (is_app(ex)) {
app * term = (app*)ex;
app * term = to_app(ex);
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
set_up_axioms(term->get_arg(i));

2
src/solver/smt_logics.cpp
View file

@ -153,5 +153,5 @@ bool smt_logics::logic_has_pb(symbol const& s) {
}
bool smt_logics::logic_has_datatype(symbol const& s) {
return s == "QF_FD";
return s == "QF_FD" || s == "ALL";
}

16
src/test/lp.cpp
View file

@ -1159,12 +1159,14 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
lp_solver<double, double> * solver = reader.create_solver(dual);
setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
if (dual) {
std::cout << "solving for dual" << std::endl;
}
solver->find_maximal_solution();
int span = get_millisecond_span(begin);
sw.stop();
double span = sw.get_seconds();
std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
if (solver->get_status() == lp_status::OPTIMAL) {
if (reader.column_names().size() < 20) {
@ -1213,7 +1215,8 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
if (reader.is_ok()) {
auto * solver = reader.create_solver(dual);
setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
solver->find_maximal_solution();
std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
@ -1227,7 +1230,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
}
std::cout << "cost = " << cost.get_double() << std::endl;
}
std::cout << "processed in " << get_millisecond_span(begin) / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
delete solver;
} else {
std::cout << "cannot process " << file_name << std::endl;
@ -2426,9 +2429,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl;
return;
}
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
lp_status status = solver->solve();
std::cout << "status is " << lp_status_to_string(status) << ", processed for " << get_millisecond_span(begin) / 1000.0 <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
std::cout << "status is " << lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
if (solver->get_status() == INFEASIBLE) {
vector<std::pair<lean::mpq, constraint_index>> evidence;
solver->get_infeasibility_explanation(evidence);

4
src/util/lp/lp_primal_simplex.h
View file

@ -55,10 +55,6 @@ public:
void set_core_solver_bounds();
void update_time_limit_from_starting_time(int start_time) {
this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.);
}
void find_maximal_solution();
void fill_A_x_and_basis_for_stage_one_total_inf();

2
src/util/lp/lp_primal_simplex.hpp
View file

@ -152,7 +152,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::set_core_solver_
template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_solution() {
int preprocessing_start_time = get_millisecond_count();
if (this->problem_is_empty()) {
this->m_status = lp_status::EMPTY;
return;
@ -169,7 +168,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
fill_acceptable_values_for_x();
this->count_slacks_and_artificials();
set_core_solver_bounds();
update_time_limit_from_starting_time(preprocessing_start_time);
solve_with_total_inf();
}

15
src/util/lp/lp_settings.h
View file

@ -8,9 +8,9 @@
#include <string>
#include <algorithm>
#include <limits>
#include <sys/timeb.h>
#include <iomanip>
#include "util/lp/lp_utils.h"
#include "util/stopwatch.h"
namespace lean {
typedef unsigned var_index;
@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f
template <typename X> bool is_epsilon_small(const X & v, const double& eps); // forward definition
int get_millisecond_count();
int get_millisecond_span(int start_time);
class lp_resource_limit {
public:
virtual bool get_cancel_flag() = 0;
@ -92,12 +88,13 @@ struct lp_settings {
private:
class default_lp_resource_limit : public lp_resource_limit {
lp_settings& m_settings;
int m_start_time;
stopwatch m_sw;
public:
default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {}
default_lp_resource_limit(lp_settings& s): m_settings(s) {
m_sw.start();
}
virtual bool get_cancel_flag() {
int span_in_mills = get_millisecond_span(m_start_time);
return (span_in_mills / 1000.0 > m_settings.time_limit);
return (m_sw.get_current_seconds() > m_settings.time_limit);
}
};

13
src/util/lp/lp_settings.hpp
View file

@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) {
lean_unreachable();
return lp_status::UNKNOWN; // it is unreachable
}
int get_millisecond_count() {
timeb tb;
ftime(&tb);
return tb.millitm + (tb.time & 0xfffff) * 1000;
}
int get_millisecond_span(int start_time) {
int span = get_millisecond_count() - start_time;
if (span < 0)
span += 0x100000 * 1000;
return span;
}
template <typename T>

8
src/util/lp/matrix.hpp
View file

@ -58,8 +58,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
unsigned r = 0;
for (unsigned i = 0; i < A.size(); i++) {
vector<std::string> & t = A[i];
std::string str= t[j];
unsigned s = str.size();
std::string str = t[j];
unsigned s = static_cast<unsigned>(str.size());
if (r < s) {
r = s;
}
@ -69,8 +69,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
void print_matrix_with_widths(vector<vector<std::string>> & A, vector<unsigned> & ws, std::ostream & out) {
for (unsigned i = 0; i < A.size(); i++) {
for (unsigned j = 0; j < A[i].size(); j++) {
print_blanks(ws[j] - A[i][j].size(), out);
for (unsigned j = 0; j < static_cast<unsigned>(A[i].size()); j++) {
print_blanks(ws[j] - static_cast<unsigned>(A[i][j].size()), out);
out << A[i][j] << " ";
}
out << std::endl;

6
src/util/lp/sparse_matrix.hpp
View file

@ -1050,8 +1050,8 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
if (i_inv < k) continue;
unsigned j_inv = adjust_column_inverse(j);
if (j_inv < k) continue;
int small = elem_is_too_small(i, j, c_partial_pivoting);
if (!small) {
int _small = elem_is_too_small(i, j, c_partial_pivoting);
if (!_small) {
#ifdef LEAN_DEBUG
// if (!really_best_pivot(i, j, c_partial_pivoting, k)) {
// print_active_matrix(k);
@ -1063,7 +1063,7 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
j = j_inv;
return true;
}
if (small != 2) { // 2 means that the pair is not in the matrix
if (_small != 2) { // 2 means that the pair is not in the matrix
pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j));
}
}