diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index e146be973..3282fa2ba 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -1,5 +1,10 @@
RELEASE NOTES
+Version 4.3.2
+=============
+
+- Added get_version() and get_version_string() to Z3Py
+
Version 4.3.1
=============
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index cb1dae205..4ef6efd11 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
- set_version(4, 3, 1, 0)
+ set_version(4, 3, 2, 0)
add_lib('util', [])
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
@@ -30,7 +30,7 @@ def init_project_def():
# Simplifier module will be deleted in the future.
# It has been replaced with rewriter module.
add_lib('simplifier', ['rewriter', 'front_end_params'], 'ast/simplifier')
- add_lib('normal_forms', ['rewriter', 'simplifier'], 'ast/normal_forms')
+ add_lib('normal_forms', ['rewriter', 'front_end_params'], 'ast/normal_forms')
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic')
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
@@ -41,7 +41,7 @@ def init_project_def():
add_lib('cmd_context', ['solver', 'rewriter'])
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
- add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
+ add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
add_lib('macros', ['simplifier', 'front_end_params'], 'ast/macros')
add_lib('proof_checker', ['rewriter', 'front_end_params'], 'ast/proof_checker')
add_lib('bit_blaster', ['rewriter', 'simplifier', 'front_end_params'], 'ast/rewriter/bit_blaster')
@@ -68,6 +68,7 @@ def init_project_def():
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
reexports=['api'],
dll_name='libz3',
+ static=build_static_lib(),
export_files=API_files)
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 54f1931e5..6828dd8f9 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -40,6 +40,7 @@ Z3PY_SRC_DIR=None
VS_PROJ = False
TRACE = False
DOTNET_ENABLED=False
+STATIC_LIB=False
VER_MAJOR=None
VER_MINOR=None
@@ -56,6 +57,9 @@ def set_version(major, minor, build, revision):
def get_version():
return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
+def build_static_lib():
+ return STATIC_LIB
+
def is_cr_lf(fname):
# Check whether text files use cr/lf
f = open(fname, 'r')
@@ -120,11 +124,12 @@ def display_help():
print " -v, --vsproj generate Visual Studio Project Files."
print " -t, --trace enable tracing in release mode."
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules."
+ print " --staticlib build Z3 static library."
exit(0)
# 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, DOTNET_ENABLED
+ global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED, STATIC_LIB
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=',
'debug',
'silent',
@@ -134,7 +139,8 @@ def parse_options():
'showcpp',
'vsproj',
'trace',
- 'nodotnet'
+ 'nodotnet',
+ 'staticlib'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@@ -161,6 +167,8 @@ def parse_options():
TRACE = True
elif opt in ('-n', '--nodotnet'):
DOTNET_ENABLED = False
+ elif opt in ('--staticlib'):
+ STATIC_LIB = True
else:
raise MKException("Invalid command line option '%s'" % opt)
@@ -370,6 +378,10 @@ class Component:
def require_def_file(self):
return False
+ # Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
+ def require_mem_initializer(self):
+ return False
+
def mk_install(self, out):
return
@@ -482,6 +494,9 @@ class ExeComponent(Component):
def require_install_tactics(self):
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
+ def require_mem_initializer(self):
+ return True
+
# All executables are included in the all: rule
def main_component(self):
return True
@@ -492,9 +507,8 @@ class ExeComponent(Component):
out.write('\t@cp %s $(PREFIX)/bin/%s\n' % (exefile, exefile))
def mk_uninstall(self, out):
- if self.install:
- exefile = '%s$(EXE_EXT)' % self.exe_name
- out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
+ exefile = '%s$(EXE_EXT)' % self.exe_name
+ out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
def mk_win_dist(self, build_path, dist_path):
if self.install:
@@ -511,7 +525,7 @@ class ExtraExeComponent(ExeComponent):
return False
class DLLComponent(Component):
- def __init__(self, name, dll_name, path, deps, export_files, reexports, install):
+ def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static):
Component.__init__(self, name, path, deps)
if dll_name == None:
dll_name = name
@@ -519,6 +533,7 @@ class DLLComponent(Component):
self.export_files = export_files
self.reexports = reexports
self.install = install
+ self.static = static
def mk_makefile(self, out):
Component.mk_makefile(self, out)
@@ -556,15 +571,46 @@ class DLLComponent(Component):
if IS_WINDOWS:
out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name))
out.write('\n')
- out.write('%s: %s\n\n' % (self.name, dllfile))
+ if self.static:
+ self.mk_static(out)
+ libfile = '%s$(LIB_EXT)' % self.dll_name
+ out.write('%s: %s %s\n\n' % (self.name, dllfile, libfile))
+ else:
+ out.write('%s: %s\n\n' % (self.name, dllfile))
- # All DLLs are included in the all: rule
+ def mk_static(self, out):
+ # generate rule for lib
+ objs = []
+ for cppfile in get_cpp_files(self.src_dir):
+ objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
+ objs.append(objfile)
+ # we have to "reexport" all object files
+ for dep in self.deps:
+ dep = get_component(dep)
+ for cppfile in get_cpp_files(dep.src_dir):
+ objfile = '%s/%s$(OBJ_EXT)' % (dep.build_dir, os.path.splitext(cppfile)[0])
+ objs.append(objfile)
+ libfile = '%s$(LIB_EXT)' % self.dll_name
+ out.write('%s:' % libfile)
+ for obj in objs:
+ out.write(' ')
+ out.write(obj)
+ out.write('\n')
+ out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
+ for obj in objs:
+ out.write(' ')
+ out.write(obj)
+ out.write('\n')
+
def main_component(self):
- return True
+ return self.install
def require_install_tactics(self):
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
+ def require_mem_initializer(self):
+ return True
+
def require_def_file(self):
return IS_WINDOWS and self.export_files
@@ -573,18 +619,27 @@ class DLLComponent(Component):
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('\t@cp %s $(PREFIX)/lib/%s\n' % (dllfile, dllfile))
out.write('\t@cp %s %s/%s\n' % (dllfile, PYTHON_PACKAGE_DIR, dllfile))
+ if self.static:
+ libfile = '%s$(LIB_EXT)' % self.dll_name
+ out.write('\t@cp %s $(PREFIX)/lib/%s\n' % (libfile, libfile))
+
def mk_uninstall(self, out):
- if self.install:
- dllfile = '%s$(SO_EXT)' % self.dll_name
- out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
- out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
+ dllfile = '%s$(SO_EXT)' % self.dll_name
+ out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
+ out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
+ libfile = '%s$(LIB_EXT)' % self.dll_name
+ out.write('\t@rm -f $(PREFIX)/lib/%s\n' % libfile)
def mk_win_dist(self, build_path, dist_path):
if self.install:
mk_dir('%s/bin' % dist_path)
shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
'%s/bin/%s.dll' % (dist_path, self.dll_name))
+ if self.static:
+ mk_dir('%s/bin' % dist_path)
+ shutil.copy('%s/%s.lib' % (build_path, self.dll_name),
+ '%s/bin/%s.lib' % (dist_path, self.dll_name))
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@@ -763,8 +818,8 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
c = ExtraExeComponent(name, exe_name, path, deps, install)
reg_component(name, c)
-def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True):
- c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install)
+def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False):
+ c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static)
reg_component(name, c)
def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None):
@@ -882,6 +937,7 @@ def mk_auto_src():
if not ONLY_MAKEFILES:
mk_pat_db()
mk_all_install_tactic_cpps()
+ mk_all_mem_initializer_cpps()
# TODO: delete after src/ast/pattern/expr_pattern_match
# database.smt ==> database.h
@@ -1054,6 +1110,60 @@ def mk_all_install_tactic_cpps():
cnames.append(c.name)
mk_install_tactic_cpp(cnames, c.src_dir)
+# Generate an mem_initializer.cpp at path.
+# This file implements the procedures
+# void mem_initialize()
+# void mem_finalize()
+# This procedures are invoked by the Z3 memory_manager
+def mk_mem_initializer_cpp(cnames, path):
+ initializer_cmds = []
+ finalizer_cmds = []
+ fullname = '%s/mem_initializer.cpp' % path
+ fout = open(fullname, 'w')
+ fout.write('// Automatically generated file.\n')
+ initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
+ finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
+ for cname in cnames:
+ c = get_component(cname)
+ h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
+ for h_file in h_files:
+ added_include = False
+ fin = open("%s/%s" % (c.src_dir, h_file), 'r')
+ for line in fin:
+ m = initializer_pat.match(line)
+ if m:
+ if not added_include:
+ added_include = True
+ fout.write('#include"%s"\n' % h_file)
+ initializer_cmds.append(m.group(1))
+ m = finalizer_pat.match(line)
+ if m:
+ if not added_include:
+ added_include = True
+ fout.write('#include"%s"\n' % h_file)
+ finalizer_cmds.append(m.group(1))
+ fout.write('void mem_initialize() {\n')
+ for cmd in initializer_cmds:
+ fout.write(cmd)
+ fout.write('\n')
+ fout.write('}\n')
+ fout.write('void mem_finalize() {\n')
+ for cmd in finalizer_cmds:
+ fout.write(cmd)
+ fout.write('\n')
+ fout.write('}\n')
+ if VERBOSE:
+ print "Generated '%s'" % fullname
+
+def mk_all_mem_initializer_cpps():
+ if not ONLY_MAKEFILES:
+ for c in get_components():
+ if c.require_mem_initializer():
+ cnames = []
+ cnames.extend(c.deps)
+ cnames.append(c.name)
+ mk_mem_initializer_cpp(cnames, c.src_dir)
+
# Generate a .def based on the files at c.export_files slot.
def mk_def_file(c):
pat1 = re.compile(".*Z3_API.*")
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 394df7a17..7674e8676 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -26,6 +26,9 @@ Revision History:
#include"datalog_parser.h"
#include"cancel_eh.h"
#include"scoped_timer.h"
+#include"dl_cmds.h"
+#include"cmd_context.h"
+#include"smt2parser.h"
namespace api {
@@ -124,55 +127,6 @@ namespace api {
return str.str();
}
- void fixedpoint_context::simplify_rules(
- unsigned num_rules, expr* const* rules,
- unsigned num_outputs, func_decl* const* outputs, expr_ref_vector& result) {
- ast_manager& m = m_context.get_manager();
-
- datalog::context ctx(m, m_context.get_fparams());
- for (unsigned i = 0; i < num_rules; ++i) {
- expr* rule = rules[i], *body, *head;
- while (true) {
- if (is_quantifier(rule)) {
- rule = to_quantifier(rule)->get_expr();
- }
- else if (m.is_implies(rule, body, head)) {
- rule = head;
- }
- else {
- break;
- }
- }
- if (is_app(rule)) {
- func_decl* r = to_app(rule)->get_decl();
- if (!ctx.is_predicate(r)) {
- ctx.register_predicate(r);
- if (num_outputs == 0) {
- ctx.set_output_predicate(r);
- }
- }
- }
- }
- for (unsigned i = 0; i < num_outputs; ++i) {
- ctx.set_output_predicate(outputs[i]);
- }
- for (unsigned i = 0; i < num_rules; ++i) {
- expr* rule = rules[i];
- ctx.add_rule(rule, symbol::null);
- }
- model_converter_ref mc; // not exposed.
- proof_converter_ref pc; // not exposed.
- ctx.apply_default_transformation(mc, pc);
- datalog::rule_set const& new_rules = ctx.get_rules();
- datalog::rule_set::iterator it = new_rules.begin(), end = new_rules.end();
- for (; it != end; ++it) {
- datalog::rule* r = *it;
- expr_ref fml(m);
- r->to_formula(fml);
- result.push_back(fml);
- }
- }
-
};
extern "C" {
@@ -384,6 +338,62 @@ extern "C" {
Z3_CATCH_RETURN("");
}
+ Z3_ast_vector Z3_fixedpoint_from_stream(
+ Z3_context c,
+ Z3_fixedpoint d,
+ std::istream& s) {
+ ast_manager& m = mk_c(c)->m();
+ dl_collected_cmds coll(m);
+ cmd_context ctx(&mk_c(c)->fparams(), false, &m);
+ install_dl_collect_cmds(coll, ctx);
+ ctx.set_ignore_check(true);
+ if (!parse_smt2_commands(ctx, s)) {
+ SET_ERROR_CODE(Z3_PARSER_ERROR);
+ return 0;
+ }
+
+ Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+ mk_c(c)->save_object(v);
+ for (unsigned i = 0; i < coll.m_queries.size(); ++i) {
+ v->m_ast_vector.push_back(coll.m_queries[i].get());
+ }
+ for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
+ to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get());
+ }
+ for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
+ to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
+ }
+ return of_ast_vector(v);
+ }
+
+ Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
+ Z3_context c,
+ Z3_fixedpoint d,
+ Z3_string s) {
+ Z3_TRY;
+ LOG_Z3_fixedpoint_from_string(c, d, s);
+ std::string str(s);
+ std::istringstream is(str);
+ RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
+ Z3_CATCH_RETURN(0);
+ }
+
+ Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
+ Z3_context c,
+ Z3_fixedpoint d,
+ Z3_string s) {
+ Z3_TRY;
+ LOG_Z3_fixedpoint_from_file(c, d, s);
+ std::ifstream is(s);
+ if (!is) {
+ SET_ERROR_CODE(Z3_PARSER_ERROR);
+ RETURN_Z3(0);
+ }
+ RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
+ Z3_CATCH_RETURN(0);
+ }
+
+
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d) {
Z3_TRY;
LOG_Z3_fixedpoint_get_statistics(c, d);
@@ -419,6 +429,27 @@ extern "C" {
Z3_CATCH;
}
+
+ Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
+ Z3_context c,
+ Z3_fixedpoint d)
+ {
+ Z3_TRY;
+ LOG_Z3_fixedpoint_get_rules(c, d);
+ ast_manager& m = mk_c(c)->m();
+ Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+ mk_c(c)->save_object(v);
+ datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules();
+ datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+ for (; it != end; ++it) {
+ expr_ref fml(m);
+ (*it)->to_formula(fml);
+ v->m_ast_vector.push_back(fml);
+ }
+ RETURN_Z3(of_ast_vector(v));
+ Z3_CATCH_RETURN(0);
+ }
+
void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) {
Z3_TRY;
@@ -435,31 +466,6 @@ extern "C" {
Z3_CATCH;
}
- Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
- Z3_context c,
- Z3_fixedpoint d,
- unsigned num_rules,
- Z3_ast _rules[],
- unsigned num_outputs,
- Z3_func_decl _outputs[]) {
- Z3_TRY;
- LOG_Z3_fixedpoint_simplify_rules(c, d, num_rules, _rules, num_outputs, _outputs);
- RESET_ERROR_CODE();
- expr** rules = (expr**)_rules;
- func_decl** outputs = (func_decl**)_outputs;
- ast_manager& m = mk_c(c)->m();
- expr_ref_vector result(m);
- to_fixedpoint_ref(d)->simplify_rules(num_rules, rules, num_outputs, outputs, result);
- Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
- mk_c(c)->save_object(v);
- for (unsigned i = 0; i < result.size(); ++i) {
- v->m_ast_vector.push_back(result[i].get());
- }
- RETURN_Z3(of_ast_vector(v));
- Z3_CATCH_RETURN(0)
- }
-
-
void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state) {
Z3_TRY;
// not logged
diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 1d6bb995a..97bedfc9b 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -62,9 +62,6 @@ namespace api {
void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
void updt_params(params_ref const& p) { m_context.updt_params(p); }
- void simplify_rules(
- unsigned num_rules, expr* const* rules,
- unsigned num_outputs, func_decl* const* outputs, expr_ref_vector& result);
};
};
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 3e04e6169..c8a677196 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -261,6 +261,23 @@ namespace Microsoft.Z3
AST.ArrayLength(queries), AST.ArrayToNative(queries));
}
+ ///
+ /// Retrieve set of rules added to fixedpoint context.
+ ///
+ public BoolExpr[] Rules {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
+ uint n = v.Size;
+ BoolExpr[] res = new BoolExpr[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = new BoolExpr(Context, v[i].NativeObject);
+ return res;
+ }
+ }
+
#region Internal
internal Fixedpoint(Context ctx, IntPtr obj)
diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs
index cdec553fb..1ac6cb520 100644
--- a/src/api/dotnet/Properties/AssemblyInfo.cs
+++ b/src/api/dotnet/Properties/AssemblyInfo.cs
@@ -34,6 +34,6 @@ using System.Security.Permissions;
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")]
-[assembly: AssemblyVersion("4.3.1.0")]
-[assembly: AssemblyFileVersion("4.3.1.0")]
+[assembly: AssemblyVersion("4.3.2.0")]
+[assembly: AssemblyFileVersion("4.3.2.0")]
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index f3de4258a..3e73e9b1a 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -49,6 +49,22 @@ def enable_trace(msg):
def disable_trace(msg):
Z3_disable_trace(msg)
+def get_version_string():
+ major = ctypes.c_uint(0)
+ minor = ctypes.c_uint(0)
+ build = ctypes.c_uint(0)
+ rev = ctypes.c_uint(0)
+ Z3_get_version(major, minor, build, rev)
+ return "%s.%s.%s" % (major.value, minor.value, build.value)
+
+def get_version():
+ major = ctypes.c_uint(0)
+ minor = ctypes.c_uint(0)
+ build = ctypes.c_uint(0)
+ rev = ctypes.c_uint(0)
+ Z3_get_version(major, minor, build, rev)
+ return (major.value, minor.value, build.value, rev.value)
+
# We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com
def _z3_assert(cond, msg):
@@ -6102,7 +6118,6 @@ class Fixedpoint(Z3PPObject):
"""Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
-
def register_relation(self, *relations):
"""Register relation as recursive"""
relations = _get_args(relations)
@@ -6119,16 +6134,35 @@ class Fixedpoint(Z3PPObject):
args[i] = representations[i]
Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
+ def parse_string(self, s):
+ """Parse rules and queries from a string"""
+ return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
+
+ def parse_file(self, f):
+ """Parse rules and queries from a file"""
+ return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
+
+ def get_rules(self):
+ """retrieve rules that have been added to fixedpoint context"""
+ return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
+
def __repr__(self):
"""Return a formatted string with all added rules and constraints."""
return self.sexpr()
def sexpr(self):
- """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
-
+ """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
"""
- return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
+ return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
+ def to_string(self, queries):
+ """Return a formatted string (in Lisp-like format) with all added constraints.
+ We say the string is in s-expression format.
+ Include also queries.
+ """
+ args, len = _to_ast_array(queries)
+ return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
+
def statistics(self):
"""Return statistics for the last `query()`.
"""
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 8d00fb044..4a28807f1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5688,19 +5688,13 @@ END_MLAPI_EXCLUDE
__in_ecount(num_relations) Z3_symbol const relation_kinds[]);
/**
- \brief Simplify rules into a set of new rules that are returned.
- The simplification routines apply inlining, quantifier elimination, and other
- algebraic simplifications.
+ \brief Retrieve set of rules from fixedpoint context.
- def_API('Z3_fixedpoint_simplify_rules', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2,AST), _in(UINT), _in_array(4,FUNC_DECL)))
- */
- Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
+ def_API('Z3_fixedpoint_get_rules', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
+ */
+ Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
__in Z3_context c,
- __in Z3_fixedpoint f,
- __in unsigned num_rules,
- __in_ecount(num_rules) Z3_ast rules[],
- __in unsigned num_outputs,
- __in_ecount(num_outputs) Z3_func_decl outputs[]);
+ __in Z3_fixedpoint f);
/**
\brief Set parameters on fixedpoint context.
@@ -5738,6 +5732,38 @@ END_MLAPI_EXCLUDE
__in unsigned num_queries,
__in_ecount(num_queries) Z3_ast queries[]);
+ /**
+ \brief Parse an SMT-LIB2 string with fixedpoint rules.
+ Add the rules to the current fixedpoint context.
+ Return the set of queries in the file.
+
+ \param c - context.
+ \param f - fixedpoint context.
+ \param s - string containing SMT2 specification.
+
+ def_API('Z3_fixedpoint_from_string', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
+ */
+ Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
+ __in Z3_context c,
+ __in Z3_fixedpoint f,
+ __in Z3_string s);
+
+ /**
+ \brief Parse an SMT-LIB2 file with fixedpoint rules.
+ Add the rules to the current fixedpoint context.
+ Return the set of queries in the file.
+
+ \param c - context.
+ \param f - fixedpoint context.
+ \param s - string containing SMT2 specification.
+
+ def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
+ */
+ Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
+ __in Z3_context c,
+ __in Z3_fixedpoint f,
+ __in Z3_string s);
+
/**
\brief Create a backtracking point.
diff --git a/src/ast/ast_pp.cpp b/src/ast/ast_pp.cpp
deleted file mode 100644
index 842f05408..000000000
--- a/src/ast/ast_pp.cpp
+++ /dev/null
@@ -1,516 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- ast_pp.cpp
-
-Abstract:
-
- Expression DAG pretty printer
-
-Author:
-
- Leonardo de Moura 2008-01-20.
-
-Revision History:
-
---*/
-
-#include"ast_pp.h"
-#include"pp.h"
-#include"obj_pair_hashtable.h"
-#include"ast_ll_pp.h"
-#include"arith_decl_plugin.h"
-#include"bv_decl_plugin.h"
-#include"datatype_decl_plugin.h"
-#include"dl_decl_plugin.h"
-#include"ast_list.h"
-#include
-
-using namespace format_ns;
-
-mk_pp::mk_pp(ast * a, ast_manager & m, pp_params const & p, unsigned indent, unsigned num_var_names, char const * const * var_names):
- m_ast(a),
- m_manager(m),
- m_params(p),
- m_indent(indent),
- m_num_var_names(num_var_names),
- m_var_names(var_names) {
-}
-
-mk_pp::mk_pp(ast * a, ast_manager & m, unsigned indent, unsigned num_var_names, char const * const * var_names):
- m_ast(a),
- m_manager(m),
- m_params(get_pp_default_params()),
- m_indent(indent),
- m_num_var_names(num_var_names),
- m_var_names(var_names) {
-}
-
-std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m) {
- return ast_pp(strm, n, m, get_pp_default_params());
-}
-
-struct pp_cache {
- typedef obj_pair_map cache;
-
- ast_manager & m_manager;
- cache m_cache;
-
- pp_cache(ast_manager & m):
- m_manager(m) {
- }
-
- ~pp_cache() {
- reset();
- }
-
- bool contains(ast * k1, quantifier_list * k2) const { return m_cache.contains(k1, k2); }
-
- void get(ast * k1, quantifier_list * k2, format * & r) const { m_cache.find(k1, k2, r); }
-
- void insert(ast * k1, quantifier_list * k2, format * f) {
- SASSERT(!m_cache.contains(k1, k2));
- fm(m_manager).inc_ref(f);
- m_cache.insert(k1, k2, f);
- }
-
- void reset() {
- cache::iterator it = m_cache.begin();
- cache::iterator end = m_cache.end();
- for (; it != end; ++it) {
- format * f = (*it).get_value();
- fm(m_manager).dec_ref(f);
- }
- m_cache.reset();
- }
-};
-
-class formatter {
- typedef quantifier_list_manager qlist_manager;
- typedef quantifier_list_ref qlist_ref;
- typedef quantifier_list_ref_vector qlist_ref_vector;
- pp_params const & m_params;
- ast_manager & m_manager;
- qlist_manager m_qlist_manager;
- pp_cache m_cache;
- typedef std::pair pp_entry;
- svector m_todo;
- qlist_ref_vector m_qlists;
- app_ref m_nil;
- arith_util m_autil;
- bv_util m_bvutil;
- datatype_util m_datatype_util;
- datalog::dl_decl_util m_dl_util;
- ptr_vector m_datatypes;
- app_ref_vector m_format_trail;
- ast_mark m_visited_datatypes;
- unsigned m_num_var_names;
- char const * const * m_var_names;
-
- struct symbol2format {
- ast_manager & m_manager;
- symbol2format(ast_manager & m):m_manager(m) {}
- format * operator()(symbol const & s) {
- std::string str = s.str();
- return mk_string(m_manager, str.c_str());
- }
- };
-
- format * get_cached(ast * n, quantifier_list * qlist) {
- format * f = 0;
- if (is_sort(n)) {
- qlist = m_qlist_manager.mk_nil();
- }
- m_cache.get(n, qlist, f);
- SASSERT(f);
- return f;
- }
-
- void visit(ast * n, quantifier_list * qlist, bool & visited) {
- if (is_sort(n)) {
- qlist = m_qlist_manager.mk_nil();
- }
- if (!m_cache.contains(n, qlist)) {
- m_todo.push_back(pp_entry(n, qlist));
- visited = false;
- }
- }
-
- bool visit_children(ast * n, quantifier_list * qlist) {
- unsigned j;
- bool visited = true;
- switch (n->get_kind()) {
- case AST_FUNC_DECL: {
- func_decl* f = to_func_decl(n);
- j = f->get_arity();
- while (j > 0) {
- --j;
- visit(f->get_domain(j), qlist, visited);
- }
- visit(f->get_range(), qlist, visited);
- j = f->get_num_parameters();
- while (j > 0) {
- --j;
- parameter p(f->get_parameter(j));
- if (p.is_ast()) {
- visit(p.get_ast(), qlist, visited);
- }
- }
- break;
- }
- case AST_SORT: {
- sort* s = to_sort(n);
- j = s->get_num_parameters();
- while (j > 0) {
- --j;
- parameter p(s->get_parameter(j));
- if (p.is_ast()) {
- visit(p.get_ast(), qlist, visited);
- }
- }
- break;
- }
- case AST_APP: {
- app* a = to_app(n);
- j = a->get_num_args();
- while (j > 0) {
- --j;
- visit(a->get_arg(j), qlist, visited);
- }
- visit(a->get_decl(), qlist, visited);
- break;
- }
- case AST_QUANTIFIER:
- j = to_quantifier(n)->get_num_patterns();
- qlist = m_qlist_manager.mk_cons(to_quantifier(n), qlist);
- m_qlists.push_back(qlist);
- while (j > 0) {
- --j;
- visit(to_quantifier(n)->get_pattern(j), qlist, visited);
- }
- j = to_quantifier(n)->get_num_no_patterns();
- while (j > 0) {
- --j;
- visit(to_quantifier(n)->get_no_pattern(j), qlist, visited);
- }
- j = to_quantifier(n)->get_num_decls();
- while (j > 0) {
- --j;
- visit(to_quantifier(n)->get_decl_sort(j), qlist, visited);
- visit_sort(to_quantifier(n)->get_decl_sort(j));
- }
- visit(to_quantifier(n)->get_expr(), qlist, visited);
- break;
- default:
- break;
- }
- return visited;
- }
-
- void reduce1(ast * n, quantifier_list * qlist) {
- format * r;
- switch(n->get_kind()) {
- case AST_APP:
- r = reduce1_app(to_app(n), qlist);
- break;
- case AST_VAR:
- r = reduce1_var(to_var(n), qlist);
- break;
- case AST_QUANTIFIER:
- r = reduce1_quantifier(to_quantifier(n), qlist);
- break;
- case AST_SORT:
- r = reduce1_sort(to_sort(n), qlist);
- break;
- case AST_FUNC_DECL:
- r = reduce1_func_decl(to_func_decl(n), qlist);
- break;
- }
- m_cache.insert(n, qlist, r);
- }
-
- format * mk_parameter(parameter const & p, quantifier_list * qlist) {
- if (p.is_int()) {
- return mk_int(m_manager, p.get_int());
- }
- else if (p.is_symbol()) {
- return mk_string(m_manager, p.get_symbol().str().c_str());
- }
- else if (p.is_ast()) {
- ast * n = p.get_ast();
- if (is_func_decl(n)) {
- return mk_string(m_manager, to_func_decl(n)->get_name().str().c_str());
- }
- else {
- return get_cached(p.get_ast(), qlist);
- }
- }
- else if (p.is_rational()) {
- return mk_string(m_manager, p.get_rational().to_string().c_str());
- }
- else {
- return 0;
- }
- }
-
- void mk_parameters(unsigned num_params, parameter const * p, quantifier_list * qlist, ptr_buffer & result, bool add_separator) {
- bool first = true;
- for (unsigned i = 0; i < num_params; i++) {
- if (!first && add_separator) {
- result.push_back(mk_string(m_manager, ":"));
- }
- format * pp = mk_parameter(p[i], qlist);
- if (pp) {
- result.push_back(pp);
- first = false;
- }
- }
- }
-
- format * mk_parameters(unsigned num_params, parameter const * p, quantifier_list * qlist) {
- if (num_params == 0)
- return m_nil;
- ptr_buffer buffer;
- buffer.push_back(mk_string(m_manager, "["));
- mk_parameters(num_params, p, qlist, buffer, true);
- buffer.push_back(mk_string(m_manager, "]"));
- return mk_compose(m_manager, buffer.size(), buffer.c_ptr());
- }
-
- void visit_sort(sort* s) {
- if (m_datatype_util.is_datatype(s) &&
- !m_visited_datatypes.is_marked(s)) {
- m_datatypes.push_back(s);
- m_visited_datatypes.mark(s, true);
- }
- }
-
- format * reduce1_sort(sort * s, quantifier_list * qlist) {
- if (m_datatype_util.is_datatype(s)) {
- return mk_string(m_manager, s->get_name().str().c_str());
- }
- ptr_buffer pps;
- mk_parameters(s->get_num_parameters(), s->get_parameters(), qlist, pps, false);
- std::string name = s->get_name().str();
- if (pps.empty())
- return mk_string(m_manager, name.c_str());
- return mk_seq1(m_manager, pps.c_ptr(), pps.c_ptr() + pps.size(),
- f2f(), name.c_str());
- }
-
- format * reduce1_func_decl(func_decl * f, quantifier_list * qlist) {
- ptr_buffer children;
- children.push_back(mk_compose(m_manager,
- mk_string(m_manager, f->get_name().str().c_str()),
- mk_parameters(f->get_num_parameters(), f->get_parameters(), qlist)));
- for (unsigned i = 0; i < f->get_arity(); i++)
- children.push_back(get_cached(f->get_domain(i), qlist));
- children.push_back(get_cached(f->get_range(), qlist));
- return mk_seq1(m_manager, children.begin(), children.end(), f2f(), "define");
- }
-
- void get_children(app * n, quantifier_list * qlist, ptr_buffer & result) {
- for (unsigned i = 0; i < n->get_num_args(); i++)
- result.push_back(get_cached(n->get_arg(i), qlist));
- }
-
- format * reduce1_app(app * n, quantifier_list * qlist) {
- rational val;
- bool is_int;
- bool pos;
- unsigned bv_size;
- uint64 uval;
- buffer names;
- ptr_buffer children;
- if (m_autil.is_numeral(n, val, is_int)) {
- std::string str;
- if (val.is_neg()) {
- str = "(- " + (-val).to_string() + ")";
- }
- else {
- str = val.to_string();
- }
- return mk_string(m_manager, str.c_str());
- }
- else if (m_bvutil.is_numeral(n, val, bv_size)) {
- std::string str = val.to_string();
- return mk_compose(m_manager,
- mk_string(m_manager, "bv"),
- mk_string(m_manager, str.c_str()),
- mk_compose(m_manager, mk_string(m_manager, "["), mk_unsigned(m_manager, bv_size), mk_string(m_manager, "]")));
- }
- else if (m_dl_util.is_finite_sort(n) &&
- m_dl_util.is_numeral_ext(n, uval)) {
- return mk_string(m_manager, rational(uval,rational::ui64()).to_string().c_str());
- }
- else if (m_manager.is_label(n, pos, names)) {
- get_children(n, qlist, children);
- symbol2format f(m_manager);
- format * lbl = names.size() > 1 ? mk_seq5(m_manager, names.begin(), names.end(), f) : f(names[0]);
- format * args[2] = { lbl, children[0] };
- format ** begin = args;
- return mk_seq1(m_manager, begin, begin+2, f2f(), pos ? "lblpos" : "lblneg");
- }
- else if (m_manager.is_pattern(n)) {
- get_children(n, qlist, children);
- return mk_seq5(m_manager, children.begin(), children.end(), f2f(), "{", "}");
- }
- else if (m_manager.is_proof(n)) {
- get_children(n, qlist, children);
- return mk_seq2(m_manager, children.begin(), children.end(), f2f(), n->get_decl()->get_name().str().c_str(),
- FORMAT_DEFAULT_INDENT, "[", "]");
- }
- else if (m_params.m_pp_fixed_indent || (n->get_decl()->get_num_parameters() > 0 && !n->get_decl()->private_parameters())) {
- format * head = mk_compose(m_manager,
- mk_string(m_manager, n->get_decl()->get_name().str().c_str()),
- mk_parameters(n->get_decl()->get_num_parameters(), n->get_decl()->get_parameters(), qlist));
- if (n->get_num_args() == 0)
- return head;
- children.push_back(head);
- get_children(n, qlist, children);
- return mk_seq4(m_manager, children.begin(), children.end(), f2f());
- }
- else if (n->get_num_args() == 0)
- return mk_string(m_manager, n->get_decl()->get_name().str().c_str());
- else {
- get_children(n, qlist, children);
- return mk_seq1(m_manager, children.begin(), children.end(), f2f(), n->get_decl()->get_name().str().c_str());
- }
- }
-
- format * reduce1_var(var * v, quantifier_list * qlist) {
- unsigned idx = v->get_idx();
- unsigned i = idx;
- while (!is_nil(qlist)) {
- quantifier * q = head(qlist);
- if (i < q->get_num_decls())
- return mk_string(m_manager, q->get_decl_name(q->get_num_decls() - i - 1).str().c_str());
- i -= q->get_num_decls();
- qlist = tail(qlist);
- }
- if (i < m_num_var_names) {
- return mk_string(m_manager, m_var_names[m_num_var_names - i - 1]);
- }
- else {
- return mk_compose(m_manager, mk_string(m_manager, "#"), mk_unsigned(m_manager, idx));
- }
- }
-
- format * reduce1_quantifier(quantifier * q, quantifier_list * qlist) {
- qlist = m_qlist_manager.mk_cons(q, qlist);
-
- ptr_buffer buffer;
- unsigned num = q->get_num_decls();
- for (unsigned j = 0; j < num; j++) {
- format * d[2];
- d[0] = mk_string(m_manager, q->get_decl_name(j).str().c_str());
- d[1] = get_cached(q->get_decl_sort(j), qlist);
- format ** it = d;
- buffer.push_back(mk_seq5(m_manager, it, it+2, f2f()));
- }
- buffer.push_back(get_cached(q->get_expr(), qlist));
- num = q->get_num_patterns();
- char const * pat = ":pat ";
- unsigned pat_indent = static_cast(strlen(pat));
- for (unsigned i = 0; i < num; i++)
- buffer.push_back(mk_compose(m_manager, mk_string(m_manager, pat), mk_indent(m_manager, pat_indent, get_cached(q->get_pattern(i), qlist))));
- num = q->get_num_no_patterns();
- for (unsigned i = 0; i < num; i++)
- buffer.push_back(mk_compose(m_manager, mk_string(m_manager, ":nopat {"), get_cached(q->get_no_pattern(i), qlist), mk_string(m_manager, "}")));
- if (q->get_qid() != symbol::null)
- buffer.push_back(mk_compose(m_manager, mk_string(m_manager, ":qid {"), mk_string(m_manager, q->get_qid().str().c_str()), mk_string(m_manager, "}")));
- return mk_seq3(m_manager, buffer.begin(), buffer.end(), f2f(), q->is_forall() ? "forall" : "exists",
- q->get_num_decls());
- }
-
-public:
- formatter(ast_manager & m, pp_params const & p, unsigned num_var_names, char const * const * var_names):
- m_params(p),
- m_manager(m),
- m_qlist_manager(m),
- m_cache(m),
- m_qlists(m_qlist_manager),
- m_nil(mk_nil(m), fm(m)),
- m_autil(m),
- m_bvutil(m),
- m_datatype_util(m),
- m_dl_util(m),
- m_format_trail(fm(m)),
- m_num_var_names(num_var_names),
- m_var_names(var_names) {
- }
-
- ~formatter() {
- }
-
- format * operator()(ast * n) {
- m_todo.push_back(pp_entry(n, m_qlist_manager.mk_nil()));
- while (!m_todo.empty()) {
- pp_entry k = m_todo.back();
- if (m_cache.contains(k.first, k.second))
- m_todo.pop_back();
- else if (visit_children(k.first, k.second)) {
- m_todo.pop_back();
- reduce1(k.first, k.second);
- }
- }
- format* f1 = get_cached(n, m_qlist_manager.mk_nil());
-
- if (m_datatypes.empty()) {
- return f1;
- }
- ptr_buffer formats;
- formats.push_back(f1);
-
- for (unsigned i = 0; i < m_datatypes.size(); ++i) {
- sort* s = m_datatypes[i];
- std::ostringstream buffer;
- m_datatype_util.display_datatype(s, buffer);
- format* f2 = mk_string(m_manager, buffer.str().c_str());
- formats.push_back(mk_line_break(m_manager));
- formats.push_back(f2);
- }
- f1 = mk_compose(m_manager, formats.size(), formats.c_ptr());
- //
- // Ensure that reference count is live.
- //
- m_format_trail.push_back(f1);
- return f1;
- }
-};
-
-
-std::ostream & ast_pp(std::ostream & out, ast * n, ast_manager & m, pp_params const & p, unsigned indent,
- unsigned num_vars, char const * const * names) {
- formatter f(m, p, num_vars, names);
- app_ref fmt(fm(m));
- fmt = f(n);
- if (indent > 0)
- fmt = format_ns::mk_indent(m, indent, fmt);
- pp(out, fmt, m, p);
- return out;
-}
-
-std::string & ast_pp(std::string & out, ast * n, ast_manager & m, pp_params const & p, unsigned indent) {
- std::ostringstream buffer;
- buffer << mk_pp(n, m, p, indent);
- out += buffer.str();
- return out;
-}
-
-std::string ast_pp(ast * n, ast_manager & m, pp_params const & p, unsigned indent) {
- std::string out;
- return ast_pp(out, n, m, p, indent);
-}
-
-
-std::string & ast_pp(std::string & out, ast * n, ast_manager & m) {
- return ast_pp(out, n, m, get_pp_default_params());
-}
-
-std::string ast_pp(ast * n, ast_manager & m) {
- return ast_pp(n, m, get_pp_default_params());
-}
-
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index eeee29d44..d99fb7670 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -15,39 +15,22 @@ Author:
Revision History:
+ 2012-11-17 - ast_smt2_pp is the official pretty printer in Z3
+
--*/
#ifndef _AST_PP_H_
#define _AST_PP_H_
-#include"ast.h"
-#include"pp_params.h"
+#include"ast_smt2_pp.h"
-std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0,
- unsigned num_vars = 0, char const * const * names = 0);
-std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m);
-
-std::string & ast_pp(std::string & s, ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0);
-std::string ast_pp(ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0);
-std::string & ast_pp(std::string & s, ast * n, ast_manager & m);
-std::string ast_pp(ast * n, ast_manager & m);
-
-struct mk_pp {
- ast * m_ast;
- ast_manager & m_manager;
- pp_params const & m_params;
- unsigned m_indent;
- unsigned m_num_var_names;
- char const * const * m_var_names;
- mk_pp(ast * a, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_var_names = 0, char const * const * var_names = 0);
- mk_pp(ast * a, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const * const * var_names = 0);
+struct mk_pp : public mk_ismt2_pp {
+ mk_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
+ mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
+ }
+ mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
+ mk_ismt2_pp(t, m, indent, num_vars, var_prefix) {
+ }
};
-inline std::ostream& operator<<(std::ostream& out, const mk_pp & p) {
- return ast_pp(out, p.m_ast, p.m_manager, p.m_params, p.m_indent, p.m_num_var_names, p.m_var_names);
-}
-
-inline std::string& operator+=(std::string& out, const mk_pp & p) {
- return ast_pp(out, p.m_ast, p.m_manager, p.m_params, p.m_indent);
-}
-
#endif
+
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index aa3a9c76d..944eb1e26 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -317,8 +317,8 @@ class smt_printer {
}
void visit_sort(sort* s, bool bool2int = false) {
- symbol sym;
- if (bool2int && is_bool(s)) {
+ symbol sym;
+ if (bool2int && is_bool(s) && !m_is_smt2) {
sym = symbol("Int");
} else if (s->is_sort_of(m_bv_fid, BV_SORT)) {
sym = symbol("BitVec");
diff --git a/src/ast/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp
index f43b85154..d454c7f00 100644
--- a/src/ast/normal_forms/cnf.cpp
+++ b/src/ast/normal_forms/cnf.cpp
@@ -16,8 +16,9 @@ Author:
Revision History:
--*/
-
#include"cnf.h"
+#include"var_subst.h"
+#include"ast_util.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp
index fa531c73a..5158439a7 100644
--- a/src/ast/normal_forms/pull_quant.cpp
+++ b/src/ast/normal_forms/pull_quant.cpp
@@ -17,369 +17,372 @@ Notes:
--*/
#include"pull_quant.h"
+#include"var_subst.h"
+#include"rewriter_def.h"
#include"ast_pp.h"
-#include"for_each_expr.h"
-void pull_quant::pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
- ptr_buffer var_sorts;
- buffer var_names;
- symbol qid;
- int w = INT_MAX;
-
- // The input formula is in Skolem normal form...
- // So all children are forall (positive context) or exists (negative context).
- // Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...)))
- // So, when pulling a quantifier over a NOT, it becomes an exists.
+struct pull_quant::imp {
- if (m_manager.is_not(d)) {
- SASSERT(num_children == 1);
- expr * child = children[0];
- if (is_quantifier(child)) {
- quantifier * q = to_quantifier(child);
- expr * body = q->get_expr();
- result = m_manager.update_quantifier(q, !q->is_forall(), m_manager.mk_not(body));
+ struct rw_cfg : public default_rewriter_cfg {
+ ast_manager & m_manager;
+ shift_vars m_shift;
+
+ rw_cfg(ast_manager & m):
+ m_manager(m),
+ m_shift(m) {
}
- else {
- result = m_manager.mk_not(child);
- }
- return;
- }
- bool found_quantifier = false;
- bool forall_children;
-
- for (unsigned i = 0; i < num_children; i++) {
- expr * child = children[i];
- if (is_quantifier(child)) {
+ bool pull_quant1_core(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
+ ptr_buffer var_sorts;
+ buffer var_names;
+ symbol qid;
+ int w = INT_MAX;
- if (!found_quantifier) {
- found_quantifier = true;
- forall_children = is_forall(child);
- }
- else {
- // Since the initial formula was in SNF, all children must be EXISTS or FORALL.
- SASSERT(forall_children == is_forall(child));
+ // The input formula is in Skolem normal form...
+ // So all children are forall (positive context) or exists (negative context).
+ // Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...)))
+ // So, when pulling a quantifier over a NOT, it becomes an exists.
+
+ if (m_manager.is_not(d)) {
+ SASSERT(num_children == 1);
+ expr * child = children[0];
+ if (is_quantifier(child)) {
+ quantifier * q = to_quantifier(child);
+ expr * body = q->get_expr();
+ result = m_manager.update_quantifier(q, !q->is_forall(), m_manager.mk_not(body));
+ return true;
+ }
+ else {
+ return false;
+ }
}
- quantifier * nested_q = to_quantifier(child);
- if (var_sorts.empty()) {
- // use the qid of one of the nested quantifiers.
- qid = nested_q->get_qid();
+ bool found_quantifier = false;
+ bool forall_children;
+
+ for (unsigned i = 0; i < num_children; i++) {
+ expr * child = children[i];
+ if (is_quantifier(child)) {
+
+ if (!found_quantifier) {
+ found_quantifier = true;
+ forall_children = is_forall(child);
+ }
+ else {
+ // Since the initial formula was in SNF, all children must be EXISTS or FORALL.
+ SASSERT(forall_children == is_forall(child));
+ }
+
+ quantifier * nested_q = to_quantifier(child);
+ if (var_sorts.empty()) {
+ // use the qid of one of the nested quantifiers.
+ qid = nested_q->get_qid();
+ }
+ w = std::min(w, nested_q->get_weight());
+ unsigned j = nested_q->get_num_decls();
+ while (j > 0) {
+ --j;
+ var_sorts.push_back(nested_q->get_decl_sort(j));
+ symbol s = nested_q->get_decl_name(j);
+ if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
+ var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str()));
+ else
+ var_names.push_back(s);
+ }
+ }
}
- w = std::min(w, nested_q->get_weight());
- unsigned j = nested_q->get_num_decls();
- while (j > 0) {
- --j;
- var_sorts.push_back(nested_q->get_decl_sort(j));
- symbol s = nested_q->get_decl_name(j);
- if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
- var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str()));
- else
- var_names.push_back(s);
- }
- }
- }
-
- if (!var_sorts.empty()) {
- SASSERT(found_quantifier);
- // adjust the variable ids in formulas in new_children
- expr_ref_buffer new_adjusted_children(m_manager);
- expr_ref adjusted_child(m_manager);
- unsigned num_decls = var_sorts.size();
- unsigned shift_amount = 0;
- TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";);
- for (unsigned i = 0; i < num_children; i++) {
- expr * child = children[i];
- if (!is_quantifier(child)) {
- // increment the free variables in child by num_decls because
- // child will be in the scope of num_decls bound variables.
- m_shift(child, num_decls, adjusted_child);
- TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" <<
- mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
+
+ if (!var_sorts.empty()) {
+ SASSERT(found_quantifier);
+ // adjust the variable ids in formulas in new_children
+ expr_ref_buffer new_adjusted_children(m_manager);
+ expr_ref adjusted_child(m_manager);
+ unsigned num_decls = var_sorts.size();
+ unsigned shift_amount = 0;
+ TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";);
+ for (unsigned i = 0; i < num_children; i++) {
+ expr * child = children[i];
+ if (!is_quantifier(child)) {
+ // increment the free variables in child by num_decls because
+ // child will be in the scope of num_decls bound variables.
+ m_shift(child, num_decls, adjusted_child);
+ TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" <<
+ mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
+ }
+ else {
+ quantifier * nested_q = to_quantifier(child);
+ SASSERT(num_decls >= nested_q->get_num_decls());
+ // Assume nested_q is of the form
+ // forall xs. P(xs, ys)
+ // where xs (ys) represents the set of bound (free) variables.
+ //
+ // - the index of the variables xs must be increased by shift_amount.
+ // That is, the number of new bound variables that will precede the bound
+ // variables xs.
+ //
+ // - the index of the variables ys must be increased by num_decls - nested_q->get_num_decls.
+ // That is, the total number of new bound variables that will be in the scope
+ // of nested_q->get_expr().
+ m_shift(nested_q->get_expr(),
+ nested_q->get_num_decls(), // bound for shift1/shift2
+ num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound)
+ shift_amount, // shift2 (shift by this ammount if var idx < bound)
+ adjusted_child);
+ TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount <<
+ " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) <<
+ "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
+ shift_amount += nested_q->get_num_decls();
+ }
+ new_adjusted_children.push_back(adjusted_child);
+ }
+
+ // Remark: patterns are ignored.
+ // This is ok, since this functor is used in one of the following cases:
+ //
+ // 1) Superposition calculus is being used, so the
+ // patterns are useless.
+ //
+ // 2) No patterns were provided, and the functor is used
+ // to increase the effectiveness of the pattern inference
+ // procedure.
+ //
+ // 3) MBQI
+ std::reverse(var_sorts.begin(), var_sorts.end());
+ std::reverse(var_names.begin(), var_names.end());
+ result = m_manager.mk_quantifier(forall_children,
+ var_sorts.size(),
+ var_sorts.c_ptr(),
+ var_names.c_ptr(),
+ m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
+ w,
+ qid);
+ return true;
}
else {
- quantifier * nested_q = to_quantifier(child);
- SASSERT(num_decls >= nested_q->get_num_decls());
- // Assume nested_q is of the form
- // forall xs. P(xs, ys)
- // where xs (ys) represents the set of bound (free) variables.
- //
- // - the index of the variables xs must be increased by shift_amount.
- // That is, the number of new bound variables that will precede the bound
- // variables xs.
- //
- // - the index of the variables ys must be increased by num_decls - nested_q->get_num_decls.
- // That is, the total number of new bound variables that will be in the scope
- // of nested_q->get_expr().
- m_shift(nested_q->get_expr(),
- nested_q->get_num_decls(), // bound for shift1/shift2
- num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound)
- shift_amount, // shift2 (shift by this ammount if var idx < bound)
- adjusted_child);
- TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount <<
- " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) <<
- "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
- shift_amount += nested_q->get_num_decls();
+ SASSERT(!found_quantifier);
+ return false;
}
- new_adjusted_children.push_back(adjusted_child);
}
- // Remark: patterns are ignored.
- // This is ok, since this functor is used in one of the following cases:
- //
- // 1) Superposition calculus is being used, so the
- // patterns are useless.
- //
- // 2) No patterns were provided, and the functor is used
- // to increase the effectiveness of the pattern inference
- // procedure.
- //
- // 3) MBQI
- std::reverse(var_sorts.begin(), var_sorts.end());
- std::reverse(var_names.begin(), var_names.end());
- result = m_manager.mk_quantifier(forall_children,
- var_sorts.size(),
+ void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
+ if (!pull_quant1_core(d, num_children, children, result)) {
+ result = m_manager.mk_app(d, num_children, children);
+ }
+ }
+
+
+ void pull_quant1_core(quantifier * q, expr * new_expr, expr_ref & result) {
+ // The original formula was in SNF, so the original quantifiers must be universal.
+ SASSERT(is_forall(q));
+ SASSERT(is_forall(new_expr));
+ quantifier * nested_q = to_quantifier(new_expr);
+ ptr_buffer var_sorts;
+ buffer var_names;
+ var_sorts.append(q->get_num_decls(), const_cast(q->get_decl_sorts()));
+ var_sorts.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_sorts()));
+ var_names.append(q->get_num_decls(), const_cast(q->get_decl_names()));
+ var_names.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_names()));
+ // Remark: patterns are ignored.
+ // See comment in reduce1_app
+ result = m_manager.mk_forall(var_sorts.size(),
var_sorts.c_ptr(),
var_names.c_ptr(),
- m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
- w,
- qid);
- }
- else {
- SASSERT(!found_quantifier);
- result = m_manager.mk_app(d, num_children, children);
- }
-}
-
-void pull_quant::pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {
- // The original formula was in SNF, so the original quantifiers must be universal.
- SASSERT(is_forall(q));
- if (is_forall(new_expr)) {
- quantifier * nested_q = to_quantifier(new_expr);
- ptr_buffer var_sorts;
- buffer var_names;
- var_sorts.append(q->get_num_decls(), const_cast(q->get_decl_sorts()));
- var_sorts.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_sorts()));
- var_names.append(q->get_num_decls(), const_cast(q->get_decl_names()));
- var_names.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_names()));
- // Remark: patterns are ignored.
- // See comment in reduce1_app
- result = m_manager.mk_forall(var_sorts.size(),
- var_sorts.c_ptr(),
- var_names.c_ptr(),
- nested_q->get_expr(),
- std::min(q->get_weight(), nested_q->get_weight()),
- q->get_qid());
- }
- else {
- SASSERT(!is_quantifier(new_expr));
- result = m_manager.update_quantifier(q, new_expr);
- }
-}
-
-void pull_quant::pull_quant1(expr * n, expr_ref & result) {
- if (is_app(n))
- pull_quant1(to_app(n)->get_decl(), to_app(n)->get_num_args(), to_app(n)->get_args(), result);
- else if (is_quantifier(n))
- pull_quant1(to_quantifier(n), to_quantifier(n)->get_expr(), result);
- else
- result = n;
-}
-
-// Code for proof generation...
-void pull_quant::pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
- pr = 0;
- if (is_app(n)) {
- expr_ref_buffer new_args(m_manager);
- expr_ref new_arg(m_manager);
- ptr_buffer proofs;
- unsigned num = to_app(n)->get_num_args();
- for (unsigned i = 0; i < num; i++) {
- expr * arg = to_app(n)->get_arg(i);
- pull_quant1(arg , new_arg);
- new_args.push_back(new_arg);
- if (new_arg != arg)
- proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
+ nested_q->get_expr(),
+ std::min(q->get_weight(), nested_q->get_weight()),
+ q->get_qid());
}
- pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
- if (m_manager.fine_grain_proofs()) {
- app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
- proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
- proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
- pr = m_manager.mk_transitivity(p1, p2);
- }
- }
- else if (is_quantifier(n)) {
- expr_ref new_expr(m_manager);
- pull_quant1(to_quantifier(n)->get_expr(), new_expr);
- pull_quant1(to_quantifier(n), new_expr, r);
- if (m_manager.fine_grain_proofs()) {
- quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
- proof * p1 = 0;
- if (n != q1) {
- proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr));
- p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
+
+ void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {
+ // The original formula was in SNF, so the original quantifiers must be universal.
+ SASSERT(is_forall(q));
+ if (is_forall(new_expr)) {
+ pull_quant1_core(q, new_expr, result);
}
- proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));
- pr = m_manager.mk_transitivity(p1, p2);
- }
- }
- else {
- r = n;
- }
-}
-
-bool pull_quant::visit_children(expr * n) {
- bool visited = true;
- unsigned j;
- switch(n->get_kind()) {
- case AST_APP:
- // This transformation is also applied after the formula
- // has been converted into a SNF using only OR and NOT.
- if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) {
- j = to_app(n)->get_num_args();
- while (j > 0) {
- --j;
- visit(to_app(n)->get_arg(j), visited);
- }
- }
- else {
- // This class assumes the formula is in skolem normal form.
- SASSERT(!has_quantifiers(n));
- }
- break;
- case AST_QUANTIFIER:
- if (to_quantifier(n)->is_forall())
- visit(to_quantifier(n)->get_expr(), visited);
- break;
- default:
- break;
- }
- return visited;
-}
-
-void pull_quant::reduce1(expr * n) {
- switch(n->get_kind()) {
- case AST_APP:
- reduce1_app(to_app(n));
- break;
- case AST_VAR:
- cache_result(n, n, 0);
- break;
- case AST_QUANTIFIER:
- reduce1_quantifier(to_quantifier(n));
- break;
- default:
- UNREACHABLE();
- break;
- }
-}
-
-void pull_quant::reduce1_app(app * n) {
- if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) {
- ptr_buffer new_children;
- ptr_buffer new_children_proofs;
- unsigned num = n->get_num_args();
- for (unsigned i = 0; i < num; i++) {
- expr * new_child = 0;
- proof * new_child_pr = 0;
- get_cached(n->get_arg(i), new_child, new_child_pr);
- new_children.push_back(new_child);
- if (new_child_pr) {
- new_children_proofs.push_back(new_child_pr);
+ else {
+ SASSERT(!is_quantifier(new_expr));
+ result = m_manager.update_quantifier(q, new_expr);
}
}
- expr_ref r(m_manager);
- pull_quant1(n->get_decl(), new_children.size(), new_children.c_ptr(), r);
- proof * pr = 0;
- if (m_manager.fine_grain_proofs()) {
- app * n_prime = m_manager.mk_app(n->get_decl(), new_children.size(), new_children.c_ptr());
- TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n";
- tout << mk_pp(n_prime, m_manager) << "\n";);
- proof * p1 = n == n_prime ? 0 : m_manager.mk_congruence(n, n_prime,
- new_children_proofs.size(), new_children_proofs.c_ptr());
- proof * p2 = n_prime == r ? 0 : m_manager.mk_pull_quant(n_prime, to_quantifier(r));
- pr = m_manager.mk_transitivity(p1, p2);
+ void pull_quant1(expr * n, expr_ref & result) {
+ if (is_app(n))
+ pull_quant1(to_app(n)->get_decl(), to_app(n)->get_num_args(), to_app(n)->get_args(), result);
+ else if (is_quantifier(n))
+ pull_quant1(to_quantifier(n), to_quantifier(n)->get_expr(), result);
+ else
+ result = n;
+ }
+
+ // Code for proof generation...
+ void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
+ pr = 0;
+ if (is_app(n)) {
+ expr_ref_buffer new_args(m_manager);
+ expr_ref new_arg(m_manager);
+ ptr_buffer proofs;
+ unsigned num = to_app(n)->get_num_args();
+ for (unsigned i = 0; i < num; i++) {
+ expr * arg = to_app(n)->get_arg(i);
+ pull_quant1(arg , new_arg);
+ new_args.push_back(new_arg);
+ if (new_arg != arg)
+ proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
+ }
+ pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
+ if (m_manager.fine_grain_proofs()) {
+ app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
+ proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
+ proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
+ pr = m_manager.mk_transitivity(p1, p2);
+ }
+ }
+ else if (is_quantifier(n)) {
+ expr_ref new_expr(m_manager);
+ pull_quant1(to_quantifier(n)->get_expr(), new_expr);
+ pull_quant1(to_quantifier(n), new_expr, r);
+ if (m_manager.fine_grain_proofs()) {
+ quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
+ proof * p1 = 0;
+ if (n != q1) {
+ proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr));
+ p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
+ }
+ proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));
+ pr = m_manager.mk_transitivity(p1, p2);
+ }
+ }
+ else {
+ r = n;
+ }
}
- cache_result(n, r, pr);
- return;
- }
- TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n";);
- cache_result(n, n, 0);
-}
-void pull_quant::reduce1_quantifier(quantifier * q) {
- if (q->is_forall()) {
- expr * new_expr;
- proof * new_expr_pr;
- get_cached(q->get_expr(), new_expr, new_expr_pr);
- expr_ref r(m_manager);
- pull_quant1(q, new_expr, r);
- proof * pr = 0;
- if (m_manager.fine_grain_proofs()) {
- quantifier * q_prime = m_manager.update_quantifier(q, new_expr);
- proof * p1 = q == q_prime ? 0 : m_manager.mk_quant_intro(q, q_prime, new_expr_pr);
- proof * p2 = q_prime == r ? 0 : m_manager.mk_pull_quant(q_prime, to_quantifier(r));
- pr = m_manager.mk_transitivity(p1, p2);
+ br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+ if (!m_manager.is_or(f) && !m_manager.is_and(f) && !m_manager.is_not(f))
+ return BR_FAILED;
+
+ if (!pull_quant1_core(f, num, args, result))
+ return BR_FAILED;
+
+ if (m_manager.proofs_enabled()) {
+ result_pr = m_manager.mk_pull_quant(m_manager.mk_app(f, num, args),
+ to_quantifier(result.get()));
+ }
+ return BR_DONE;
}
- cache_result(q, r, pr);
- return;
- }
- // should be unreachable, right?
- UNREACHABLE();
- cache_result(q, q, 0);
-}
+
+ bool reduce_quantifier(quantifier * old_q,
+ expr * new_body,
+ expr * const * new_patterns,
+ expr * const * new_no_patterns,
+ expr_ref & result,
+ proof_ref & result_pr) {
+
+ if (old_q->is_exists()) {
+ UNREACHABLE();
+ return false;
+ }
+
+ if (!is_forall(new_body))
+ return false;
+
+ pull_quant1_core(old_q, new_body, result);
+ if (m_manager.proofs_enabled())
+ result_pr = m_manager.mk_pull_quant(old_q, to_quantifier(result.get()));
+ return true;
+ }
+ };
+
+ struct rw : public rewriter_tpl {
+ rw_cfg m_cfg;
+ rw(ast_manager & m):
+ rewriter_tpl(m, m.proofs_enabled(), m_cfg),
+ m_cfg(m) {
+ }
+ };
-pull_quant::pull_quant(ast_manager & m):
- base_simplifier(m),
- m_shift(m) {
+ rw m_rw;
+
+ imp(ast_manager & m):
+ m_rw(m) {
+ }
+
+ void operator()(expr * n, expr_ref & r, proof_ref & p) {
+ m_rw(n, r, p);
+ }
+};
+
+pull_quant::pull_quant(ast_manager & m) {
+ m_imp = alloc(imp, m);
+}
+
+pull_quant::~pull_quant() {
+ dealloc(m_imp);
}
void pull_quant::operator()(expr * n, expr_ref & r, proof_ref & p) {
- flush_cache();
- m_todo.push_back(n);
- while (!m_todo.empty()) {
- expr * n = m_todo.back();
- if (is_cached(n))
- m_todo.pop_back();
- else if (visit_children(n)) {
- m_todo.pop_back();
- reduce1(n);
+ (*m_imp)(n, r, p);
+}
+
+void pull_quant::reset() {
+ m_imp->m_rw.reset();
+}
+
+void pull_quant::pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
+ m_imp->m_rw.cfg().pull_quant2(n, r, pr);
+}
+
+struct pull_nested_quant::imp {
+
+ struct rw_cfg : public default_rewriter_cfg {
+ pull_quant m_pull;
+ expr_ref m_r;
+ proof_ref m_pr;
+
+ rw_cfg(ast_manager & m):m_pull(m), m_r(m), m_pr(m) {}
+
+ bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+ if (!is_quantifier(s))
+ return false;
+ m_pull(to_quantifier(s), m_r, m_pr);
+ t = m_r.get();
+ t_pr = m_pr.get();
+ return true;
}
- }
-
- expr * result;
- proof * result_proof;
- get_cached(n, result, result_proof);
+ };
- r = result;
+ struct rw : public rewriter_tpl {
+ rw_cfg m_cfg;
+ rw(ast_manager & m):
+ rewriter_tpl(m, m.proofs_enabled(), m_cfg),
+ m_cfg(m) {
+ }
+ };
- switch (m_manager.proof_mode()) {
- case PGM_DISABLED:
- p = m_manager.mk_undef_proof();
- break;
- case PGM_COARSE:
- if (result == n)
- p = m_manager.mk_reflexivity(n);
- else
- p = m_manager.mk_pull_quant_star(n, to_quantifier(result));
- break;
- case PGM_FINE:
- SASSERT(result_proof || result == n);
- p = result_proof ? result_proof : m_manager.mk_reflexivity(n);
- break;
+ rw m_rw;
+
+ imp(ast_manager & m):
+ m_rw(m) {
}
+
+ void operator()(expr * n, expr_ref & r, proof_ref & p) {
+ m_rw(n, r, p);
+ }
+};
+
+pull_nested_quant::pull_nested_quant(ast_manager & m) {
+ m_imp = alloc(imp, m);
}
-bool pull_nested_quant::visit_quantifier(quantifier * q) {
- // do not recurse.
- return true;
+pull_nested_quant::~pull_nested_quant() {
+ dealloc(m_imp);
}
-void pull_nested_quant::reduce1_quantifier(quantifier * q) {
- expr_ref r(m_manager);
- proof_ref pr(m_manager);
- m_pull(q, r, pr);
- cache_result(q, r, pr);
+void pull_nested_quant::operator()(expr * n, expr_ref & r, proof_ref & p) {
+ (*m_imp)(n, r, p);
}
+
+void pull_nested_quant::reset() {
+ m_imp->m_rw.reset();
+}
+
+
diff --git a/src/ast/normal_forms/pull_quant.h b/src/ast/normal_forms/pull_quant.h
index e9b2b5c65..071fb0dbe 100644
--- a/src/ast/normal_forms/pull_quant.h
+++ b/src/ast/normal_forms/pull_quant.h
@@ -19,8 +19,7 @@ Notes:
#ifndef _PULL_QUANT_H_
#define _PULL_QUANT_H_
-#include"simplifier.h"
-#include"var_subst.h"
+#include"ast.h"
/**
\brief Pull nested quantifiers in a formula.
@@ -32,22 +31,14 @@ Notes:
\remark If pull_quant(F) is a quantifier then its weight is
Min{weight(Q') | Q' is a quantifier nested in F}
*/
-class pull_quant : public base_simplifier {
-protected:
- shift_vars m_shift;
- bool visit_children(expr * n);
- void reduce1(expr *);
- void reduce1_app(app * n);
- void reduce1_quantifier(quantifier * q);
-
+class pull_quant {
+ struct imp;
+ imp * m_imp;
public:
pull_quant(ast_manager & m);
- virtual ~pull_quant() {}
+ ~pull_quant();
void operator()(expr * n, expr_ref & r, proof_ref & p);
- void reset() { flush_cache(); }
- void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result);
- void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result);
- void pull_quant1(expr * n, expr_ref & result);
+ void reset();
void pull_quant2(expr * n, expr_ref & r, proof_ref & pr);
};
@@ -55,13 +46,14 @@ public:
\brief After applying this transformation the formula will not
contain nested quantifiers.
*/
-class pull_nested_quant : public simplifier {
- pull_quant m_pull;
- virtual bool visit_quantifier(quantifier * q);
- virtual void reduce1_quantifier(quantifier * q);
+class pull_nested_quant {
+ struct imp;
+ imp * m_imp;
public:
- pull_nested_quant(ast_manager & m):simplifier(m), m_pull(m) { enable_ac_support(false); }
- virtual ~pull_nested_quant() {}
+ pull_nested_quant(ast_manager & m);
+ ~pull_nested_quant();
+ void operator()(expr * n, expr_ref & r, proof_ref & p);
+ void reset();
};
#endif /* _PULL_QUANT_H_ */
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index aca739949..25be8dbf0 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -205,14 +205,10 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
// substitution s contains registers with matching declarations.
return true;
case CHECK_TERM:
- TRACE("expr_pattern_match", display(tout, pc);
- ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
ok = (pc.m_pat == m_regs[pc.m_reg]);
break;
case SET_VAR:
case CHECK_VAR: {
- TRACE("expr_pattern_match", display(tout, pc);
- ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
app* app1 = to_app(pc.m_pat);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_APP) {
@@ -237,8 +233,6 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
break;
}
case SET_BOUND: {
- TRACE("expr_pattern_match", display(tout, pc);
- ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_VAR) {
break;
@@ -329,15 +323,6 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
if (k < fac*num_args) {
bstack.push_back(instr(CHOOSE_AC, pc.m_offset, pc.m_next, app2, k+1));
}
- TRACE("expr_pattern_match",
- {
- tout << "fac: " << fac << " num_args:" << num_args << " k:" << k << "\n";
- for (unsigned i = 0; i < num_args; ++i) {
- ast_pp(tout, m_regs[pc.m_offset + i], m_manager);
- tout << " ";
- }
- tout << "\n";
- });
break;
}
case BACKTRACK:
@@ -430,24 +415,24 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND:
out << "bind ";
- ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
+ out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_AC:
out << "bind_ac ";
- ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
+ out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_C:
out << "bind_c ";
- ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
+ out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
@@ -464,23 +449,23 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case CHECK_VAR:
out << "check_var ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
out << "other_reg: " << pc.m_other_reg << "\n";
break;
case CHECK_TERM:
out << "check ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
- out << "next: " << pc.m_next << "\n";
- out << "reg: " << pc.m_reg << "\n";
- break;
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
+ out << "next: " << pc.m_next << "\n";
+ out << "reg: " << pc.m_reg << "\n";
+ break;
case YIELD:
out << "yield\n";
break;
case SET_VAR:
out << "set_var ";
- ast_pp(out, pc.m_pat, m_manager) << "\n";
+ out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
break;
default:
diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp
index 6a9df1ef4..8a064a315 100644
--- a/src/ast/proof_checker/proof_checker.cpp
+++ b/src/ast/proof_checker/proof_checker.cpp
@@ -6,8 +6,9 @@
#include "arith_decl_plugin.h"
#include "front_end_params.h"
#include "th_rewriter.h"
+#include "var_subst.h"
-#define IS_EQUIV(_e_) (m_manager.is_eq(_e_) || m_manager.is_iff(_e_))
+#define IS_EQUIV(_e_) (m.is_eq(_e_) || m.is_iff(_e_))
#define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
@@ -79,7 +80,7 @@ void proof_checker::hyp_decl_plugin::get_sort_names(svector & sort
}
}
-proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
+proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
symbol fam_name("proof_hypothesis");
if (!m.has_plugin(fam_name)) {
@@ -87,11 +88,11 @@ proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked
}
m_hyp_fid = m.get_family_id(fam_name);
// m_spc_fid = m.get_family_id("spc");
- m_nil = m_manager.mk_const(m_hyp_fid, OP_NIL);
+ m_nil = m.mk_const(m_hyp_fid, OP_NIL);
}
bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
- proof_ref curr(m_manager);
+ proof_ref curr(m);
m_todo.push_back(p);
bool result = true;
@@ -100,7 +101,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
m_todo.pop_back();
result = check1(curr.get(), side_conditions);
if (!result) {
- IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m_manager, curr.get()););
+ IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
UNREACHABLE();
}
}
@@ -114,7 +115,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
}
bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) {
- if (p->get_family_id() == m_manager.get_basic_family_id()) {
+ if (p->get_family_id() == m.get_basic_family_id()) {
return check1_basic(p, side_conditions);
}
#if 0
@@ -129,11 +130,11 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
#if 0
decl_kind k = p->get_decl_kind();
bool is_univ = false;
- expr_ref fact(m_manager), fml(m_manager);
- expr_ref body(m_manager), fml1(m_manager), fml2(m_manager);
- sort_ref_vector sorts(m_manager);
- proof_ref p1(m_manager), p2(m_manager);
- proof_ref_vector proofs(m_manager);
+ expr_ref fact(m), fml(m);
+ expr_ref body(m), fml1(m), fml2(m);
+ sort_ref_vector sorts(m);
+ proof_ref p1(m), p2(m);
+ proof_ref_vector proofs(m);
if (match_proof(p, proofs)) {
for (unsigned i = 0; i < proofs.size(); ++i) {
@@ -159,15 +160,15 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
case PR_FACTORING:
case PR_SPC_DER: {
if (match_fact(p, fact)) {
- expr_ref_vector rewrite_eq(m_manager);
+ expr_ref_vector rewrite_eq(m);
rewrite_eq.push_back(fact.get());
for (unsigned i = 0; i < proofs.size(); ++i) {
if (match_fact(proofs[i].get(), fml)) {
- rewrite_eq.push_back(m_manager.mk_not(fml.get()));
+ rewrite_eq.push_back(m.mk_not(fml.get()));
}
}
- expr_ref rewrite_cond(m_manager);
- rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
+ expr_ref rewrite_cond(m);
+ rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
side_conditions.push_back(rewrite_cond.get());
return true;
}
@@ -184,18 +185,18 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
decl_kind k = p->get_decl_kind();
- expr_ref fml0(m_manager), fml1(m_manager), fml2(m_manager), fml(m_manager);
- expr_ref t1(m_manager), t2(m_manager);
- expr_ref s1(m_manager), s2(m_manager);
- expr_ref u1(m_manager), u2(m_manager);
- expr_ref fact(m_manager), body1(m_manager), body2(m_manager);
- expr_ref l1(m_manager), l2(m_manager), r1(m_manager), r2(m_manager);
- func_decl_ref d1(m_manager), d2(m_manager), d3(m_manager);
- proof_ref p0(m_manager), p1(m_manager), p2(m_manager);
- proof_ref_vector proofs(m_manager);
- func_decl_ref f1(m_manager), f2(m_manager);
- expr_ref_vector terms1(m_manager), terms2(m_manager), terms(m_manager);
- sort_ref_vector decls1(m_manager), decls2(m_manager);
+ expr_ref fml0(m), fml1(m), fml2(m), fml(m);
+ expr_ref t1(m), t2(m);
+ expr_ref s1(m), s2(m);
+ expr_ref u1(m), u2(m);
+ expr_ref fact(m), body1(m), body2(m);
+ expr_ref l1(m), l2(m), r1(m), r2(m);
+ func_decl_ref d1(m), d2(m), d3(m);
+ proof_ref p0(m), p1(m), p2(m);
+ proof_ref_vector proofs(m);
+ func_decl_ref f1(m), f2(m);
+ expr_ref_vector terms1(m), terms2(m), terms(m);
+ sort_ref_vector decls1(m), decls2(m);
if (match_proof(p, proofs)) {
for (unsigned i = 0; i < proofs.size(); ++i) {
@@ -296,7 +297,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false;
}
case PR_MONOTONICITY: {
- TRACE("proof_checker", tout << mk_bounded_pp(p, m_manager, 3) << "\n";);
+ TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
if (match_fact(p, fact) &&
match_binary(fact.get(), d1, t1, t2) &&
match_app(t1.get(), f1, terms1) &&
@@ -334,7 +335,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_fact(p1.get(), fml) &&
(match_iff(fact.get(), t1, t2) || match_oeq(fact.get(), t1, t2)) &&
(match_iff(fml.get(), s1, s2) || match_oeq(fml.get(), s1, s2)) &&
- m_manager.is_oeq(fact.get()) == m_manager.is_oeq(fml.get()) &&
+ m.is_oeq(fact.get()) == m.is_oeq(fml.get()) &&
is_quantifier(t1.get()) &&
is_quantifier(t2.get()) &&
to_quantifier(t1.get())->get_expr() == s1.get() &&
@@ -366,7 +367,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false;
}
case PR_AND_ELIM: {
- expr_ref_vector terms(m_manager);
+ expr_ref_vector terms(m);
if (match_proof(p, p1) &&
match_fact(p, fact) &&
match_fact(p1.get(), fml) &&
@@ -381,7 +382,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false;
}
case PR_NOT_OR_ELIM: {
- expr_ref_vector terms(m_manager);
+ expr_ref_vector terms(m);
if (match_proof(p, p1) &&
match_fact(p, fact) &&
match_fact(p1.get(), fml) &&
@@ -403,25 +404,25 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
side_conditions.push_back(fact.get());
return true;
}
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager););
+ IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_REWRITE_STAR: {
if (match_fact(p, fact) &&
match_equiv(fact.get(), t1, t2)) {
- expr_ref_vector rewrite_eq(m_manager);
+ expr_ref_vector rewrite_eq(m);
rewrite_eq.push_back(fact.get());
for (unsigned i = 0; i < proofs.size(); ++i) {
if (match_fact(proofs[i].get(), fml)) {
- rewrite_eq.push_back(m_manager.mk_not(fml.get()));
+ rewrite_eq.push_back(m.mk_not(fml.get()));
}
}
- expr_ref rewrite_cond(m_manager);
- rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
+ expr_ref rewrite_cond(m);
+ rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
side_conditions.push_back(rewrite_cond.get());
return true;
}
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager););
+ IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_PULL_QUANT: {
@@ -432,7 +433,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD: check the enchilada.
return true;
}
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m_manager););
+ IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_PULL_QUANT_STAR: {
@@ -442,7 +443,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD: check the enchilada.
return true;
}
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m_manager););
+ IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_PUSH_QUANT: {
@@ -509,9 +510,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
if (match_proof(p, p1) &&
match_fact(p, fact) &&
match_fact(p1.get(), fml) &&
- m_manager.is_false(fml.get())) {
- expr_ref_vector hypotheses(m_manager);
- expr_ref_vector ors(m_manager);
+ m.is_false(fml.get())) {
+ expr_ref_vector hypotheses(m);
+ expr_ref_vector ors(m);
get_hypotheses(p1.get(), hypotheses);
if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
// Suppose fact is (or a b c) and hypothesis is (not (or a b c))
@@ -531,18 +532,18 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
tout << "i: " << i << "\n";
tout << "ORs:\n";
for (unsigned i = 0; i < ors.size(); i++) {
- tout << mk_pp(ors.get(i), m_manager) << "\n";
+ tout << mk_pp(ors.get(i), m) << "\n";
}
tout << "HYPOTHESIS:\n";
for (unsigned i = 0; i < hypotheses.size(); i++) {
- tout << mk_pp(hypotheses.get(i), m_manager) << "\n";
+ tout << mk_pp(hypotheses.get(i), m) << "\n";
});
UNREACHABLE();
return false;
}
TRACE("proof_checker", tout << "Matched:\n";
- ast_ll_pp(tout, m_manager, hypotheses[i].get());
- ast_ll_pp(tout, m_manager, ors[j-1].get()););
+ ast_ll_pp(tout, m, hypotheses[i].get());
+ ast_ll_pp(tout, m, ors[j-1].get()););
}
return true;
}
@@ -555,7 +556,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_fact(proofs[0].get(), fml1) &&
match_fact(proofs[1].get(), fml2) &&
match_negated(fml1.get(), fml2.get()) &&
- m_manager.is_false(fact.get())) {
+ m.is_false(fact.get())) {
return true;
}
if (match_fact(p, fact) &&
@@ -580,15 +581,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
TRACE("pr_unit_bug",
tout << "Parents:\n";
for (unsigned i = 0; i < proofs.size(); i++) {
- expr_ref p(m_manager);
+ expr_ref p(m);
match_fact(proofs.get(i), p);
- tout << mk_pp(p, m_manager) << "\n";
+ tout << mk_pp(p, m) << "\n";
}
tout << "Fact:\n";
- tout << mk_pp(fact, m_manager) << "\n";
+ tout << mk_pp(fact, m) << "\n";
tout << "Clause:\n";
- tout << mk_pp(fml, m_manager) << "\n";
- tout << "Could not find premise " << mk_pp(fml2, m_manager) << "\n";
+ tout << mk_pp(fml, m) << "\n";
+ tout << "Could not find premise " << mk_pp(fml2, m) << "\n";
);
UNREACHABLE();
@@ -597,7 +598,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
}
switch(terms1.size()) {
case 0:
- return m_manager.is_false(fact.get());
+ return m.is_false(fact.get());
case 1:
return fact.get() == terms1[0].get();
default: {
@@ -609,15 +610,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
found = term1 == terms2[j].get();
}
if (!found) {
- IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m_manager) << "\n";);
+ IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
return false;
}
}
return true;
}
IF_VERBOSE(0, verbose_stream() << "Conclusion is not a disjunction:\n";
- verbose_stream() << mk_pp(fml.get(), m_manager) << "\n";
- verbose_stream() << mk_pp(fact.get(), m_manager) << "\n";);
+ verbose_stream() << mk_pp(fml.get(), m) << "\n";
+ verbose_stream() << mk_pp(fact.get(), m) << "\n";);
return false;
}
@@ -634,7 +635,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_fact(p1.get(), fml1) &&
match_iff(fact.get(), l1, r1) &&
fml1.get() == l1.get() &&
- r1.get() == m_manager.mk_true()) {
+ r1.get() == m.mk_true()) {
return true;
}
UNREACHABLE();
@@ -648,7 +649,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_iff(fact.get(), l1, r1) &&
match_not(fml1.get(), t1) &&
t1.get() == l1.get() &&
- r1.get() == m_manager.mk_false()) {
+ r1.get() == m.mk_false()) {
return true;
}
UNREACHABLE();
@@ -674,7 +675,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// axiom(?fml)
if (match_fact(p, fact) &&
match_proof(p) &&
- m_manager.is_bool(fact.get())) {
+ m.is_bool(fact.get())) {
return true;
}
UNREACHABLE();
@@ -689,7 +690,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
//
if (match_fact(p, fact) &&
match_proof(p) &&
- m_manager.is_bool(fact.get())) {
+ m.is_bool(fact.get())) {
return true;
}
UNREACHABLE();
@@ -790,16 +791,138 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TODO
return true;
}
+ case PR_HYPER_RESOLVE: {
+ proof_ref_vector premises(m);
+ expr_ref_vector fmls(m);
+ expr_ref conclusion(m), premise(m), premise0(m), premise1(m);
+ svector > positions;
+ vector substs;
+ VERIFY(m.is_hyper_resolve(p, premises, conclusion, positions, substs));
+ var_subst vs(m, false);
+ for (unsigned i = 0; i < premises.size(); ++i) {
+ expr_ref_vector const& sub = substs[i];
+ premise = m.get_fact(premises[i].get());
+ if (!sub.empty()) {
+ if (is_forall(premise)) {
+ // SASSERT(to_quantifier(premise)->get_num_decls() == sub.size());
+ premise = to_quantifier(premise)->get_expr();
+ }
+ vs(premise, sub.size(), sub.c_ptr(), premise);
+ }
+ fmls.push_back(premise.get());
+ TRACE("proof_checker",
+ tout << mk_pp(premise.get(), m) << "\n";
+ for (unsigned j = 0; j < sub.size(); ++j) {
+ tout << mk_pp(sub[j], m) << " ";
+ }
+ tout << "\n";);
+ }
+ premise0 = fmls[0].get();
+ for (unsigned i = 1; i < fmls.size(); ++i) {
+ expr_ref lit1(m), lit2(m);
+ expr* lit3 = 0;
+ std::pair pos = positions[i-1];
+ premise1 = fmls[i].get();
+ set_false(premise0, pos.first, lit1);
+ set_false(premise1, pos.second, lit2);
+ if (m.is_not(lit1, lit3) && lit3 == lit2) {
+ // ok
+ }
+ else if (m.is_not(lit2, lit3) && lit3 == lit1) {
+ // ok
+ }
+ else {
+ IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" <<
+ mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
+ }
+ fmls[i] = premise1;
+ }
+ fmls[0] = premise0;
+ premise0 = m.mk_or(fmls.size(), fmls.c_ptr());
+ if (is_forall(conclusion)) {
+ quantifier* q = to_quantifier(conclusion);
+ premise0 = m.mk_iff(premise0, q->get_expr());
+ premise0 = m.mk_forall(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), premise0);
+ }
+ else {
+ premise0 = m.mk_iff(premise0, conclusion);
+ }
+ side_conditions.push_back(premise0);
+ return true;
+ }
default:
UNREACHABLE();
return false;
}
}
+/**
+ \brief Premises of the rules are of the form
+ (or l0 l1 l2 .. ln)
+ or
+ (=> (and ln+1 ln+2 .. ln+m) l0)
+ or in the most general (ground) form:
+ (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
+ In other words we use the following (Prolog style) convention for Horn
+ implications:
+ The head of a Horn implication is position 0,
+ the first conjunct in the body of an implication is position 1
+ the second conjunct in the body of an implication is position 2
+
+ Set the position provided in the argument to 'false'.
+*/
+void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
+ app* a = to_app(e);
+ expr* head, *body;
+ expr_ref_vector args(m);
+ if (m.is_or(e)) {
+ SASSERT(position < a->get_num_args());
+ args.append(a->get_num_args(), a->get_args());
+ lit = args[position].get();
+ args[position] = m.mk_false();
+ e = m.mk_or(args.size(), args.c_ptr());
+ }
+ else if (m.is_implies(e, body, head)) {
+ expr* const* heads = &head;
+ unsigned num_heads = 1;
+ if (m.is_or(head)) {
+ num_heads = to_app(head)->get_num_args();
+ heads = to_app(head)->get_args();
+ }
+ expr*const* bodies = &body;
+ unsigned num_bodies = 1;
+ if (m.is_and(body)) {
+ num_bodies = to_app(body)->get_num_args();
+ bodies = to_app(body)->get_args();
+ }
+ if (position < num_heads) {
+ args.append(num_heads, heads);
+ lit = args[position].get();
+ args[position] = m.mk_false();
+ e = m.mk_implies(body, m.mk_or(args.size(), args.c_ptr()));
+ }
+ else {
+ position -= num_heads;
+ args.append(num_bodies, bodies);
+ lit = m.mk_not(args[position].get());
+ args[position] = m.mk_true();
+ e = m.mk_implies(m.mk_and(args.size(), args.c_ptr()), head);
+ }
+ }
+ else if (position == 0) {
+ lit = e;
+ e = m.mk_false();
+ }
+ else {
+ IF_VERBOSE(0, verbose_stream() << position << "\n" << mk_pp(e, m) << "\n";);
+ UNREACHABLE();
+ }
+}
+
bool proof_checker::match_fact(proof* p, expr_ref& fact) {
- if (m_manager.is_proof(p) &&
- m_manager.has_fact(p)) {
- fact = m_manager.get_fact(p);
+ if (m.is_proof(p) &&
+ m.has_fact(p)) {
+ fact = m.get_fact(p);
return true;
}
return false;
@@ -814,33 +937,33 @@ void proof_checker::add_premise(proof* p) {
bool proof_checker::match_proof(proof* p) {
return
- m_manager.is_proof(p) &&
- m_manager.get_num_parents(p) == 0;
+ m.is_proof(p) &&
+ m.get_num_parents(p) == 0;
}
bool proof_checker::match_proof(proof* p, proof_ref& p0) {
- if (m_manager.is_proof(p) &&
- m_manager.get_num_parents(p) == 1) {
- p0 = m_manager.get_parent(p, 0);
+ if (m.is_proof(p) &&
+ m.get_num_parents(p) == 1) {
+ p0 = m.get_parent(p, 0);
return true;
}
return false;
}
bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
- if (m_manager.is_proof(p) &&
- m_manager.get_num_parents(p) == 2) {
- p0 = m_manager.get_parent(p, 0);
- p1 = m_manager.get_parent(p, 1);
+ if (m.is_proof(p) &&
+ m.get_num_parents(p) == 2) {
+ p0 = m.get_parent(p, 0);
+ p1 = m.get_parent(p, 1);
return true;
}
return false;
}
bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
- if (m_manager.is_proof(p)) {
- for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
- parents.push_back(m_manager.get_parent(p, i));
+ if (m.is_proof(p)) {
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ parents.push_back(m.get_parent(p, i));
}
return true;
}
@@ -886,7 +1009,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
if (e->get_kind() == AST_APP &&
- to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+ to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
to_app(e)->get_num_args() == 2) {
t1 = to_app(e)->get_arg(0);
@@ -898,7 +1021,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
if (e->get_kind() == AST_APP &&
- to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+ to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k) {
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
terms.push_back(to_app(e)->get_arg(i));
@@ -911,7 +1034,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
if (e->get_kind() == AST_APP &&
- to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+ to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
to_app(e)->get_num_args() == 1) {
t = to_app(e)->get_arg(0);
@@ -953,7 +1076,7 @@ bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
}
bool proof_checker::match_negated(expr* a, expr* b) {
- expr_ref t(m_manager);
+ expr_ref t(m);
return
(match_not(a, t) && t.get() == b) ||
(match_not(b, t) && t.get() == a);
@@ -961,7 +1084,7 @@ bool proof_checker::match_negated(expr* a, expr* b) {
void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
ptr_buffer buffer;
- if (m_manager.is_or(e)) {
+ if (m.is_or(e)) {
app* a = to_app(e);
ors.append(a->get_num_args(), a->get_args());
}
@@ -974,12 +1097,12 @@ void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
ptr_vector stack;
expr* h = 0;
- expr_ref hyp(m_manager);
+ expr_ref hyp(m);
stack.push_back(p);
while (!stack.empty()) {
p = stack.back();
- SASSERT(m_manager.is_proof(p));
+ SASSERT(m.is_proof(p));
if (m_hypotheses.contains(p)) {
stack.pop_back();
continue;
@@ -992,15 +1115,15 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
continue;
}
// in this system all hypotheses get bound by lemmas.
- if (m_manager.is_lemma(p)) {
+ if (m.is_lemma(p)) {
m_hypotheses.insert(p, mk_nil());
stack.pop_back();
continue;
}
bool all_found = true;
ptr_vector hyps;
- for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
- proof* p_i = m_manager.get_parent(p, i);
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ proof* p_i = m.get_parent(p, i);
if (m_hypotheses.find(p_i, h)) {
hyps.push_back(h);
}
@@ -1028,7 +1151,7 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
ptr_buffer todo;
expr_mark mark;
todo.push_back(h);
- expr_ref a(m_manager), b(m_manager);
+ expr_ref a(m), b(m);
while (!todo.empty()) {
h = todo.back();
@@ -1051,10 +1174,10 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
}
TRACE("proof_checker",
{
- ast_ll_pp(tout << "Getting hypotheses from: ", m_manager, p);
+ ast_ll_pp(tout << "Getting hypotheses from: ", m, p);
tout << "Found hypotheses:\n";
for (unsigned i = 0; i < ante.size(); ++i) {
- ast_ll_pp(tout, m_manager, ante[i].get());
+ ast_ll_pp(tout, m, ante[i].get());
}
});
@@ -1090,11 +1213,11 @@ bool proof_checker::match_atom(expr* e, expr_ref& a) const {
}
expr* proof_checker::mk_atom(expr* e) {
- return m_manager.mk_app(m_hyp_fid, OP_ATOM, e);
+ return m.mk_app(m_hyp_fid, OP_ATOM, e);
}
expr* proof_checker::mk_cons(expr* a, expr* b) {
- return m_manager.mk_app(m_hyp_fid, OP_CONS, a, b);
+ return m.mk_app(m_hyp_fid, OP_CONS, a, b);
}
expr* proof_checker::mk_nil() {
@@ -1103,7 +1226,7 @@ expr* proof_checker::mk_nil() {
bool proof_checker::is_hypothesis(proof* p) const {
return
- m_manager.is_proof(p) &&
+ m.is_proof(p) &&
p->get_decl_kind() == PR_HYPOTHESIS;
}
@@ -1130,14 +1253,14 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
void proof_checker::dump_proof(proof * pr) {
if (!m_dump_lemmas)
return;
- SASSERT(m_manager.has_fact(pr));
- expr * consequent = m_manager.get_fact(pr);
- unsigned num = m_manager.get_num_parents(pr);
+ SASSERT(m.has_fact(pr));
+ expr * consequent = m.get_fact(pr);
+ unsigned num = m.get_num_parents(pr);
ptr_buffer antecedents;
for (unsigned i = 0; i < num; i++) {
- proof * a = m_manager.get_parent(pr, i);
- SASSERT(m_manager.has_fact(a));
- antecedents.push_back(m_manager.get_fact(a));
+ proof * a = m.get_parent(pr, i);
+ SASSERT(m.has_fact(a));
+ antecedents.push_back(m.get_fact(a));
}
dump_proof(antecedents.size(), antecedents.c_ptr(), consequent);
}
@@ -1150,21 +1273,20 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
sprintf(buffer, "proof_lemma_%d.smt", m_proof_lemma_id);
#endif
std::ofstream out(buffer);
- ast_smt_pp pp(m_manager);
+ ast_smt_pp pp(m);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(m_logic.c_str());
for (unsigned i = 0; i < num_antecedents; i++)
pp.add_assumption(antecedents[i]);
- expr_ref n(m_manager);
- n = m_manager.mk_not(consequent);
+ expr_ref n(m);
+ n = m.mk_not(consequent);
pp.display(out, n);
out.close();
m_proof_lemma_id++;
}
bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) {
- ast_manager& m = m_manager;
arith_util a(m);
app* lit = lit0;
@@ -1173,7 +1295,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
is_pos = !is_pos;
}
if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
- std::cout << mk_pp(lit, m) << "\n";
+ IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
return false;
}
SASSERT(lit->get_num_args() == 2);
@@ -1237,7 +1359,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
rw(sum);
}
- std::cout << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";
+ IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
#endif
return true;
@@ -1247,7 +1369,6 @@ bool proof_checker::check_arith_proof(proof* p) {
func_decl* d = p->get_decl();
SASSERT(PR_TH_LEMMA == p->get_decl_kind());
SASSERT(d->get_parameter(0).get_symbol() == "arith");
- ast_manager& m = m_manager;
unsigned num_params = d->get_num_parameters();
arith_util autil(m);
@@ -1257,7 +1378,7 @@ bool proof_checker::check_arith_proof(proof* p) {
return true;
}
expr_ref fact(m);
- proof_ref_vector proofs(m_manager);
+ proof_ref_vector proofs(m);
if (!match_fact(p, fact)) {
UNREACHABLE();
@@ -1331,7 +1452,7 @@ bool proof_checker::check_arith_proof(proof* p) {
rw(sum);
if (!m.is_false(sum)) {
- std::cout << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";
+ IF_VERBOSE(0, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
m_dump_lemmas = true;
dump_proof(p);
return false;
diff --git a/src/ast/proof_checker/proof_checker.h b/src/ast/proof_checker/proof_checker.h
index 6704f154a..9c5f8a749 100644
--- a/src/ast/proof_checker/proof_checker.h
+++ b/src/ast/proof_checker/proof_checker.h
@@ -23,7 +23,7 @@ Revision History:
#include "map.h"
class proof_checker {
- ast_manager& m_manager;
+ ast_manager& m;
proof_ref_vector m_todo;
expr_mark m_marked;
expr_ref_vector m_pinned;
@@ -111,6 +111,8 @@ private:
expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
void dump_proof(proof * pr);
void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
+
+ void set_false(expr_ref& e, unsigned idx, expr_ref& lit);
};
#endif
diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp
index 6e44c68f2..81b2f7be6 100644
--- a/src/ast/substitution/substitution_tree.cpp
+++ b/src/ast/substitution/substitution_tree.cpp
@@ -610,7 +610,7 @@ void substitution_tree::display(std::ostream & out, node * n, unsigned delta) co
pp_params p;
p.m_pp_single_line = true;
out << " ==> ";
- ast_pp(out, n->m_expr, m_manager, p);
+ out << mk_pp(n->m_expr, m_manager, p);
out << "\n";
}
else {
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 1be6fe395..225f0be87 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -459,7 +459,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "UFNIA" ||
s == "LIA" ||
s == "LRA" ||
- s == "QF_FPA" ;
+ s == "QF_FPA" ||
+ s == "HORN";
}
bool cmd_context::logic_has_arith() const {
@@ -479,6 +480,12 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
s == "QF_BVRE";
}
+bool cmd_context::logic_has_horn(symbol const& s) const {
+ return
+ s == "HORN";
+
+}
+
bool cmd_context::logic_has_bv() const {
return !has_logic() || logic_has_bv_core(m_logic);
}
@@ -589,6 +596,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
return s == "QF_UF" || s == "UF" ||
logic_has_arith_core(s) || logic_has_bv_core(s) ||
logic_has_array_core(s) || logic_has_seq_core(s) ||
+ logic_has_horn(s) ||
s == "QF_FPA";
}
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 34a3375d7..5f83e0224 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -233,6 +233,7 @@ protected:
bool logic_has_bv_core(symbol const & s) const;
bool logic_has_array_core(symbol const & s) const;
bool logic_has_seq_core(symbol const & s) const;
+ bool logic_has_horn(symbol const& s) const;
bool logic_has_arith() const;
bool logic_has_bv() const;
bool logic_has_seq() const;
diff --git a/src/math/euclid/README b/src/math/euclid/README
new file mode 100644
index 000000000..7235cd76f
--- /dev/null
+++ b/src/math/euclid/README
@@ -0,0 +1,2 @@
+Basic Euclidean solver for linear integer equations.
+This solver generates "explanations".
\ No newline at end of file
diff --git a/src/math/interval/README b/src/math/interval/README
new file mode 100644
index 000000000..75aa2e9c6
--- /dev/null
+++ b/src/math/interval/README
@@ -0,0 +1,2 @@
+Template for interval arithmetic. The template can be instantiated using different numeral (integers/mpz, rationals/mpq, floating-point/mpf, etc) packages.
+The class im_default_config defines a default configuration for the template that uses rationals. It also shows what is the expected signature used by the template.
\ No newline at end of file
diff --git a/src/math/polynomial/README b/src/math/polynomial/README
new file mode 100644
index 000000000..5d079eea0
--- /dev/null
+++ b/src/math/polynomial/README
@@ -0,0 +1,3 @@
+Polynomial manipulation package.
+It contains support for univariate (upolynomial.*) and multivariate polynomials (polynomial.*).
+Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled.
\ No newline at end of file
diff --git a/src/muz_qe/dl_base.cpp b/src/muz_qe/dl_base.cpp
index 5556920f0..89ebc7e4e 100644
--- a/src/muz_qe/dl_base.cpp
+++ b/src/muz_qe/dl_base.cpp
@@ -47,7 +47,7 @@ namespace datalog {
out<<"(";
for(unsigned i=0; i
class dl_context {
cmd_context & m_cmd;
+ dl_collected_cmds* m_collected_cmds;
unsigned m_ref_count;
datalog::dl_decl_plugin* m_decl_plugin;
- scoped_ptr m_context;
+ scoped_ptr m_context;
+ trail_stack m_trail;
public:
- dl_context(cmd_context & ctx):
+ dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
m_cmd(ctx),
+ m_collected_cmds(collected_cmds),
m_ref_count(0),
- m_decl_plugin(0) {}
+ m_decl_plugin(0),
+ m_trail(*this) {}
void inc_ref() {
++m_ref_count;
@@ -74,14 +79,53 @@ public:
void reset() {
m_context = 0;
}
+
+ void register_predicate(func_decl* pred, unsigned num_kinds, symbol const* kinds) {
+ if (m_collected_cmds) {
+ m_collected_cmds->m_rels.push_back(pred);
+ m_trail.push(push_back_vector(m_collected_cmds->m_rels));
+ }
+ dlctx().register_predicate(pred, false);
+ dlctx().set_predicate_representation(pred, num_kinds, kinds);
+ }
void add_rule(expr * rule, symbol const& name) {
init();
- std::string error_msg;
- m_context->add_rule(rule, name);
+ if (m_collected_cmds) {
+ expr_ref rl = m_context->bind_variables(rule, true);
+ m_collected_cmds->m_rules.push_back(rl);
+ m_collected_cmds->m_names.push_back(name);
+ m_trail.push(push_back_vector(m_collected_cmds->m_rules));
+ m_trail.push(push_back_vector >(m_collected_cmds->m_names));
+ }
+ else {
+ m_context->add_rule(rule, name);
+ }
}
+
+ bool collect_query(expr* q) {
+ if (m_collected_cmds) {
+ expr_ref qr = m_context->bind_variables(q, false);
+ m_collected_cmds->m_queries.push_back(qr);
+ m_trail.push(push_back_vector(m_collected_cmds->m_queries));
+ return true;
+ }
+ else {
+ return false;
+ }
+ }
+
+ void push() {
+ m_trail.push_scope();
+ dlctx().push();
+ }
+
+ void pop() {
+ m_trail.pop_scope(1);
+ dlctx().pop();
+ }
- datalog::context & get_dl_context() {
+ datalog::context & dlctx() {
init();
return *m_context;
}
@@ -160,7 +204,10 @@ public:
if (m_target == 0) {
throw cmd_exception("invalid query command, argument expected");
}
- datalog::context& dlctx = m_dl_ctx->get_dl_context();
+ if (m_dl_ctx->collect_query(m_target)) {
+ return;
+ }
+ datalog::context& dlctx = m_dl_ctx->dlctx();
set_background(ctx);
dlctx.updt_params(m_params);
unsigned timeout = m_params.get_uint(":timeout", UINT_MAX);
@@ -217,7 +264,7 @@ public:
}
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
- m_dl_ctx->get_dl_context().collect_params(p);
+ m_dl_ctx->dlctx().collect_params(p);
insert_timeout(p);
p.insert(":print-answer", CPK_BOOL, "(default: false) print answer instance(s) to query.");
p.insert(":print-certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability.");
@@ -227,7 +274,7 @@ public:
private:
void set_background(cmd_context& ctx) {
- datalog::context& dlctx = m_dl_ctx->get_dl_context();
+ datalog::context& dlctx = m_dl_ctx->dlctx();
ptr_vector::const_iterator it = ctx.begin_assertions();
ptr_vector::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
@@ -237,7 +284,7 @@ private:
void print_answer(cmd_context& ctx) {
if (m_params.get_bool(":print-answer", false)) {
- datalog::context& dlctx = m_dl_ctx->get_dl_context();
+ datalog::context& dlctx = m_dl_ctx->dlctx();
ast_manager& m = ctx.m();
expr_ref query_result(dlctx.get_answer_as_formula(), m);
sbuffer var_names;
@@ -253,7 +300,7 @@ private:
void print_statistics(cmd_context& ctx) {
if (m_params.get_bool(":print-statistics", false)) {
statistics st;
- datalog::context& dlctx = m_dl_ctx->get_dl_context();
+ datalog::context& dlctx = m_dl_ctx->dlctx();
unsigned long long max_mem = memory::get_max_used_memory();
unsigned long long mem = memory::get_allocation_size();
dlctx.collect_statistics(st);
@@ -266,7 +313,7 @@ private:
void print_certificate(cmd_context& ctx) {
if (m_params.get_bool(":print-certificate", false)) {
- datalog::context& dlctx = m_dl_ctx->get_dl_context();
+ datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for selected DL_ENGINE");
}
@@ -286,6 +333,7 @@ class dl_declare_rel_cmd : public cmd {
void ensure_domain(cmd_context& ctx) {
if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
}
+
public:
dl_declare_rel_cmd(dl_context * dl_ctx):
cmd("declare-rel"),
@@ -334,11 +382,7 @@ public:
func_decl_ref pred(
m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
ctx.insert(pred);
- datalog::context& dctx = m_dl_ctx->get_dl_context();
- dctx.register_predicate(pred, false);
- if(!m_kinds.empty()) {
- dctx.set_predicate_representation(pred, m_kinds.size(), m_kinds.c_ptr());
- }
+ m_dl_ctx->register_predicate(pred, m_kinds.size(), m_kinds.c_ptr());
m_domain = 0;
}
@@ -385,7 +429,7 @@ public:
ast_manager& m = ctx.m();
func_decl_ref var(m.mk_func_decl(m_var_name, 0, static_cast(0), m_var_sort), m);
ctx.insert(var);
- m_dl_ctx->get_dl_context().register_variable(var);
+ m_dl_ctx->dlctx().register_variable(var);
}
};
@@ -402,7 +446,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "push context on the fixedpoint engine"; }
virtual void execute(cmd_context& ctx) {
- m_ctx->get_dl_context().push();
+ m_ctx->push();
}
};
@@ -418,19 +462,24 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "pop context on the fixedpoint engine"; }
virtual void execute(cmd_context& ctx) {
- m_ctx->get_dl_context().pop();
+ m_ctx->pop();
}
};
-
-
-void install_dl_cmds(cmd_context & ctx) {
- dl_context * dl_ctx = alloc(dl_context, ctx);
+static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
+ dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
ctx.insert(alloc(dl_rule_cmd, dl_ctx));
ctx.insert(alloc(dl_query_cmd, dl_ctx));
ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
PRIVATE_PARAMS(ctx.insert(alloc(dl_push_cmd, dl_ctx));); // not exposed to keep command-extensions simple.
- PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););
+ PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););
}
+void install_dl_cmds(cmd_context & ctx) {
+ install_dl_cmds_aux(ctx, 0);
+}
+
+void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context & ctx) {
+ install_dl_cmds_aux(ctx, &collected_cmds);
+}
diff --git a/src/muz_qe/dl_cmds.h b/src/muz_qe/dl_cmds.h
index 72eb2dee2..d71b319c4 100644
--- a/src/muz_qe/dl_cmds.h
+++ b/src/muz_qe/dl_cmds.h
@@ -10,7 +10,7 @@ Abstract:
Author:
- Leonardo (leonardo) 2011-03-28
+ Nikolaj Bjorner (nbjorner) 2012-11-17
Notes:
@@ -18,30 +18,20 @@ Notes:
#ifndef _DL_CMDS_H_
#define _DL_CMDS_H_
-class cmd;
+#include "ast.h"
+
class cmd_context;
+struct dl_collected_cmds {
+ expr_ref_vector m_rules;
+ svector m_names;
+ expr_ref_vector m_queries;
+ func_decl_ref_vector m_rels;
+ dl_collected_cmds(ast_manager& m) : m_rules(m), m_queries(m), m_rels(m) {}
+};
+
void install_dl_cmds(cmd_context & ctx);
+void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context& ctx);
-namespace datalog {
-
- class context;
-
- /**
- Create a command for declaring relations which is connected to
- a particular datalog context.
-
- Caller must ensure the returned object is deallocated (e.g. by passing it to a cmd_context).
- */
- cmd * mk_declare_rel_cmd(context& dctx);
-
- /**
- Declare a constant as a universal/existential variable.
- It is implicitly existentially or universally quantified
- by the rules.
- */
- cmd * mk_declare_var_cmd(context& dctx);
-
-}
#endif
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index dd94796a0..ecd9ee5cb 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -49,11 +49,14 @@ Revision History:
#include"dl_skip_table.h"
#endif
#include"for_each_expr.h"
+#include"ast_smt_pp.h"
#include"ast_smt2_pp.h"
#include"expr_functors.h"
#include"dl_mk_partial_equiv.h"
#include"dl_mk_bit_blast.h"
#include"datatype_decl_plugin.h"
+#include"expr_abstract.h"
+
namespace datalog {
@@ -331,8 +334,39 @@ namespace datalog {
m_vars.push_back(m.mk_const(var));
}
+ expr_ref context::bind_variables(expr* fml, bool is_forall) {
+ expr_ref result(m);
+ app_ref_vector const& vars = m_vars;
+ if (vars.empty()) {
+ result = fml;
+ }
+ else {
+ ptr_vector sorts;
+ expr_abstract(m, 0, vars.size(), reinterpret_cast(vars.c_ptr()), fml, result);
+ get_free_vars(result, sorts);
+ if (sorts.empty()) {
+ result = fml;
+ }
+ else {
+ svector names;
+ for (unsigned i = 0; i < sorts.size(); ++i) {
+ if (!sorts[i]) {
+ sorts[i] = m.mk_bool_sort();
+ }
+ names.push_back(symbol(i));
+ }
+ quantifier_ref q(m);
+ q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
+ elim_unused_vars(m, q, result);
+ }
+ }
+ return result;
+ }
+
void context::register_predicate(func_decl * decl, bool named) {
- SASSERT(!m_preds.contains(decl));
+ if (m_preds.contains(decl)) {
+ return;
+ }
m_pinned.push_back(decl);
m_preds.insert(decl);
if (named) {
@@ -429,57 +463,35 @@ namespace datalog {
}
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
- symbol * const relation_names) {
+ symbol const * relation_names) {
relation_manager & rmgr = get_rmanager();
family_id target_kind = null_family_id;
- if (relation_name_cnt==1) {
+ switch (relation_name_cnt) {
+ case 0:
+ return;
+ case 1:
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
- } else {
- relation_plugin * tr_plugin = 0; //table plugin, if there is such
- ptr_vector rel_plugins; //plugins that are not table plugins
- svector rel_kinds; //kinds of plugins that are not table plugins
- for (unsigned i=0; i rel_kinds; // kinds of plugins that are not table plugins
+ family_id rel_kind; // the aggregate kind of non-table plugins
+ for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
- //commented out, because support combining relations with tables using fpr is not yet implemented
- /*if (p.from_table()) {
- if (tr_plugin) {
- //it does not give any extra benefit to have an intersection of two tables.
- //Maybe when we can specify which columns belong to which plugin,
- //it might be of use.
- throw default_exception("two table plugins cannot be specified as relation type");
- }
- tr_plugin = &p;
- }
- else {*/
- rel_plugins.push_back(&p);
- rel_kinds.push_back(p.get_kind());
- /*}*/
+ rel_kinds.push_back(p.get_kind());
}
- SASSERT(!rel_kinds.empty());
- // relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
- family_id rel_kind; //the aggregate kind of non-table plugins
- if (rel_kinds.size()==1) {
+ if (rel_kinds.size() == 1) {
rel_kind = rel_kinds[0];
- // rel_plugin = rel_plugins[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
- // rel_plugin = &prod_plugin;
- }
- if (tr_plugin==0) {
- target_kind = rel_kind;
- }
- else {
- NOT_IMPLEMENTED_YET();
-#if 0
- finite_product_relation_plugin & fprp = finite_product_relation_plugin::get_plugin(rmgr, *rel_plugin);
- finite_product_relation_plugin::rel_spec spec;
-#endif
}
+ target_kind = rel_kind;
+ break;
+ }
}
SASSERT(target_kind != null_family_id);
@@ -958,7 +970,8 @@ namespace datalog {
p.insert(":output-profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions");
p.insert(":output-tuples", CPK_BOOL, "determines whether tuples for output predicates should be output");
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
-
+
+ p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
@@ -1198,7 +1211,6 @@ namespace datalog {
case DATALOG_ENGINE:
return dl_query(query);
case PDR_ENGINE:
- return pdr_query(query);
case QPDR_ENGINE:
return pdr_query(query);
case BMC_ENGINE:
@@ -1219,6 +1231,28 @@ namespace datalog {
m_last_answer = get_manager().mk_true();
}
+ model_ref context::get_model() {
+ switch(get_engine()) {
+ case PDR_ENGINE:
+ case QPDR_ENGINE:
+ ensure_pdr();
+ return m_pdr->get_model();
+ default:
+ return model_ref(alloc(model, m));
+ }
+ }
+
+ proof_ref context::get_proof() {
+ switch(get_engine()) {
+ case PDR_ENGINE:
+ case QPDR_ENGINE:
+ ensure_pdr();
+ return m_pdr->get_proof();
+ default:
+ return proof_ref(m.mk_asserted(m.mk_true()), m);
+ }
+ }
+
void context::ensure_pdr() {
if (!m_pdr.get()) {
m_pdr = alloc(pdr::dl_interface, *this);
@@ -1479,13 +1513,12 @@ namespace datalog {
case DATALOG_ENGINE:
return false;
case PDR_ENGINE:
- m_pdr->display_certificate(out);
- return true;
- case QPDR_ENGINE:
+ ensure_pdr();
m_pdr->display_certificate(out);
return true;
case BMC_ENGINE:
case QBMC_ENGINE:
+ ensure_bmc();
m_bmc->display_certificate(out);
return true;
default:
@@ -1493,20 +1526,31 @@ namespace datalog {
}
}
+ void context::reset_statistics() {
+ if (m_pdr) {
+ m_pdr->reset_statistics();
+ }
+ if (m_bmc) {
+ m_bmc->reset_statistics();
+ }
+ }
- void context::collect_statistics(statistics& st) {
- switch(get_engine()) {
+ void context::collect_statistics(statistics& st) const {
+
+ switch(m_engine) {
case DATALOG_ENGINE:
break;
case PDR_ENGINE:
- m_pdr->collect_statistics(st);
- break;
case QPDR_ENGINE:
- m_pdr->collect_statistics(st);
+ if (m_pdr) {
+ m_pdr->collect_statistics(st);
+ }
break;
case BMC_ENGINE:
case QBMC_ENGINE:
- m_bmc->collect_statistics(st);
+ if (m_bmc) {
+ m_bmc->collect_statistics(st);
+ }
break;
default:
break;
@@ -1564,11 +1608,14 @@ namespace datalog {
expr* const* axioms = m_background.c_ptr();
expr_ref fml(m);
expr_ref_vector rules(m);
+ svector names;
+ bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
{
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
rules.push_back(fml);
+ names.push_back((*it)->name());
}
}
@@ -1586,13 +1633,17 @@ namespace datalog {
if (f->get_family_id() != null_family_id) {
//
}
- else if (is_predicate(f)) {
+ else if (is_predicate(f) && use_fixedpoint_extensions) {
rels.insert(f);
}
else {
funcs.insert(f);
}
}
+
+ if (!use_fixedpoint_extensions) {
+ out << "(set-logic HORN)\n";
+ }
it = funcs.begin(), end = funcs.end();
@@ -1619,23 +1670,51 @@ namespace datalog {
out << "))\n";
}
- declare_vars(rules, fresh_names, out);
-
+ if (use_fixedpoint_extensions) {
+ declare_vars(rules, fresh_names, out);
+ }
for (unsigned i = 0; i < num_axioms; ++i) {
+ SASSERT(use_fixedpoint_extensions);
out << "(assert ";
ast_smt2_pp(out, axioms[i], env, params);
out << ")\n";
}
- for (unsigned i = 0; i < rules.size(); ++i) {
- out << "(rule ";
- ast_smt2_pp(out, rules[i].get(), env, params);
+ for (unsigned i = 0; i < rules.size(); ++i) {
+ out << (use_fixedpoint_extensions?"(rule ":"(assert ");
+ expr* r = rules[i].get();
+ if (symbol::null != names[i]) {
+ out << "(! ";
+ }
+ if (use_fixedpoint_extensions) {
+ ast_smt2_pp(out, r, env, params);
+ }
+ else {
+ out << mk_smt_pp(r, m);
+ }
+ if (symbol::null != names[i]) {
+ out << " :named " << names[i] << ")";
+ }
out << ")\n";
}
- for (unsigned i = 0; i < num_queries; ++i) {
- out << "(query ";
- ast_smt2_pp(out, queries[i], env, params);
- out << ")\n";
+ if (use_fixedpoint_extensions) {
+ for (unsigned i = 0; i < num_queries; ++i) {
+ out << "(query ";
+ ast_smt2_pp(out, queries[i], env, params);
+ out << ")\n";
+ }
+ }
+ else {
+ for (unsigned i = 0; i < num_queries; ++i) {
+ if (num_queries > 1) out << "(push)\n";
+ out << "(assert ";
+ expr_ref q(m);
+ q = m.mk_not(queries[i]);
+ ast_smt2_pp(out, q, env, params);
+ out << ")\n";
+ out << "(check-sat)\n";
+ if (num_queries > 1) out << "(pop)\n";
+ }
}
}
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 462e83ede..a6f8fc5e2 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -184,7 +184,7 @@ namespace datalog {
void register_variable(func_decl* var);
- app_ref_vector const& get_variables() const { return m_vars; }
+ expr_ref bind_variables(expr* fml, bool is_forall);
/**
Register datalog relation.
@@ -242,7 +242,7 @@ namespace datalog {
symbol get_argument_name(const func_decl * pred, unsigned arg_index);
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
- symbol * const relation_names);
+ symbol const * relation_names);
void set_output_predicate(func_decl * pred);
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
@@ -383,6 +383,21 @@ namespace datalog {
lbool query(expr* q);
+ /**
+ \brief retrieve model from inductive invariant that shows query is unsat.
+
+ \pre engine == 'pdr' - this option is only supported for PDR mode.
+ */
+ model_ref get_model();
+
+ /**
+ \brief retrieve proof from derivation of the query.
+
+ \pre engine == 'pdr' - this option is only supported for PDR mode.
+ */
+ proof_ref get_proof();
+
+
/**
Query multiple output relations.
*/
@@ -411,7 +426,9 @@ namespace datalog {
expr* get_answer_as_formula();
- void collect_statistics(statistics& st);
+ void collect_statistics(statistics& st) const;
+
+ void reset_statistics();
/**
\brief Display a certificate for reachability and/or unreachability.
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index b7e31a75d..f92a56a4f 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -116,16 +116,20 @@ namespace datalog {
apply(src, false, UINT_MAX, tail, tail_neg);
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
SASSERT(tail.size()==tail_neg.size());
- res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+ res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize);
res->set_accounting_parent_object(m_context, const_cast(&tgt));
- res->norm_vars(m_rm);
- m_rm.fix_unbound_vars(res, true);
- if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
- res = simpl_rule;
- return true;
+ if (m_normalize) {
+ m_rm.fix_unbound_vars(res, true);
+ if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
+ res = simpl_rule;
+ return true;
+ }
+ else {
+ return false;
+ }
}
else {
- return false;
+ return true;
}
}
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index 1be7ef059..6d5448cd6 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -38,11 +38,12 @@ namespace datalog {
substitution m_subst;
unifier m_unif;
bool m_ready;
+ bool m_normalize;
unsigned m_deltas[2];
public:
rule_unifier(context& ctx)
: m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx),
- m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false) {}
+ m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
/** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
@@ -60,6 +61,13 @@ namespace datalog {
*/
expr_ref_vector get_rule_subst(rule const& r, bool is_tgt);
+ /**
+ Control if bound variables are normalized after unification.
+ The default is 'true': bound variables are re-mapped to an
+ initial segment of de-Bruijn indices.
+ */
+ void set_normalize(bool n) { m_normalize = n; }
+
private:
void apply(app * a, bool is_tgt, app_ref& res);
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index b5e6b9305..9b0af2554 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -33,7 +33,6 @@ Revision History:
#include"for_each_expr.h"
#include"used_vars.h"
#include"var_subst.h"
-#include"expr_abstract.h"
#include"rewriter_def.h"
#include"th_rewriter.h"
#include"ast_smt2_pp.h"
@@ -291,30 +290,7 @@ namespace datalog {
}
void rule_manager::bind_variables(expr* fml, bool is_forall, expr_ref& result) {
- app_ref_vector const& vars = m_ctx.get_variables();
- if (vars.empty()) {
- result = fml;
- }
- else {
- ptr_vector sorts;
- expr_abstract(m, 0, vars.size(), reinterpret_cast(vars.c_ptr()), fml, result);
- get_free_vars(result, sorts);
- if (sorts.empty()) {
- result = fml;
- }
- else {
- svector names;
- for (unsigned i = 0; i < sorts.size(); ++i) {
- if (!sorts[i]) {
- sorts[i] = m.mk_bool_sort();
- }
- names.push_back(symbol(i));
- }
- quantifier_ref q(m);
- q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
- elim_unused_vars(m, q, result);
- }
- }
+ result = m_ctx.bind_variables(fml, is_forall);
}
void rule_manager::flatten_body(app_ref_vector& body) {
@@ -526,7 +502,7 @@ namespace datalog {
}
}
- rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name) {
+ rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name, bool normalize) {
DEBUG_CODE(check_valid_rule(head, n, tail););
unsigned sz = rule::get_obj_size(n);
void * mem = m.get_allocator().allocate(sz);
@@ -588,7 +564,9 @@ namespace datalog {
r->m_positive_cnt = r->m_uninterp_cnt;
}
- r->norm_vars(*this);
+ if (normalize) {
+ r->norm_vars(*this);
+ }
return r;
}
@@ -823,7 +801,7 @@ namespace datalog {
new_tail.push_back(to_app(tmp));
tail_neg.push_back(r->is_neg_tail(i));
}
- r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name());
+ r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name(), false);
// keep old variable indices around so we can compose with substitutions.
// r->norm_vars(*this);
@@ -1068,24 +1046,25 @@ namespace datalog {
us(fml);
sorts.reverse();
- for (unsigned i = 0; i < sorts.size(); ) {
+ for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
- for (unsigned j = 0; i < sorts.size(); ++j) {
- for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
- func_decl_ref f(m);
- std::stringstream _name;
- _name << c;
- if (j > 0) _name << j;
- symbol name(_name.str().c_str());
- if (!us.contains(name)) {
- names.push_back(name);
- ++i;
- }
+ }
+
+ for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
+ for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
+ func_decl_ref f(m);
+ std::stringstream _name;
+ _name << c;
+ if (j > 0) _name << j;
+ symbol name(_name.str().c_str());
+ if (!us.contains(name)) {
+ names.push_back(name);
+ ++i;
}
}
- }
+ }
fml = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml);
}
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 0882a52f3..79a46052c 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -116,7 +116,7 @@ namespace datalog {
\remark A tail may contain negation. tail[i] is assumed to be negated if is_neg != 0 && is_neg[i] == true
*/
rule * mk(app * head, unsigned n, app * const * tail, bool const * is_neg = 0,
- symbol const& name = symbol::null);
+ symbol const& name = symbol::null, bool normalize = true);
/**
\brief Create a rule with the same tail as \c source and with a specified head.
@@ -252,7 +252,7 @@ namespace datalog {
std::ostream& display_smt2(ast_manager& m, std::ostream & out) const;
- symbol const& name() { return m_name; }
+ symbol const& name() const { return m_name; }
unsigned hash() const;
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index d3c87985b..451ec2e7d 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -20,9 +20,6 @@ Revision History:
Notes:
- TODO:
- - fix the slicing with covers.
- -
--*/
@@ -101,6 +98,12 @@ namespace pdr {
}
st.update("PDR num properties", np);
}
+
+ void pred_transformer::reset_statistics() {
+ m_solver.reset_statistics();
+ m_reachable.reset_statistics();
+ m_stats.reset();
+ }
void pred_transformer::init_sig() {
if (m_sig.empty()) {
@@ -972,6 +975,7 @@ namespace pdr {
proof_ref_vector trail(m);
datalog::rule_ref_vector rules_trail(rm);
proof* pr = 0;
+ unifier.set_normalize(false);
todo.push_back(m_root);
while (!todo.empty()) {
model_node* n = todo.back();
@@ -1023,6 +1027,7 @@ namespace pdr {
binding_is_id = is_var(v) && to_var(v)->get_idx() == i;
}
if (rls.size() > 1 || !binding_is_id) {
+ expr_ref tmp(m);
vector substs;
svector > positions;
substs.push_back(binding); // TODO base substitution.
@@ -1030,9 +1035,10 @@ namespace pdr {
datalog::rule& src = *rls[i];
bool unified = unifier.unify_rules(*reduced_rule, 0, src);
if (!unified) {
- std::cout << "Could not unify rules: ";
- reduced_rule->display(dctx, std::cout);
- src.display(dctx, std::cout);
+ IF_VERBOSE(0,
+ verbose_stream() << "Could not unify rules: ";
+ reduced_rule->display(dctx, verbose_stream());
+ src.display(dctx, verbose_stream()););
}
expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true);
TRACE("pdr",
@@ -1041,8 +1047,15 @@ namespace pdr {
}
tout << "\n";
);
+
for (unsigned j = 0; j < substs.size(); ++j) {
- // TODO. apply sub1 to subst.
+ for (unsigned k = 0; k < substs[j].size(); ++k) {
+ var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp);
+ substs[j][k] = tmp;
+ }
+ while (substs[j].size() < sub1.size()) {
+ substs[j].push_back(sub1[substs[j].size()].get());
+ }
}
positions.push_back(std::make_pair(i,0));
@@ -1050,9 +1063,11 @@ namespace pdr {
VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
reduced_rule = r3;
}
+
expr_ref fml_concl(m);
reduced_rule->to_formula(fml_concl);
p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
+
}
cache.insert(n->state(), p1);
rules.insert(n->state(), reduced_rule);
@@ -1335,24 +1350,68 @@ namespace pdr {
if (!ok) {
IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
}
+ for (unsigned i = 0; i < side_conditions.size(); ++i) {
+ expr* cond = side_conditions[i].get();
+ expr_ref tmp(m);
+ tmp = m.mk_not(cond);
+ IF_VERBOSE(2, verbose_stream() << "checking side-condition:\n" << mk_pp(cond, m) << "\n";);
+ smt::kernel solver(m, get_fparams());
+ solver.assert_expr(tmp);
+ lbool res = solver.check();
+ if (res != l_false) {
+ IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
+ verbose_stream() << mk_pp(cond, m) << "\n";
+ );
+ }
+ }
break;
}
case l_false: {
- expr_ref_vector refs(m);
+ expr_ref_vector refs(m), fmls(m);
+ expr_ref tmp(m);
model_ref model;
vector rs;
+ model_converter_ref mc;
get_level_property(m_inductive_lvl, refs, rs);
- inductive_property ex(m, const_cast(m_mc), rs);
+ inductive_property ex(m, mc, rs);
ex.to_model(model);
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
- var_subst vs(m, false);
+ var_subst vs(m, false);
for (; it != end; ++it) {
ptr_vector const& rules = it->m_value->rules();
for (unsigned i = 0; i < rules.size(); ++i) {
- // datalog::rule* rule = rules[i];
- // vs(rule->get_head(),
- // apply interpretation of predicates to rule.
- // create formula and check for unsat.
+ datalog::rule& r = *rules[i];
+ model->eval(r.get_head(), tmp);
+ fmls.push_back(m.mk_not(tmp));
+ unsigned utsz = r.get_uninterpreted_tail_size();
+ unsigned tsz = r.get_tail_size();
+ for (unsigned j = 0; j < utsz; ++j) {
+ model->eval(r.get_tail(j), tmp);
+ fmls.push_back(tmp);
+ }
+ for (unsigned j = utsz; j < tsz; ++j) {
+ fmls.push_back(r.get_tail(j));
+ }
+ tmp = m.mk_and(fmls.size(), fmls.c_ptr());
+ ptr_vector sorts;
+ svector names;
+ get_free_vars(tmp, sorts);
+ for (unsigned i = 0; i < sorts.size(); ++i) {
+ if (!sorts[i]) {
+ sorts[i] = m.mk_bool_sort();
+ }
+ names.push_back(symbol(i));
+ }
+ sorts.reverse();
+ tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
+ smt::kernel solver(m, get_fparams());
+ solver.assert_expr(tmp);
+ lbool res = solver.check();
+ if (res != l_false) {
+ IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
+ verbose_stream() << mk_pp(tmp, m) << "\n";
+ );
+ }
}
}
break;
@@ -1442,7 +1501,14 @@ namespace pdr {
simplify_formulas();
m_last_result = l_false;
TRACE("pdr", display_certificate(tout););
- IF_VERBOSE(1, display_certificate(verbose_stream()););
+ IF_VERBOSE(1, {
+ expr_ref_vector refs(m);
+ vector rs;
+ get_level_property(m_inductive_lvl, refs, rs);
+ model_converter_ref mc;
+ inductive_property ex(m, mc, rs);
+ verbose_stream() << ex.to_string();
+ });
validate();
return l_false;
}
@@ -1477,13 +1543,15 @@ namespace pdr {
}
}
- void context::get_model(model_ref& md) {
+ model_ref context::get_model() {
SASSERT(m_last_result == l_false);
expr_ref_vector refs(m);
vector rs;
+ model_ref md;
get_level_property(m_inductive_lvl, refs, rs);
inductive_property ex(m, m_mc, rs);
ex.to_model(md);
+ return md;
}
proof_ref context::get_proof() const {
@@ -1871,6 +1939,20 @@ namespace pdr {
}
}
+ void context::reset_statistics() {
+ decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+ for (it = m_rels.begin(); it != end; ++it) {
+ it->m_value->reset_statistics();
+ }
+ m_stats.reset();
+ m_pm.reset_statistics();
+
+ for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
+ m_core_generalizers[i]->reset_statistics();
+ }
+
+ }
+
std::ostream& context::display(std::ostream& out) const {
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 0f9af5649..14be82dae 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -132,6 +132,7 @@ namespace pdr {
std::ostream& display(std::ostream& strm) const;
void collect_statistics(statistics& st) const;
+ void reset_statistics();
bool is_reachable(expr* state);
void remove_predecessors(expr_ref_vector& literals);
@@ -275,6 +276,7 @@ namespace pdr {
}
}
virtual void collect_statistics(statistics& st) const {}
+ virtual void reset_statistics() {}
};
class context {
@@ -366,6 +368,7 @@ namespace pdr {
void collect_statistics(statistics& st) const;
+ void reset_statistics();
std::ostream& display(std::ostream& strm) const;
@@ -401,7 +404,7 @@ namespace pdr {
void add_cover(int level, func_decl* pred, expr* property);
- void get_model(model_ref& md);
+ model_ref get_model();
proof_ref get_proof() const;
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 098fd0c56..532019025 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -197,6 +197,10 @@ void dl_interface::collect_statistics(statistics& st) const {
m_context->collect_statistics(st);
}
+void dl_interface::reset_statistics() {
+ m_context->reset_statistics();
+}
+
void dl_interface::display_certificate(std::ostream& out) const {
m_context->display_certificate(out);
}
@@ -218,6 +222,14 @@ void dl_interface::updt_params() {
m_context = alloc(pdr::context, m_ctx.get_fparams(), m_ctx.get_params(), m_ctx.get_manager());
}
+model_ref dl_interface::get_model() {
+ return m_context->get_model();
+}
+
+proof_ref dl_interface::get_proof() {
+ return m_context->get_proof();
+}
+
void dl_interface::collect_params(param_descrs& p) {
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
@@ -239,8 +251,8 @@ void dl_interface::collect_params(param_descrs& p) {
"checking for reachability (not only during cube weakening)"););
PRIVATE_PARAMS(p.insert(":max-num-contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create"););
PRIVATE_PARAMS(p.insert(":try-minimize-core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)"););
- PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"););
- PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"););
+ p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation");
+ p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation");
p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
p.insert(":coalesce-rules", CPK_BOOL, "BMC: (default false) coalesce rules");
}
diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h
index 096583a70..61f56282e 100644
--- a/src/muz_qe/pdr_dl_interface.h
+++ b/src/muz_qe/pdr_dl_interface.h
@@ -57,6 +57,8 @@ namespace pdr {
void collect_statistics(statistics& st) const;
+ void reset_statistics();
+
expr_ref get_answer();
unsigned get_num_levels(func_decl* pred);
@@ -66,8 +68,12 @@ namespace pdr {
void add_cover(int level, func_decl* pred, expr* property);
static void collect_params(param_descrs& p);
-
+
void updt_params();
+
+ model_ref get_model();
+
+ proof_ref get_proof();
};
}
diff --git a/src/muz_qe/pdr_manager.h b/src/muz_qe/pdr_manager.h
index 398f2716f..85f2116e9 100644
--- a/src/muz_qe/pdr_manager.h
+++ b/src/muz_qe/pdr_manager.h
@@ -313,6 +313,8 @@ namespace pdr {
pdr::smt_context* mk_fresh() { return m_contexts.mk_fresh(); }
void collect_statistics(statistics& st) const { m_contexts.collect_statistics(st); }
+
+ void reset_statistics() { m_contexts.reset_statistics(); }
};
}
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index 865bfe32b..574be63b1 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -364,8 +364,7 @@ namespace pdr {
m_core->append(lemmas);
}
- lbool prop_solver::check_assumptions(const expr_ref_vector & atoms)
- {
+ lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) {
return check_assumptions_and_formula(atoms, m.mk_true());
}
@@ -393,5 +392,10 @@ namespace pdr {
void prop_solver::collect_statistics(statistics& st) const {
}
+ void prop_solver::reset_statistics() {
+ }
+
+
+
}
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h
index da0a1b31e..15122a21a 100644
--- a/src/muz_qe/pdr_prop_solver.h
+++ b/src/muz_qe/pdr_prop_solver.h
@@ -122,6 +122,8 @@ namespace pdr {
expr * form);
void collect_statistics(statistics& st) const;
+
+ void reset_statistics();
};
}
diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz_qe/pdr_reachable_cache.cpp
index baa18839c..ed9926f85 100644
--- a/src/muz_qe/pdr_reachable_cache.cpp
+++ b/src/muz_qe/pdr_reachable_cache.cpp
@@ -27,9 +27,6 @@ namespace pdr {
m_ctx(0),
m_ref_holder(m),
m_disj_connector(m),
- m_cache_hits(0),
- m_cache_miss(0),
- m_cache_inserts(0),
m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint(":cache-mode",0)) {
if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
m_ctx = pm.mk_fresh();
@@ -63,13 +60,13 @@ namespace pdr {
break;
case datalog::HASH_CACHE:
- m_cache_inserts++;
+ m_stats.m_inserts++;
m_cache.insert(cube);
m_ref_holder.push_back(cube);
break;
case datalog::CONSTRAINT_CACHE:
- m_cache_inserts++;
+ m_stats.m_inserts++;
TRACE("pdr", tout << mk_pp(cube, m) << "\n";);
add_disjuncted_formula(cube);
break;
@@ -112,14 +109,18 @@ namespace pdr {
UNREACHABLE();
break;
}
- if (found) m_cache_hits++; m_cache_miss++;
+ if (found) m_stats.m_hits++; m_stats.m_miss++;
return found;
}
void reachable_cache::collect_statistics(statistics& st) const {
- st.update("cache inserts", m_cache_inserts);
- st.update("cache miss", m_cache_miss);
- st.update("cache hits", m_cache_hits);
+ st.update("cache inserts", m_stats.m_inserts);
+ st.update("cache miss", m_stats.m_miss);
+ st.update("cache hits", m_stats.m_hits);
+ }
+
+ void reachable_cache::reset_statistics() {
+ m_stats.reset();
}
diff --git a/src/muz_qe/pdr_reachable_cache.h b/src/muz_qe/pdr_reachable_cache.h
index d40e0e703..d8096f15c 100644
--- a/src/muz_qe/pdr_reachable_cache.h
+++ b/src/muz_qe/pdr_reachable_cache.h
@@ -28,15 +28,21 @@ Revision History:
namespace pdr {
class reachable_cache {
+ struct stats {
+ unsigned m_hits;
+ unsigned m_miss;
+ unsigned m_inserts;
+ stats() { reset(); }
+ void reset() { memset(this, 0, sizeof(*this)); }
+ };
+
ast_manager & m;
manager & m_pm;
scoped_ptr m_ctx;
ast_ref_vector m_ref_holder;
app_ref m_disj_connector;
obj_hashtable m_cache;
- unsigned m_cache_hits;
- unsigned m_cache_miss;
- unsigned m_cache_inserts;
+ stats m_stats;
datalog::PDR_CACHE_MODE m_cache_mode;
void add_disjuncted_formula(expr * f);
@@ -53,6 +59,8 @@ namespace pdr {
bool is_reachable(expr * cube);
void collect_statistics(statistics& st) const;
+
+ void reset_statistics();
};
}
diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp
index 36b8e2325..d79192769 100644
--- a/src/muz_qe/pdr_smt_context_manager.cpp
+++ b/src/muz_qe/pdr_smt_context_manager.cpp
@@ -136,6 +136,12 @@ namespace pdr {
}
}
+ void smt_context_manager::reset_statistics() {
+ for (unsigned i = 0; i < m_contexts.size(); ++i) {
+ m_contexts[i]->reset_statistics();
+ }
+ }
+
};
diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h
index d6aef9776..31fb8ccb3 100644
--- a/src/muz_qe/pdr_smt_context_manager.h
+++ b/src/muz_qe/pdr_smt_context_manager.h
@@ -100,6 +100,7 @@ namespace pdr {
~smt_context_manager();
smt_context* mk_fresh();
void collect_statistics(statistics& st) const;
+ void reset_statistics();
bool is_aux_predicate(func_decl* p) const { return m_predicate_set.contains(p); }
};
diff --git a/src/muz_qe/pdr_tactic.cpp b/src/muz_qe/pdr_tactic.cpp
new file mode 100644
index 000000000..6b1b13e67
--- /dev/null
+++ b/src/muz_qe/pdr_tactic.cpp
@@ -0,0 +1,286 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ pdr_tactic.h
+
+Abstract:
+
+ PDR as a tactic to solve Horn clauses.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2012-11-16.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"model_converter.h"
+#include"proof_converter.h"
+#include"pdr_tactic.h"
+#include"dl_context.h"
+
+class pdr_tactic : public tactic {
+ struct imp {
+ ast_manager& m;
+ datalog::context m_ctx;
+ front_end_params m_fparams;
+
+ imp(ast_manager & m, params_ref const & p):
+ m(m),
+ m_ctx(m, m_fparams) {
+ updt_params(p);
+ }
+
+ void updt_params(params_ref const & p) {
+ m_ctx.updt_params(p);
+ }
+
+ void collect_param_descrs(param_descrs & r) {
+ m_ctx.collect_params(r);
+ }
+
+ void reset_statistics() {
+ m_ctx.reset_statistics();
+ }
+
+ void collect_statistics(statistics & st) const {
+ m_ctx.collect_statistics(st);
+ }
+
+ void set_cancel(bool f) {
+ if (f) {
+ m_ctx.cancel();
+ }
+ }
+
+ void normalize(expr_ref& f) {
+ bool is_positive = true;
+ expr* e = 0;
+ while (true) {
+ if (is_forall(f) && is_positive) {
+ f = to_quantifier(f)->get_expr();
+ }
+ else if (is_exists(f) && !is_positive) {
+ f = to_quantifier(f)->get_expr();
+ }
+ else if (m.is_not(f, e)) {
+ is_positive = !is_positive;
+ f = e;
+ }
+ else {
+ break;
+ }
+ }
+ if (!is_positive) {
+ f = m.mk_not(f);
+ }
+
+ }
+
+ bool is_predicate(expr* a) {
+ SASSERT(m.is_bool(a));
+ return is_app(a) && to_app(a)->get_decl()->get_family_id() == null_family_id;
+ }
+
+ void register_predicate(expr* a) {
+ SASSERT(is_predicate(a));
+ m_ctx.register_predicate(to_app(a)->get_decl(), true);
+ }
+
+ enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
+
+ formula_kind get_formula_kind(expr_ref& f) {
+ normalize(f);
+ expr_ref_vector args(m), body(m);
+ expr_ref head(m);
+ expr* a = 0, *a1 = 0;
+ datalog::flatten_or(f, args);
+ for (unsigned i = 0; i < args.size(); ++i) {
+ a = args[i].get();
+ if (m.is_not(a, a1) && is_predicate(a1)) {
+ register_predicate(a1);
+ body.push_back(a1);
+ }
+ else if (is_predicate(a)) {
+ register_predicate(a);
+ if (head) {
+ return IS_NONE;
+ }
+ head = a;
+ }
+ else if (m.is_not(a, a1)) {
+ body.push_back(a1);
+ }
+ else {
+ body.push_back(m.mk_not(a));
+ }
+ }
+ f = m.mk_and(body.size(), body.c_ptr());
+ if (head) {
+ f = m.mk_implies(f, head);
+ return IS_RULE;
+ }
+ else {
+ return IS_QUERY;
+ }
+ }
+
+ expr_ref mk_rule(expr* body, expr* head) {
+ return expr_ref(m.mk_implies(body, head), m);
+ }
+
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
+ SASSERT(g->is_well_sorted());
+ mc = 0; pc = 0; core = 0;
+ tactic_report report("pdr", *g);
+ bool produce_models = g->models_enabled();
+ bool produce_proofs = g->proofs_enabled();
+
+ if (produce_proofs) {
+ if (!m_ctx.get_params().get_bool(":generate-proof-trace", true)) {
+ params_ref params = m_ctx.get_params();
+ params.set_bool(":generate-proof-trace", true);
+ updt_params(params);
+ }
+ }
+
+ unsigned sz = g->size();
+ expr_ref q(m), f(m);
+ expr_ref_vector queries(m);
+ std::stringstream msg;
+
+ for (unsigned i = 0; i < sz; i++) {
+ f = g->form(i);
+ formula_kind k = get_formula_kind(f);
+ switch(k) {
+ case IS_RULE:
+ m_ctx.add_rule(f, symbol::null);
+ break;
+ case IS_QUERY:
+ queries.push_back(f);
+ break;
+ default:
+ msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
+ throw tactic_exception(msg.str().c_str());
+ }
+ }
+
+ if (queries.size() != 1) {
+ q = m.mk_fresh_const("query", m.mk_bool_sort());
+ for (unsigned i = 0; i < queries.size(); ++i) {
+ f = mk_rule(queries[i].get(), q);
+ m_ctx.add_rule(f, symbol::null);
+ }
+ queries.reset();
+ queries.push_back(q);
+ }
+ SASSERT(queries.size() == 1);
+ q = queries[0].get();
+ lbool is_reachable = m_ctx.query(q);
+ g->inc_depth();
+ result.push_back(g.get());
+ switch (is_reachable) {
+ case l_true: {
+ // goal is unsat
+ g->assert_expr(m.mk_false());
+ if (produce_proofs) {
+ proof_ref proof = m_ctx.get_proof();
+ pc = proof2proof_converter(m, proof);
+ }
+ break;
+ }
+ case l_false: {
+ // goal is sat
+ g->reset();
+ if (produce_models) {
+ model_ref md = m_ctx.get_model();
+ mc = model2model_converter(&*md);
+ }
+ break;
+ }
+ case l_undef:
+ // subgoal is unchanged.
+ break;
+ }
+ TRACE("pdr", g->display(tout););
+ SASSERT(g->is_well_sorted());
+ }
+ };
+
+ params_ref m_params;
+ imp * m_imp;
+public:
+ pdr_tactic(ast_manager & m, params_ref const & p):
+ m_params(p) {
+ m_imp = alloc(imp, m, p);
+ }
+
+ virtual tactic * translate(ast_manager & m) {
+ return alloc(pdr_tactic, m, m_params);
+ }
+
+ virtual ~pdr_tactic() {
+ dealloc(m_imp);
+ }
+
+ virtual void updt_params(params_ref const & p) {
+ m_params = p;
+ m_imp->updt_params(p);
+ }
+
+
+ virtual void collect_param_descrs(param_descrs & r) {
+ m_imp->collect_param_descrs(r);
+ }
+
+ virtual void operator()(goal_ref const & in,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
+ (*m_imp)(in, result, mc, pc, core);
+ }
+
+
+ virtual void collect_statistics(statistics & st) const {
+ m_imp->collect_statistics(st);
+ }
+
+ virtual void reset_statistics() {
+ m_imp->reset_statistics();
+ }
+
+
+ virtual void cleanup() {
+ ast_manager & m = m_imp->m;
+ imp * d = m_imp;
+ #pragma omp critical (tactic_cancel)
+ {
+ m_imp = 0;
+ }
+ dealloc(d);
+ d = alloc(imp, m, m_params);
+ #pragma omp critical (tactic_cancel)
+ {
+ m_imp = d;
+ }
+ }
+
+protected:
+ virtual void set_cancel(bool f) {
+ if (m_imp)
+ m_imp->set_cancel(f);
+ }
+};
+
+tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
+ return clean(alloc(pdr_tactic, m, p));
+}
+
diff --git a/src/muz_qe/pdr_tactic.h b/src/muz_qe/pdr_tactic.h
new file mode 100644
index 000000000..5a315152a
--- /dev/null
+++ b/src/muz_qe/pdr_tactic.h
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ pdr_tactic.h
+
+Abstract:
+
+ PDR as a tactic to solve Horn clauses.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2012-11-16.
+
+Revision History:
+
+--*/
+#ifndef _PDR_TACTIC_H_
+#define _PDR_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+ ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)")
+*/
+#endif
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 33298c515..512d94956 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -324,13 +324,12 @@ expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector con
unsigned sz = m_model->get_num_constants();
expr_ref e(m), eq(m);
expr_ref_vector model(m);
- bool_rewriter rw(m);
for (unsigned i = 0; i < sz; i++) {
func_decl * d = m_model->get_constant(i);
expr* val = m_model->get_const_interp(d);
e = m.mk_const(d);
if (m_visited.is_marked(e)) {
- rw.mk_eq(e, val, eq);
+ eq = m.mk_eq(e, val);
model.push_back(eq);
}
}
@@ -466,6 +465,7 @@ void model_evaluator::eval_arith(app* e) {
}
void model_evaluator::inherit_value(expr* e, expr* v) {
+ expr* w;
SASSERT(!is_unknown(v));
SASSERT(m.get_sort(e) == m.get_sort(v));
if (is_x(v)) {
@@ -475,7 +475,10 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
SASSERT(m.is_bool(v));
if (is_true(v)) set_true(e);
else if (is_false(v)) set_false(e);
- else set_x(e);
+ else {
+ TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
+ set_x(e);
+ }
}
else if (m_arith.is_int_real(e)) {
set_number(e, get_number(v));
@@ -483,7 +486,11 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
else if (m.is_value(v)) {
set_value(e, v);
}
+ else if (m_values.find(v, w)) {
+ set_value(e, w);
+ }
else {
+ TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
@@ -642,6 +649,7 @@ void model_evaluator::eval_basic(app* e) {
set_bool(e, e1 == e2);
}
else {
+ TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
set_x(e);
}
}
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index 6143e6746..75c9cbb15 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -223,7 +223,7 @@ public:
found_false = true;
break;
}
- SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+ // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
parents.push_back(tmp);
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
m_units.insert(m.get_fact(tmp), tmp);
@@ -283,7 +283,7 @@ public:
found_false = true;
break;
}
- SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+ // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
change = change || (tmp != m.get_parent(p, i));
args.push_back(tmp);
}
diff --git a/src/ast/normal_forms/elim_term_ite.cpp b/src/smt/elim_term_ite.cpp
similarity index 100%
rename from src/ast/normal_forms/elim_term_ite.cpp
rename to src/smt/elim_term_ite.cpp
diff --git a/src/ast/normal_forms/elim_term_ite.h b/src/smt/elim_term_ite.h
similarity index 100%
rename from src/ast/normal_forms/elim_term_ite.h
rename to src/smt/elim_term_ite.h
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 50d972a0d..eb0534eea 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -33,6 +33,7 @@ Notes:
#include"default_tactic.h"
#include"ufbv_tactic.h"
#include"qffpa_tactic.h"
+#include"pdr_tactic.h"
#include"smt_solver.h"
MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
@@ -54,6 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
+MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p));
static void init(strategic_solver * s) {
s->set_default_tactic(alloc(default_fct));
@@ -77,6 +79,7 @@ static void init(strategic_solver * s) {
s->set_tactic_for(symbol("UFBV"), alloc(ufbv_fct));
s->set_tactic_for(symbol("BV"), alloc(ufbv_fct));
s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct));
+ s->set_tactic_for(symbol("HORN"), alloc(horn_fct));
}
solver * mk_smt_strategic_solver(bool force_tactic) {
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index d13eab75e..30e05bd26 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -549,7 +549,7 @@ public:
#ifdef _NO_OMP_
use_seq = true;
#else
- use_seq = omp_in_parallel();
+ use_seq = 0 != omp_in_parallel();
#endif
if (use_seq) {
// execute tasks sequentially
@@ -677,7 +677,7 @@ public:
#ifdef _NO_OMP_
use_seq = true;
#else
- use_seq = omp_in_parallel();
+ use_seq = 0 != omp_in_parallel();
#endif
if (use_seq) {
// execute tasks sequentially
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index e25e140a5..859672f8d 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -42,11 +42,11 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
qe(m.mk_true(), fml, result);
std::cout << " -> " << mk_pp(result, m) << " " << expected_outcome << "\n";
if (expected_outcome == l_true && !m.is_true(result)) {
- std::cout << "ERROR: expected true, instead got " << ast_pp(result, m).c_str() << "\n";
+ std::cout << "ERROR: expected true, instead got " << mk_pp(result, m) << "\n";
//exit(-1);
}
if (expected_outcome == l_false && !m.is_false(result)) {
- std::cout << "ERROR: expected false, instead got " << ast_pp(result, m).c_str() << "\n";
+ std::cout << "ERROR: expected false, instead got " << mk_pp(result, m) << "\n";
//exit(-1);
}
}
diff --git a/src/util/debug.h b/src/util/debug.h
index ab9fdd57b..64cc35fcf 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -98,6 +98,9 @@ private:
};
void finalize_debug();
+/*
+ ADD_FINALIZER('finalize_debug();')
+*/
#endif /* _DEBUG_H_ */
diff --git a/src/util/mem_stat.cpp b/src/util/mem_stat.cpp
deleted file mode 100644
index c0753dea9..000000000
--- a/src/util/mem_stat.cpp
+++ /dev/null
@@ -1,56 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- mem_stat.cpp
-
-Abstract:
-
- Memory usage statistics
-
-Author:
-
- Leonardo de Moura (leonardo) 2006-11-09.
-
-Revision History:
-
---*/
-
-#ifdef _WINDOWS
-#include
-#include
-#include
-
-double get_max_heap_size() {
- DWORD processID = GetCurrentProcessId();
- HANDLE hProcess;
- PROCESS_MEMORY_COUNTERS pmc;
-
- hProcess = OpenProcess(PROCESS_QUERY_INFORMATION |
- PROCESS_VM_READ,
- FALSE, processID);
- double result = -1.0;
-
- if (NULL == hProcess) {
- return -1.0;
- }
-
- if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
- result = static_cast(pmc.PeakWorkingSetSize) / static_cast(1024*1024);
- }
-
- CloseHandle( hProcess );
-
- return result;
-}
-
-#else
-
-double get_max_heap_size() {
- // not available in this platform
- return -1.0;
-}
-
-#endif
-
diff --git a/src/util/mem_stat.h b/src/util/mem_stat.h
deleted file mode 100644
index 84c7d0096..000000000
--- a/src/util/mem_stat.h
+++ /dev/null
@@ -1,25 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- mem_stat.h
-
-Abstract:
-
- Memory usage statistics
-
-Author:
-
- Leonardo de Moura (leonardo) 2006-11-09.
-
-Revision History:
-
---*/
-#ifndef _MEM_STAT_H_
-#define _MEM_STAT_H_
-
-double get_max_heap_size();
-
-#endif /* _MEM_STAT_H_ */
-
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 3aeb65d3b..b6eb648d9 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -1,13 +1,27 @@
+#include
#include
+#include"trace.h"
#include"memory_manager.h"
-#include"rational.h"
-#include"prime_generator.h"
-#include"debug.h"
+#include"error_codes.h"
+
+// The following two function are automatically generated by the mk_make.py script.
+// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
+// For example, rational.h contains
+// ADD_INITIALIZER('rational::initialize();')
+// ADD_FINALIZER('rational::finalize();')
+// Thus, any executable or shared object (DLL) that depends on rational.h
+// will have an automalically generated file mem_initializer.cpp containing
+// mem_initialize()
+// mem_finalize()
+// and these functions will include the statements:
+// rational::initialize();
+//
+// rational::finalize();
+void mem_initialize();
+void mem_finalize();
// If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
// #define PROFILE_MEMORY
-void initialize_symbols();
-void finalize_symbols();
out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
}
@@ -58,8 +72,7 @@ mem_usage_report g_info;
void memory::initialize(size_t max_size) {
g_memory_out_of_memory = false;
g_memory_max_size = max_size;
- rational::initialize();
- initialize_symbols();
+ mem_initialize();
}
bool memory::is_out_of_memory() {
@@ -96,14 +109,9 @@ static bool g_finalizing = false;
void memory::finalize() {
g_finalizing = true;
- finalize_debug();
- finalize_trace();
- finalize_symbols();
- rational::finalize();
- prime_iterator::finalize();
+ mem_finalize();
}
-
unsigned long long memory::get_allocation_size() {
long long r;
#pragma omp critical (z3_memory_manager)
diff --git a/src/util/prime_generator.h b/src/util/prime_generator.h
index efb675737..d63fdb224 100644
--- a/src/util/prime_generator.h
+++ b/src/util/prime_generator.h
@@ -48,6 +48,9 @@ public:
prime_iterator(prime_generator * g = 0);
uint64 next();
static void finalize();
+ /*
+ ADD_FINALIZER('prime_iterator::finalize();')
+ */
};
#endif
diff --git a/src/util/rational.h b/src/util/rational.h
index 4aa2f5fc6..f0406f30a 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -35,7 +35,10 @@ public:
static void initialize();
static void finalize();
-
+ /*
+ ADD_INITIALIZER('rational::initialize();')
+ ADD_FINALIZER('rational::finalize();')
+ */
rational() {}
rational(rational const & r) { m().set(m_val, r.m_val); }
diff --git a/src/util/symbol.h b/src/util/symbol.h
index e32eeb55b..65325b461 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -141,6 +141,10 @@ struct symbol_eq_proc {
void initialize_symbols();
void finalize_symbols();
+/*
+ ADD_INITIALIZER('initialize_symbols();')
+ ADD_FINALIZER('finalize_symbols();')
+*/
// total order on symbols... I did not overloaded '<' to avoid misunderstandings.
// numerical symbols are smaller than non numerical symbols.
diff --git a/src/util/trace.h b/src/util/trace.h
index 941520f87..0c8c2e5b6 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -40,6 +40,9 @@ bool is_trace_enabled(const char * tag);
void close_trace();
void open_trace();
void finalize_trace();
+/*
+ ADD_FINALIZER('finalize_trace();')
+*/
#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })