diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 7ac026673..2c8d93acd 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -26,6 +26,10 @@ Version 4.3.2
- Fixed crash reported at http://z3.codeplex.com/workitem/10
+- Removed auxiliary constants created by the nnf tactic from Z3 models.
+
+- Fixed problem in the pretty printer. It was not introducing quotes for attribute names such as |foo:10|.
+
Version 4.3.1
=============
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 381f92def..3ffa7e313 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -75,6 +75,8 @@ VER_BUILD=None
VER_REVISION=None
PREFIX='/usr'
GMP=False
+VS_PAR=False
+VS_PAR_NUM=8
def is_windows():
return IS_WINDOWS
@@ -362,6 +364,8 @@ def display_help(exit_code):
if not IS_WINDOWS:
print " -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX
print " -y <dir>, --pydir=<dir> installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR
+ else:
+ print " --parallel=num use cl option /MP with 'num' parallel processes"
print " -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build)."
print " -d, --debug compile Z3 in debug mode."
print " -t, --trace enable tracing in release mode."
@@ -391,13 +395,13 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
- global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
+ global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:dsxhmcvtnp:gjy:',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
- 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir='])
+ 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel='])
except:
print "ERROR: Invalid command line option"
display_help(1)
@@ -429,8 +433,11 @@ def parse_options():
DOTNET_ENABLED = False
elif opt in ('--staticlib'):
STATIC_LIB = True
- elif opt in ('-p', '--prefix'):
+ elif not IS_WINDOWS and opt in ('-p', '--prefix'):
PREFIX = arg
+ elif IS_WINDOWS and opt == '--parallel':
+ VS_PAR = True
+ VS_PAR_NUM = int(arg)
elif opt in ('-y', '--pydir'):
PYTHON_PACKAGE_DIR = arg
mk_dir(PYTHON_PACKAGE_DIR)
@@ -656,8 +663,32 @@ class Component:
out.write(' -I%s' % get_component(dep).to_src_dir)
out.write('\n')
mk_dir(os.path.join(BUILD_DIR, self.build_dir))
- for cppfile in get_cpp_files(self.src_dir):
- self.add_cpp_rules(out, include_defs, cppfile)
+ if VS_PAR and IS_WINDOWS:
+ cppfiles = get_cpp_files(self.src_dir)
+ dependencies = set()
+ for cppfile in cppfiles:
+ dependencies.add(os.path.join(self.to_src_dir, cppfile))
+ self.add_rule_for_each_include(out, cppfile)
+ includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
+ for include in includes:
+ owner = self.find_file(include, cppfile)
+ dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
+ for cppfile in cppfiles:
+ out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
+ out.write(': ')
+ for dep in dependencies:
+ out.write(dep)
+ out.write(' ')
+ out.write('\n')
+ out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
+ for cppfile in cppfiles:
+ out.write(' ')
+ out.write(os.path.join(self.to_src_dir, cppfile))
+ out.write('\n')
+ out.write('\tmove *.obj %s\n' % self.build_dir)
+ else:
+ for cppfile in get_cpp_files(self.src_dir):
+ self.add_cpp_rules(out, include_defs, cppfile)
# Return true if the component should be included in the all: rule
def main_component(self):
@@ -933,10 +964,8 @@ class DLLComponent(Component):
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
'%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
- if self.static:
- mk_dir(os.path.join(dist_path, 'bin'))
- shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
- '%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
+ shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
+ '%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@@ -1042,6 +1071,11 @@ class JavaDLLComponent(Component):
def main_component(self):
return is_java_enabled()
+ def mk_win_dist(self, build_path, dist_path):
+ if JAVA_ENABLED:
+ mk_dir(os.path.join(dist_path, 'bin'))
+ shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
+ '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
class ExampleComponent(Component):
def __init__(self, name, path):
@@ -1250,12 +1284,12 @@ def mk_config():
'SLINK_FLAGS=/nologo /LDd\n')
if not VS_X64:
config.write(
- 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
+ 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else:
config.write(
- 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
+ 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else:
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 57ae66b03..dd50a3977 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -16,13 +16,15 @@ import subprocess
import zipfile
from mk_exception import *
from mk_project import *
+import mk_util
BUILD_DIR='build-dist'
-BUILD_X64_DIR='build-dist/x64'
-BUILD_X86_DIR='build-dist/x86'
+BUILD_X64_DIR=os.path.join('build-dist', 'x64')
+BUILD_X86_DIR=os.path.join('build-dist', 'x86')
VERBOSE=True
DIST_DIR='dist'
FORCE_MK=False
+JAVA_ENABLED=True
def set_verbose(flag):
global VERBOSE
@@ -38,8 +40,8 @@ def mk_dir(d):
def set_build_dir(path):
global BUILD_DIR
BUILD_DIR = path
- BUILD_X86_DIR = '%s/x86' % path
- BUILD_X64_DIR = '%s/x64' % path
+ BUILD_X86_DIR = os.path.join(path, 'x86')
+ BUILD_X64_DIR = os.path.join(path, 'x64')
mk_dir(BUILD_X86_DIR)
mk_dir(BUILD_X64_DIR)
@@ -52,16 +54,18 @@ def display_help():
print " -s, --silent do not print verbose messages."
print " -b <sudir>, --build=<subdir> subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
print " -f, --force force script to regenerate Makefiles."
+ print " --nojava do not include Java bindings in the binary distribution files."
exit(0)
# Parse configuration option for mk_make script
def parse_options():
- global FORCE_MK
+ global FORCE_MK, JAVA_ENABLED
path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help',
'silent',
- 'force'
+ 'force',
+ 'nojava'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@@ -74,18 +78,22 @@ def parse_options():
display_help()
elif opt in ('-f', '--force'):
FORCE_MK = True
+ elif opt == '--nojava':
+ JAVA_ENABLED = False
else:
raise MKException("Invalid command line option '%s'" % opt)
set_build_dir(path)
# Check whether build directory already exists or not
def check_build_dir(path):
- return os.path.exists(path) and os.path.exists('%s/Makefile' % path)
+ return os.path.exists(path) and os.path.exists(os.path.join(path, 'Makefile'))
# Create a build directory using mk_make.py
def mk_build_dir(path, x64):
if not check_build_dir(path) or FORCE_MK:
- opts = ["python", "scripts/mk_make.py", "-b", path]
+ opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path]
+ if JAVA_ENABLED:
+ opts.append('--java')
if x64:
opts.append('-x')
if subprocess.call(opts) != 0:
@@ -147,8 +155,12 @@ def mk_dist_dir_core(x64):
else:
platform = "x86"
build_path = BUILD_X86_DIR
- dist_path = '%s/z3-%s.%s.%s-%s' % (DIST_DIR, major, minor, build, platform)
+ dist_path = os.path.join(DIST_DIR, 'z3-%s.%s.%s-%s' % (major, minor, build, platform))
mk_dir(dist_path)
+ if JAVA_ENABLED:
+ # HACK: Propagate JAVA_ENABLED flag to mk_util
+ # TODO: fix this hack
+ mk_util.JAVA_ENABLED = JAVA_ENABLED
mk_win_dist(build_path, dist_path)
if is_verbose():
print "Generated %s distribution folder at '%s'" % (platform, dist_path)
@@ -225,7 +237,7 @@ def cp_vs_runtime_core(x64):
path = '%sredist\\%s' % (vcdir, platform)
VS_RUNTIME_FILES = []
os.path.walk(path, cp_vs_runtime_visitor, '*.dll')
- bin_dist_path = '%s/%s/bin' % (DIST_DIR, get_dist_path(x64))
+ bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin')
for f in VS_RUNTIME_FILES:
shutil.copy(f, bin_dist_path)
if is_verbose():
@@ -236,8 +248,8 @@ def cp_vs_runtime():
cp_vs_runtime_core(False)
def cp_license():
- shutil.copy("LICENSE.txt", "%s/%s" % (DIST_DIR, get_dist_path(True)))
- shutil.copy("LICENSE.txt", "%s/%s" % (DIST_DIR, get_dist_path(False)))
+ shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(True)))
+ shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(False)))
# Entry point
def main():
diff --git a/scripts/trackall.sh b/scripts/trackall.sh
new file mode 100755
index 000000000..d8351af24
--- /dev/null
+++ b/scripts/trackall.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# Script for "cloning" (and tracking) all branches at codeplex.
+# On Windows, this script must be executed in the "git Bash" console.
+for branch in `git branch -a | grep remotes | grep -v HEAD | grep -v master`; do
+ git branch --track ${branch##*/} $branch
+done
+git fetch --all
+git pull --all
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index afe301ddf..1ad2b8222 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -501,7 +501,12 @@ class smt2_printer {
}
format * pp_simple_attribute(char const * attr, symbol const & s) {
- return mk_compose(m(), mk_string(m(), attr), mk_string(m(), s.str().c_str()));
+ std::string str;
+ if (is_smt2_quoted_symbol(s))
+ str = mk_smt2_quoted_symbol(s);
+ else
+ str = s.str();
+ return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
}
format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) {
@@ -851,7 +856,7 @@ class smt2_printer {
buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
}
if (q->get_skid() != symbol::null) {
- buf.push_back(pp_simple_attribute(":skid ", q->get_skid()));
+ buf.push_back(pp_simple_attribute(":skolemid ", q->get_skid()));
}
if (q->get_qid() != symbol::null) {
#if 0
diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index dab0ca0d8..16e9098fc 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -17,11 +17,67 @@ Revision History:
--*/
#include"defined_names.h"
+#include"obj_hashtable.h"
#include"used_vars.h"
#include"var_subst.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
+struct defined_names::impl {
+ typedef obj_map<expr, app *> expr2name;
+ typedef obj_map<expr, proof *> expr2proof;
+ ast_manager & m_manager;
+ symbol m_z3name;
+
+ /**
+ \brief Mapping from expressions to their names. A name is an application.
+ If the expression does not have free variables, then the name is just a constant.
+ */
+ expr2name m_expr2name;
+ /**
+ \brief Mapping from expressions to the apply-def proof.
+ That is, for each expression e, m_expr2proof[e] is the
+ proof e and m_expr2name[2] are observ. equivalent.
+
+ This mapping is not used if proof production is disabled.
+ */
+ expr2proof m_expr2proof;
+
+ /**
+ \brief Domain of m_expr2name. It is used to keep the expressions
+ alive and for backtracking
+ */
+ expr_ref_vector m_exprs;
+ expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
+ proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
+
+
+ unsigned_vector m_lims; //!< Backtracking support.
+
+ impl(ast_manager & m, char const * prefix);
+ virtual ~impl();
+
+ app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
+ void cache_new_name(expr * e, app * name);
+ void cache_new_name_intro_proof(expr * e, proof * pr);
+ void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
+ void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
+ virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
+ bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
+ void push_scope();
+ void pop_scope(unsigned num_scopes);
+ void reset();
+
+ unsigned get_num_names() const { return m_names.size(); }
+ func_decl * get_name_decl(unsigned i) const { return to_app(m_names.get(i))->get_decl(); }
+};
+
+struct defined_names::pos_impl : public defined_names::impl {
+ pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
+ virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
+};
+
+
defined_names::impl::impl(ast_manager & m, char const * prefix):
m_manager(m),
m_exprs(m),
@@ -222,5 +278,50 @@ void defined_names::impl::reset() {
m_lims.reset();
}
+defined_names::defined_names(ast_manager & m, char const * fresh_prefix) {
+ m_impl = alloc(impl, m, fresh_prefix);
+ m_pos_impl = alloc(pos_impl, m, fresh_prefix);
+}
+
+defined_names::~defined_names() {
+ dealloc(m_impl);
+ dealloc(m_pos_impl);
+}
+
+bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
+ return m_impl->mk_name(e, new_def, new_def_pr, n, pr);
+}
+
+bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
+ return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr);
+}
+
+void defined_names::push() {
+ m_impl->push_scope();
+ m_pos_impl->push_scope();
+}
+
+void defined_names::pop(unsigned num_scopes) {
+ m_impl->pop_scope(num_scopes);
+ m_pos_impl->pop_scope(num_scopes);
+}
+
+void defined_names::reset() {
+ m_impl->reset();
+ m_pos_impl->reset();
+}
+
+unsigned defined_names::get_num_names() const {
+ return m_impl->get_num_names() + m_pos_impl->get_num_names();
+}
+
+func_decl * defined_names::get_name_decl(unsigned i) const {
+ SASSERT(i < get_num_names());
+ unsigned n1 = m_impl->get_num_names();
+ return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);
+}
+
+
+
diff --git a/src/ast/normal_forms/defined_names.h b/src/ast/normal_forms/defined_names.h
index c5e4a116f..0b9f04569 100644
--- a/src/ast/normal_forms/defined_names.h
+++ b/src/ast/normal_forms/defined_names.h
@@ -21,7 +21,6 @@ Revision History:
#define _DEFINED_NAMES_H_
#include"ast.h"
-#include"obj_hashtable.h"
/**
\brief Mapping from expressions to skolem functions that are used to name them.
@@ -29,62 +28,13 @@ Revision History:
The mapping supports backtracking using the methods #push_scope and #pop_scope.
*/
class defined_names {
-
- struct impl {
- typedef obj_map<expr, app *> expr2name;
- typedef obj_map<expr, proof *> expr2proof;
- ast_manager & m_manager;
- symbol m_z3name;
-
- /**
- \brief Mapping from expressions to their names. A name is an application.
- If the expression does not have free variables, then the name is just a constant.
- */
- expr2name m_expr2name;
- /**
- \brief Mapping from expressions to the apply-def proof.
- That is, for each expression e, m_expr2proof[e] is the
- proof e and m_expr2name[2] are observ. equivalent.
-
- This mapping is not used if proof production is disabled.
- */
- expr2proof m_expr2proof;
-
- /**
- \brief Domain of m_expr2name. It is used to keep the expressions
- alive and for backtracking
- */
- expr_ref_vector m_exprs;
- expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
- proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
-
-
- unsigned_vector m_lims; //!< Backtracking support.
-
- impl(ast_manager & m, char const * prefix);
- virtual ~impl();
-
- app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
- void cache_new_name(expr * e, app * name);
- void cache_new_name_intro_proof(expr * e, proof * pr);
- void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
- void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
- virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
- bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
- void push_scope();
- void pop_scope(unsigned num_scopes);
- void reset();
- };
-
- struct pos_impl : public impl {
- pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
- virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
- };
-
- impl m_impl;
- pos_impl m_pos_impl;
+ struct impl;
+ struct pos_impl;
+ impl * m_impl;
+ pos_impl * m_pos_impl;
public:
- defined_names(ast_manager & m, char const * fresh_prefix = "z3name"):m_impl(m, fresh_prefix), m_pos_impl(m, fresh_prefix) {}
+ defined_names(ast_manager & m, char const * fresh_prefix = "z3name");
+ ~defined_names();
// -----------------------------------
//
@@ -113,9 +63,7 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
- bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
- return m_impl.mk_name(e, new_def, new_def_pr, n, pr);
- }
+ bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
/**
\brief Create a name for a positive occurrence of the expression \c e.
@@ -127,24 +75,14 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
- bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
- return m_pos_impl.mk_name(e, new_def, new_def_pr, n, pr);
- }
+ bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
- void push_scope() {
- m_impl.push_scope();
- m_pos_impl.push_scope();
- }
+ void push();
+ void pop(unsigned num_scopes);
+ void reset();
- void pop_scope(unsigned num_scopes) {
- m_impl.pop_scope(num_scopes);
- m_pos_impl.pop_scope(num_scopes);
- }
-
- void reset() {
- m_impl.reset();
- m_pos_impl.reset();
- }
+ unsigned get_num_names() const;
+ func_decl * get_name_decl(unsigned i) const;
};
#endif /* _DEFINED_NAMES_H_ */
diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.cpp b/src/muz_qe/dl_mk_extract_quantifiers2.cpp
index 33b33f0aa..cd13bb44b 100644
--- a/src/muz_qe/dl_mk_extract_quantifiers2.cpp
+++ b/src/muz_qe/dl_mk_extract_quantifiers2.cpp
@@ -333,7 +333,7 @@ namespace datalog {
smt::quantifier_manager* qm = ctx.get_quantifier_manager();
qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
#endif
- lbool res = solver.check();
+ solver.check();
for (unsigned i = 0; i < m_bindings.size(); ++i) {
expr_ref_vector& binding = m_bindings[i];
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index ca58b15af..460e07f58 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -981,6 +981,14 @@ namespace nlsat {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
+ if (!info.m_lc_const) {
+ // We have essentially shown the current factor must be zero If the leading coefficient is not zero.
+ // Note that, if the current factor is zero, then the whole polynomial is zero.
+ // The atom is true if it is an equality, and false otherwise.
+ // The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
+ // However, we have to store the fact it is not zero.
+ info.add_lc_diseq();
+ }
return;
}
else if (s == -1 && !is_even) {
@@ -1341,3 +1349,32 @@ namespace nlsat {
}
};
+
+#ifdef Z3DEBUG
+void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
+ ex.display(std::cout, num, ls);
+}
+void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
+ ex.display(std::cout, ls);
+}
+void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
+ ex.display(std::cout, p);
+ std::cout << std::endl;
+}
+void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
+ polynomial_ref _p(p, ex.m_pm);
+ ex.display(std::cout, _p);
+ std::cout << std::endl;
+}
+void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
+ ex.display(std::cout, ps);
+}
+void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
+ ex.display(std::cout, x);
+ std::cout << std::endl;
+}
+void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
+ ex.display(std::cout, l);
+ std::cout << std::endl;
+}
+#endif
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index 08f6201be..5ecb9d385 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -27,7 +27,9 @@ namespace nlsat {
class evaluator;
class explain {
+ public:
struct imp;
+ private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 6da2c15f5..5552050db 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -189,7 +189,7 @@ void asserted_formulas::push_scope() {
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead);
s.m_inconsistent_old = m_inconsistent;
- m_defined_names.push_scope();
+ m_defined_names.push();
m_bv_sharing.push_scope();
commit();
}
@@ -201,7 +201,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
m_inconsistent = s.m_inconsistent_old;
- m_defined_names.pop_scope(num_scopes);
+ m_defined_names.pop(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h
index b0a21e75b..0cd817f22 100644
--- a/src/smt/params/qi_params.h
+++ b/src/smt/params/qi_params.h
@@ -52,8 +52,6 @@ struct qi_params {
bool m_mbqi_trace;
unsigned m_mbqi_force_template;
- bool m_instgen;
-
qi_params(params_ref const & p = params_ref()):
/*
The "weight 0" performance bug
@@ -99,8 +97,7 @@ struct qi_params {
m_mbqi_max_cexs_incr(1),
m_mbqi_max_iterations(1000),
m_mbqi_trace(false),
- m_mbqi_force_template(10),
- m_instgen(false) {
+ m_mbqi_force_template(10) {
updt_params(p);
}
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index e62a3de21..519302c19 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -18,6 +18,7 @@ Revision History:
--*/
#include"smt_params.h"
#include"smt_params_helper.hpp"
+#include"model_params.hpp"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
@@ -33,6 +34,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
m_soft_timeout = p.soft_timeout();
+ model_params mp(_p);
+ m_model_compact = mp.compact();
if (_p.get_bool("arith.greatest_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (_p.get_bool("arith.least_error_pivot", false))
@@ -50,5 +53,4 @@ void smt_params::updt_params(params_ref const & p) {
void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
m_model = p.m_model;
- m_model_validate = p.m_model_validate;
}
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 3d823cb51..256c5a646 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -177,7 +177,6 @@ struct smt_params : public preprocessor_params,
// -----------------------------------
bool m_model;
bool m_model_compact;
- bool m_model_validate;
bool m_model_on_timeout;
bool m_model_on_final_check;
@@ -264,7 +263,6 @@ struct smt_params : public preprocessor_params,
m_abort_after_preproc(false),
m_model(true),
m_model_compact(false),
- m_model_validate(false),
m_model_on_timeout(false),
m_model_on_final_check(false),
m_progress_sampling_freq(0),
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index b3f16a3ce..42e761b61 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -23,7 +23,6 @@ Revision History:
#include"ast_smt2_pp.h"
#include"smt_model_finder.h"
#include"for_each_expr.h"
-#include"theory_instgen.h"
namespace smt {
@@ -530,11 +529,6 @@ namespace smt {
SASSERT(!b_internalized(q));
SASSERT(q->is_forall());
SASSERT(check_patterns(q));
- if (m_fparams.m_instgen) {
- theory* th = m_theories.get_plugin(m_manager.get_family_id("inst_gen"));
- static_cast<theory_instgen*>(th)->internalize_quantifier(q);
- return;
- }
bool_var v = mk_bool_var(q);
unsigned generation = m_generation;
unsigned _generation;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index ac31eb1a9..f0dc1f5a6 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -28,7 +28,6 @@ Revision History:
#include"theory_datatype.h"
#include"theory_dummy.h"
#include"theory_dl.h"
-#include"theory_instgen.h"
#include"theory_seq_empty.h"
namespace smt {
@@ -772,11 +771,6 @@ namespace smt {
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
}
- void setup::setup_instgen() {
- if (m_params.m_instgen) {
- m_context.register_plugin(mk_theory_instgen(m_manager, m_params));
- }
- }
void setup::setup_unknown() {
setup_arith();
@@ -784,7 +778,6 @@ namespace smt {
setup_bv();
setup_datatypes();
setup_dl();
- setup_instgen();
setup_seq();
}
diff --git a/src/smt/theory_instgen.cpp b/src/smt/theory_instgen.cpp
deleted file mode 100644
index 68e04aab0..000000000
--- a/src/smt/theory_instgen.cpp
+++ /dev/null
@@ -1,1494 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- theory_instgen.cpp
-
-Abstract:
-
- iProver style theory solver.
- It provides an instantiation based engine
- based on InstGen methods together with
- unit propagation.
-
-Author:
-
- Krystof Hoder (t-khoder)
- Nikolaj Bjorner (nbjorner) 2011-10-6
-
-Revision History:
-
-Main data-structures:
-
-- Instantiation = Var -> Expr
-- MatchingSet = Instantiation-set
- operations:
- - has_instance : Instantiation -> Bool
- has_instance(i) = exists j in MatchingSet . j <= i
-- UnificationIndex
- operations:
- - insert : Expr
- - remove : Expr
- - unify : Expr -> Expr-set
- - set of inserted expressions that unify
-- RootClauseMap : Expr -> Quantifier
- where RootClauseMap(clause) = The quantifier that originated clause
-- Occurs : Expr -> Quantifier-set
- the set of quantifiers where non-ground literal occurs.
-- LiteralMeanings : Literal -> Expr-set
- - set of non-ground literals that were grounded to Literal
-- InternalizedFoLits : Expr-set
- - forall e in InternalizedFoLits . e \in LiteralMeanings(ground(e))
-- MatchingSets : Quantifier -> MatchingSet
-
-
-Main operation:
-
- - insert all assigned literals into UnificationIndex
- - for l' in LiteralMeanings(l) do:
- for m',theta in UnificationIndex.unify(not l') do:
- for q in Occurs(l') do:
- for q' in Occurs(m') do:
- instantiate q with theta
- instantiate q' with theta
-
- instantiate q with theta:
-
-Discussion of plans:
-
-- Efficient unit propagation using the tables from dl_
- See addittional notes under unit propagation.
- The idea is to perfrm unit propagation using the tables
- provided in the dl_ module. This is similar to unit
- propagation from the EPR solver and retains succinctness
- features, but does not carry over the splitting component.
- The efficient propagator is aimed at solving ground problems more efficiently,
- for example
-
-- Reduce set of selected literals when clause already has on selected literal.
-
-- Subsumption module:
- - simplify clause using already asserted clauses.
- - check for variants.
-
-- Completeness for EPR with equality:
- The relevant equality clause for EPR are C \/ x = y and C \/ a = x
- Destructive E-resolution (DER) removes disequalities.
- Two approaches:
- 1. Rely on super-position/hyper-resolution of ordinary literals
- in the clause.
- 2. Instantiate based on congruence closure.
- The instantiation based approach takes a clause of the form C \/ x = y,
- where all other non-equality literals in C are assigned false by the
- current assignment, and (the grounded version U = U' of) x = y is
- assigned true. Take the equivalence classes of the type of x and
- instantiate x, y using representatives for different equivalence
- classes. The number of instantiations is potentially quadratic
- in the number of terms. One reduction considers symmetries:
- instantiate x by a smaller representative than y.
-- Unit propagation:
- - Why should unit-propagation matter: hunch: similar role as
- theory propagation where conflicts are created close to root
- of search tree.
- - Add theory identifiers to literals so that assign_eh is invoked.
- - Produce explanation objects for unit propagation.
- - Unit propagation index.
- - Idea only propagate known literals
-- Exchange unit literals with super position engine for equalities.
- iProver approach: perform unit super-position proof, get instances
- by labeling equalities by clauses + substitution (set-labeling)
- portfolio approach: exchange unit literals to super-position
- (or hypotheses as suggested in more general setting).
-
---*/
-
-#include "theory_instgen.h"
-#include "value_factory.h"
-#include "smt_model_generator.h"
-#include "smt_context.h"
-#include "ast_smt2_pp.h"
-#include "substitution.h"
-#include "substitution_tree.h"
-#include "uint_set.h"
-#include "unifier.h"
-#include "matcher.h"
-#include "rewriter.h"
-#include "rewriter_def.h"
-#include "var_subst.h"
-
-#define PP mk_pp
-
-namespace smt {
-
-
- //
- // expression grounding for passing to the SMT solver
- //
- class grounder {
- ast_manager& m;
- vector<obj_map<sort,expr*> > m_defaults;
- expr_ref_vector m_ref_holder;
-
- class grounding_rewriter_cfg;
-
- void reserve(unsigned idx) {
- if (m_defaults.size() <= idx) {
- m_defaults.resize(idx+1);
- }
- }
-
- expr* mk_default(sort* s) {
- return mk_default(0, s);
- }
-
- expr* mk_default(unsigned i, sort* s) {
- expr* d;
- reserve(i);
- if (!m_defaults[i].find(s, d)) {
- d = m.mk_fresh_const("U",s);
- m_defaults[i].insert(s, d);
- m_ref_holder.push_back(d);
- }
- return d;
- }
-
- class grounding_rewriter_cfg : public default_rewriter_cfg {
- grounder& m_parent;
- bool m_collapse;
- public:
- grounding_rewriter_cfg(grounder& parent, bool collapse)
- : m_parent(parent), m_collapse(collapse) {}
-
- bool get_subst(expr * s, expr * & t, proof * & t_pr) {
- SASSERT(is_app(s) || is_var(s));
- if (is_var(s)) {
- var* v = to_var(s);
- if (m_collapse) {
- t = m_parent.mk_default(v->get_sort());
- }
- else {
- t = m_parent.mk_default(v->get_idx(), v->get_sort());
- }
- }
- return is_var(s);
- }
- };
-
- void mk(expr * e, app_ref& res, bool collapse) {
- if(is_ground(e)) {
- res = to_app(e);
- }
- else {
- while (is_quantifier(e)) {
- e = to_quantifier(e)->get_expr();
- }
- SASSERT(is_app(e));
- grounding_rewriter_cfg r_cfg(*this, collapse);
- rewriter_tpl<grounding_rewriter_cfg> rwr(m, false, r_cfg);
- expr_ref res_e(m);
- rwr(e, res_e);
- res = to_app(res_e);
- }
- SASSERT(is_ground(res.get()));
- }
-
- public:
- grounder(ast_manager& m): m(m), m_ref_holder(m) {
- reserve(0);
- }
-
- /**
- create a grounding that recycles the same constant for
- different variables of the same sort.
-
- This function can be called either with whole clauses (incl. quantifier),
- or with literals one by one (without a quantifier)
- */
- void operator()(expr * e, app_ref& res) {
- mk(e, res, true);
- }
-
- //
- // create a grounding where different variables have different names
- //
- void mk_diff(expr * e, app_ref& res) {
- mk(e, res, false);
- }
- };
-
- //
- // Class for first-order subsumption checking.
- // if clause[renaming] is a superset of existing clause in context, then clause is subsumed.
- // if context => clause then clause is subsumed.
- // if context & clause => ~ lit then lit is subsumed from clause
- //
- // TBD:
- // - check unit propagation
- // - use internalizer functions directly. The assertions have already been pre-processed.
- //
- class clause_subsumption {
- ast_manager& m;
- grounder m_grounder;
- smt_params m_params;
- context m_ctx;
- quantifier_ref_vector m_assumptions;
- unsigned_vector m_limit;
- public:
- clause_subsumption(ast_manager& m, smt_params& p):
- m(m), m_grounder(m), m_params(p), m_ctx(m,m_params), m_assumptions(m) {
- m_params.m_instgen = false;
- }
-
- void simplify(quantifier* new_clause, expr_ref& result, ptr_vector<quantifier>& assumptions) {
-#if 1
- result = new_clause;
- return;
-#endif
-
- SASSERT(new_clause->is_forall());
- expr* body = new_clause->get_expr();
- app_ref ground_clause(m);
- m_grounder.mk_diff(new_clause, ground_clause);
- if (is_subsumed(ground_clause)) {
- TRACE("theory_instgen", tout << "subsumed: " << PP(new_clause,m) << "\n";);
- result = m.mk_true();
- return;
- }
- if (is_homomorphic_image(body)) {
- result = m.mk_true();
- return;
- }
- // Assert the current clause.
- m_ctx.internalize(ground_clause, true);
- m_ctx.assign(m_ctx.get_literal(ground_clause), b_justification());
- TRACE("theory_instgen", tout << "Asserting: " << PP(ground_clause,m) << "\n";);
- m_assumptions.push_back(new_clause);
- SASSERT(m.is_or(body) == m.is_or(ground_clause));
- if (!m.is_or(body)) {
- result = new_clause;
- return;
- }
- SASSERT(to_app(body)->get_num_args() == ground_clause->get_num_args());
- ptr_vector<expr> lits;
- for (unsigned i = 0; i < to_app(body)->get_num_args(); ++i) {
- m_ctx.push();
- m_ctx.assign(m_ctx.get_literal(ground_clause->get_arg(i)), b_justification());
- lbool is_sat = m_ctx.check();
- m_ctx.pop(1);
- if (is_sat != l_false) {
- lits.push_back(to_app(body)->get_arg(i));
- }
- else {
- TRACE("theory_instgen", tout << "subsumed literal: " << PP(to_app(body)->get_arg(i),m) << "\n";);
- }
- }
- if (lits.size() == ground_clause->get_num_args()) {
- result = new_clause;
- }
- else {
- SASSERT(!lits.empty());
- result = lits.size()==1?lits[0]:m.mk_or(lits.size(), lits.c_ptr());
- result = m.update_quantifier(new_clause, result);
- TRACE("theory_instgen", tout << "simplified: " << PP(new_clause,m) << "\n";
- tout << PP(result.get(), m) << "\n";
- );
- //overapproximation of required assumptions
- //( m_assumptions.size()-1 ... the -1 is not to make ourselves as an assumption)
- assumptions.append(m_assumptions.size()-1, m_assumptions.c_ptr());
- }
- }
-
- void push() {
- m_ctx.push();
- m_limit.push_back(m_assumptions.size());
- }
-
- void pop(unsigned num_scopes) {
- m_ctx.pop(num_scopes);
-
- unsigned last_idx = m_limit.size()-num_scopes;
- unsigned restored_assumptions_size = m_limit[last_idx];
- m_limit.resize(last_idx);
- m_assumptions.resize(restored_assumptions_size);
- }
-
- private:
-
- bool is_subsumed(expr* ground_clause) {
- m_ctx.push();
- m_ctx.internalize(ground_clause, true);
- m_ctx.assign(~m_ctx.get_literal(ground_clause), b_justification());
- lbool is_sat = m_ctx.check();
- m_ctx.pop(1);
- TRACE("theory_instgen",
- tout << PP(ground_clause, m) << " " <<
- ((is_sat==l_false)?"unsat":"sat") << "\n";);
- return (is_sat == l_false);
- }
-
- bool is_homomorphic_image(expr* body) {
- // TBD
- return false;
- }
-
- };
-
- class fo_clause_internalizer;
- class instantiator;
- class theory_instgen_impl;
- typedef expr_ref_vector inst;
-
- class instantiation_result {
- quantifier_ref m_clause;
- inst m_subst;
- public:
- instantiation_result(ast_manager& m) : m_clause(m), m_subst(m) {}
-
- void init(quantifier * q, const inst& subst) {
- SASSERT(!m_clause); //we init each object at most once
- SASSERT(m_subst.empty());
- SASSERT(q);
- m_clause = q;
- m_subst.append(subst);
- }
- quantifier * clause() const { return m_clause; }
- const inst& subst() const { return m_subst; }
- };
-
- typedef vector<instantiation_result> instantiation_result_vector;
-
- // TBD: replace this by the substitution tree index.
- // It should do the trick of identifying instances and generalizers.
- // see matching_set2..
- //
- class matching_set {
- ast_manager& m;
- vector<inst> m_inst;
-
- //used in the has_instance function
- mutable substitution m_subst;
-
- public:
- matching_set(ast_manager& m) : m(m), m_subst(m) {}
- unsigned size() const { return m_inst.size(); }
- inst const& operator[](unsigned i) const { return m_inst[i]; }
-
- void insert(inst const& inst) {
- SASSERT(m_inst.empty() || m_inst.back().size() == inst.size());
- TRACE("theory_instgen_verbose",
- for (unsigned i = 0; i < inst.size(); ++i) {
- tout << PP(inst[i], m) << " ";
- }
- tout << "\n";
- );
- m_inst.push_back(inst);
- }
- void insert(unsigned sz, expr* const* exprs) {
- insert(inst(m, sz, exprs));
- }
- void pop_insert() { m_inst.pop_back(); }
-
- bool has_instance(inst const& inst) {
- unsigned dont_care;
- return has_instance(inst, dont_care);
- }
-
- bool has_instance(inst const& new_inst, unsigned& index) {
- for (unsigned i = 0; i < size(); ++i) {
- if (has_instance(new_inst, m_inst[i])) {
- index = i;
- return true;
- }
- }
- return false;
- }
-
- class insert_inst : public trail<smt::context> {
- matching_set& m_ms;
- public:
- insert_inst(matching_set& m): m_ms(m) {}
- virtual void undo(smt::context& ctx) { m_ms.pop_insert(); }
- };
-
- static bool is_identity(const inst& subst) {
- uint_set vars;
- vars.reset();
- unsigned sz = subst.size();
- for(unsigned i=0; i<sz; i++) {
- expr * val = subst[i];
- if(!is_var(val)) { return false; }
- unsigned var_idx = to_var(val)->get_idx();
- if(vars.contains(var_idx)) {
- return false;
- }
- vars.insert(var_idx);
- }
- return true;
- }
-
- private:
- // check if old_instance is an instance of new_instance.
- bool has_instance(inst const& new_instance, inst const& old_instance) const {
- SASSERT(new_instance.size() == old_instance.size());
- unsigned sz = new_instance.size();
- m_subst.reset();
- m_subst.reserve_vars(sz);
- m_subst.reserve_offsets(2);
- matcher mtchr(m);
- for(unsigned i = 0; i < sz; i++) {
- TRACE("theory_instgen_verbose", tout << PP(new_instance[i], m) << " " << PP(old_instance[i], m) << "\n";);
- if(!mtchr(new_instance[i], old_instance[i], m_subst)) {
- return false;
- }
- }
- return true;
- }
- };
-
-
- class matching_set2 {
- class inst_visitor : public st_visitor {
- bool m_found;
- public:
- inst_visitor(substitution& s): st_visitor(s), m_found(false) {}
- virtual bool operator()(expr * e) {
- m_found = true;
- return false;
- }
- void reset() { m_found = false; }
- bool found() const { return m_found; }
- };
-
- ast_manager& m;
- substitution_tree m_st;
- func_decl_ref m_f;
- app_ref_vector m_trail;
- substitution m_dummy;
- inst_visitor m_visitor;
-
- public:
- matching_set2(ast_manager& m) : m(m), m_st(m), m_f(m), m_trail(m), m_dummy(m), m_visitor(m_dummy) {}
-
- void insert(inst const& inst) {
- if (!m_f.get()) {
- ptr_buffer<sort> domain;
- for (unsigned i = 0; i < inst.size(); ++i) {
- domain.push_back(m.get_sort(inst[i]));
- }
- m_f = m.mk_func_decl(symbol("tuple"),inst.size(), domain.c_ptr(), m.mk_bool_sort());
- m_trail.push_back(m.mk_app(m_f, inst.size(), inst.c_ptr()));
- m_st.insert(m_trail.back());
- }
- }
- void insert(unsigned sz, expr* const* exprs) {
- insert(inst(m, sz, exprs));
- }
- void pop_insert() {
- m_st.erase(m_trail.back());
- m_trail.pop_back();
- }
-
- bool has_instance(inst const& inst) {
- app_ref f(m);
- f = m.mk_app(m_f, inst.size(), inst.c_ptr());
- m_visitor.reset();
- m_st.inst(f, m_visitor);
- return m_visitor.found();
- }
-
- class insert_inst : public trail<smt::context> {
- matching_set& m_ms;
- public:
- insert_inst(matching_set& m): m_ms(m) {}
- virtual void undo(smt::context& ctx) { m_ms.pop_insert(); }
- };
-
- static bool is_identity(const inst& subst) {
- uint_set vars;
- vars.reset();
- unsigned sz = subst.size();
- for(unsigned i=0; i<sz; i++) {
- expr * val = subst[i];
- if(!is_var(val)) { return false; }
- unsigned var_idx = to_var(val)->get_idx();
- if(vars.contains(var_idx)) {
- return false;
- }
- vars.insert(var_idx);
- }
- return true;
- }
- };
-
-
- /////////////////////////
- // inst_gen_unif_index
- //
-
- class inst_gen_unif_index {
- ast_manager & m;
- substitution_tree m_st;
- unsigned m_num_vars;
- app_ref_vector m_ref_holder;
- unsigned_vector m_lim;
-
- class collecting_visitor : public st_visitor {
- app_ref_vector& m_acc;
- public:
- collecting_visitor(app_ref_vector& acc, substitution& subst)
- : st_visitor(subst), m_acc(acc) {}
- virtual bool operator()(expr * e) {
- SASSERT(is_app(e));
- m_acc.push_back(to_app(e));
- return true;
- }
- };
-
-
- class st_contains_visitor : public st_visitor {
- expr* m_e;
- bool m_found;
- public:
- st_contains_visitor(substitution& s, expr* e): st_visitor(s), m_e(e), m_found(false) {}
- virtual bool operator()(expr* e) {
- if (e == m_e) {
- m_found = true;
- return false;
- }
- return true;
- }
- bool found() const { return m_found; }
- };
-
- void debug_st(char const* cmd, app* l) {
- expr_ref e(m);
- ptr_vector<sort> sorts;
- svector<symbol> names;
- get_free_vars(l, 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();
- if (!sorts.empty()) {
- e = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), l);
- }
- else {
- e = l;
- }
- std::cout << ":" << cmd << " " << PP(e.get(),m) << "\n";
- }
-
- public:
- inst_gen_unif_index(ast_manager & m) :
- m(m), m_st(m), m_num_vars(0), m_ref_holder(m) {}
-
- void insert_literal(app * lit) {
- // debug_st("st_insert", lit);
- m_ref_holder.push_back(lit);
- m_st.insert(lit);
- }
-
- void get_unifications(app * lit, app_ref_vector& res) {
- substitution subst(m);
- subst.reserve_vars(m_num_vars);
- subst.reserve_offsets(m_st.get_approx_num_regs());
- collecting_visitor visitor(res, subst);
- // TRACE("theory_instgen", m_st.display(tout); );
- m_st.unify(lit, visitor);
- }
- void reserve_num_vars(unsigned num_vars) {
- if (num_vars > m_num_vars) m_num_vars = num_vars;
- }
-
- void push() {
- m_lim.push_back(m_ref_holder.size());
- }
-
- void pop() {
- unsigned sz = m_lim.back();
- m_ref_holder.resize(sz);
- m_lim.pop_back();
- m_st.reset();
- }
-
- void pop_orig() {
- unsigned sz = m_lim.back();
- while (m_ref_holder.size() > sz) {
- debug_st("st_erase", m_ref_holder.back());
- m_st.erase(m_ref_holder.back());
-
- substitution subst(m);
- subst.reserve_vars(m_num_vars);
- subst.reserve_offsets(m_st.get_approx_num_regs());
- st_contains_visitor cv(subst, m_ref_holder.back());
- m_st.unify(m_ref_holder.back(), cv);
- if (cv.found()) {
- m_st.display(std::cout);
- m_st.erase(m_ref_holder.back());
- }
- SASSERT(!cv.found());
- m_ref_holder.pop_back();
- }
- m_lim.pop_back();
- }
-
- void display(std::ostream& out) {
- m_st.display(out);
- }
-
- bool empty() const{
- return m_st.empty();
- }
- };
-
-
- ///////////////////////////
- // fo_clause_internalizer
- //
-
- class fo_clause_internalizer {
- private:
- typedef map<literal, app_ref_vector*, obj_hash<literal>, default_eq<literal> > literal_meaning_map;
- typedef obj_map<expr,quantifier_ref_vector*> occurs;
- typedef obj_map<expr,quantifier*> root_clause_map; //for any clause instance it gives us the clause from the original problem
-
- theory_instgen_impl& m_parent;
- expr_ref_vector m_vars;
- var_subst m_subst;
- occurs m_occurs;
- grounder m_grounder;
- /**
- For each clause which is a result of instantiation contains the
- original problem clause from which it derives.
- */
- root_clause_map m_root_clause_map;
-
-
- /**
- For each SMT literal contains a vector of first-order literals
- that are represented by this literal.
- */
- literal_meaning_map m_literal_meanings;
-
- /**
- fo literals that have been internalized by this object.
- Invariant: any app* fol in this set has a literal l such that
- m_literal_meanings[l].contains(fol).
- Particularly, l==get_context().get_literal(gnd_fol) where gnd_fol
- is a grounded version of this literal
- */
- obj_hashtable<expr> m_internalized_fo_lits;
-
-
- ast_manager& m() const;
- smt::context& get_context() const;
-
- class insert_occurs_trail : public trail<smt::context> {
- occurs& m_occ;
- quantifier_ref_vector* m_qs;
- expr_ref m_lit;
- public:
- insert_occurs_trail(occurs& o, expr_ref& lit, quantifier* q): m_occ(o), m_qs(0), m_lit(lit) {
- occurs::obj_map_entry* e = m_occ.insert_if_not_there2(lit,0);
- m_qs = e->get_data().m_value;
- if (!m_qs) {
- m_qs = alloc(quantifier_ref_vector, lit.get_manager());
- e->get_data().m_value = m_qs;
- }
- m_qs->push_back(q);
- }
-
- virtual void undo(smt::context& ctx) {
- SASSERT(m_qs && !m_qs->empty());
- SASSERT(m_qs == m_occ.find_core(m_lit)->get_data().m_value);
- m_qs->pop_back();
- if (m_qs->empty()) {
- m_occ.remove(m_lit);
- dealloc(m_qs);
- }
- }
- };
-
- class lit_meaning_trail : public trail<smt::context> {
- literal_meaning_map& m_map;
- app_ref_vector* m_apps;
- smt::literal m_smtlit;
- public:
-
- lit_meaning_trail(literal_meaning_map& map, ast_manager& m, smt::literal l, app* lit):
- m_map(map), m_smtlit(l) {
- literal_meaning_map::entry* e = map.insert_if_not_there2(l, 0);
- m_apps = e->get_data().m_value;
- if (!m_apps) {
- m_apps = alloc(app_ref_vector, m);
- e->get_data().m_value = m_apps;
- }
- m_apps->push_back(lit);
- }
-
- virtual void undo(smt::context& ctx) {
- SASSERT(m_apps && !m_apps->empty());
- SASSERT(m_apps == m_map.find_core(m_smtlit)->get_data().m_value);
- m_apps->pop_back();
- if (m_apps->empty()) {
- m_map.remove(m_smtlit);
- dealloc(m_apps);
- }
- }
- };
-
- quantifier * get_root_clause(expr* clause) const {
- quantifier * root;
- if(!m_root_clause_map.find(clause, root)) {
- SASSERT(is_forall(clause));
- root = to_quantifier(clause);
- }
- return root;
- }
-
- void replace_by_root_clauses(ptr_vector<quantifier>& vect) const {
- unsigned sz = vect.size();
- for(unsigned i=0; i<sz; ++i) {
- vect[i] = get_root_clause(vect[i]);
- }
- }
-
- literal get_root_clause_control_literal(quantifier* root_clause) {
- get_context().internalize(root_clause, true);
- return get_context().get_literal(root_clause);
- }
-
- //
- // Grounding
- //
-
- void insert_occurs(app * lit, quantifier* clause) {
- SASSERT(clause);
- TRACE("theory_instgen", tout << PP(lit, m()) << " occurs in " << PP(clause, m()) << "\n";);
- expr_ref t(lit,m());
- get_context().push_trail(insert_occurs_trail(m_occurs, t, clause));
- }
-
- literal ground_fo_literal(app * lit, quantifier* q) {
-
- literal smt_lit;
-
- if (is_ground(lit)) {
- get_context().internalize(lit, true);
- smt_lit = get_context().get_literal(lit);
- get_context().mark_as_relevant(smt_lit);
- return smt_lit;
- }
- insert_occurs(lit, q);
-
- app_ref grounded_lit(m());
- m_grounder(lit, grounded_lit);
-
- if(m_internalized_fo_lits.contains(lit)) {
- smt_lit = get_context().get_literal(grounded_lit);
- }
- else {
- get_context().internalize(grounded_lit, true);
- smt_lit = get_context().get_literal(grounded_lit);
- m_internalized_fo_lits.insert(lit);
-
- expr_ref t(lit, m());
- get_context().push_trail(obj_ref_trail<smt::context,ast_manager,expr>(t));
- get_context().push_trail(insert_obj_trail<smt::context,expr>(m_internalized_fo_lits, lit));
- get_context().push_trail(lit_meaning_trail(m_literal_meanings, m(), smt_lit, lit));
- TRACE("theory_instgen", tout << smt_lit << " "<< PP(grounded_lit, m()) << " |-> " << PP(lit, m()) << "\n";);
- }
- get_context().mark_as_relevant(smt_lit);
- return smt_lit;
- }
-
- void add_clause_to_smt(expr * clause, quantifier* root_clause, ptr_vector<quantifier> const& assumptions=ptr_vector<quantifier>());
-
- void get_instance_clause(instantiation_result const& ir, expr_ref& res);
-
- /**
- return false if nothing was done
-
- assumptions are instantiated clauses (to get a correct assumption for the SMT solver, we need
- to convert the vector to root clauses).
- */
- bool simplify_clause(quantifier * clause, expr_ref& result, ptr_vector<quantifier>& assumptions);
-
- public:
-
- fo_clause_internalizer(theory_instgen_impl& parent):
- m_parent(parent),
- m_vars(m()),
- m_subst(m()),
- m_grounder(m()) {
- }
-
- ~fo_clause_internalizer() {
- reset_dealloc_values(m_occurs);
- }
-
- void get_literal_meanings(literal l, ptr_vector<app>& fo_lits) {
- app_ref_vector* lits = 0;
- m_literal_meanings.find(l, lits);
- if (lits) {
- fo_lits.append(lits->size(), lits->c_ptr());
- }
- }
-
- void add_initial_clause(quantifier* q) {
- add_clause_to_smt(q, 0);
- }
-
- quantifier_ref_vector* find_occurs(app * l) {
- quantifier_ref_vector* result = 0;
- m_occurs.find(l, result);
- return result;
- }
-
- void add_new_instance(instantiation_result const& ir) {
- quantifier * root_clause = get_root_clause(ir.clause());
- expr_ref inst_clause(m());
- get_instance_clause(ir, inst_clause);
-
- ptr_vector<quantifier> assumptions;
- if(is_quantifier(inst_clause.get())) {
- quantifier * q_clause = to_quantifier(inst_clause.get());
- bool simplified = simplify_clause(q_clause, inst_clause, assumptions);
- SASSERT(simplified || assumptions.empty());
- }
- replace_by_root_clauses(assumptions);
-
- if(!m_root_clause_map.contains(inst_clause)) {
- m_root_clause_map.insert(inst_clause, root_clause);
- get_context().push_trail(insert_obj_map<smt::context,expr,quantifier*>(m_root_clause_map, inst_clause));
- }
- add_clause_to_smt(inst_clause, root_clause, assumptions);
- }
- };
-
-
- /////////////////
- // instantiator
- //
-
- class instantiator {
- private:
- typedef quantifier clause_type;
- typedef ptr_vector<clause_type> clause_vector;
- typedef obj_map<quantifier,matching_set*> matching_sets;
-
- ast_manager& m;
- theory_instgen_impl& m_parent;
- fo_clause_internalizer& m_internalizer;
- inst_gen_unif_index m_unif_index;
- matching_sets m_matching;
- unifier m_unifier; //used in the unify method, but we don't want to recreate over and over
-
- class var_rename_rewriter_cfg : public default_rewriter_cfg {
- ast_manager& m;
- u_map<unsigned> m_index_rename;
- public:
- var_rename_rewriter_cfg(ast_manager& m) : m(m) {}
-
- bool get_subst(expr * s, expr * & t, proof * & t_pr) {
- if (is_var(s)) {
- unsigned idx = to_var(s)->get_idx();
- unsigned new_idx = 0;
- if (!m_index_rename.find(idx, new_idx)) {
- new_idx = m_index_rename.size();
- m_index_rename.insert(idx, new_idx);
- }
- t = m.mk_var(new_idx, to_var(s)->get_sort());
- return true;
- }
- else {
- return false;
- }
- }
- };
-
- static void extract_substitution(substitution& s, quantifier * q, unsigned subst_var_cnt, bool is_first_bank, expr_ref_vector& tgt) {
- // unsigned var_increment = is_first_bank ? 0 : subst_var_cnt;
- unsigned var_offset = is_first_bank ? 0 : 1;
-
- unsigned deltas[2] = {0, subst_var_cnt};
- ast_manager& m = s.get_manager();
- unsigned var_cnt = q->get_num_decls();
- var_rename_rewriter_cfg r_cfg(m);
- rewriter_tpl<var_rename_rewriter_cfg> rwr(m, false, r_cfg);
- for(unsigned i=0; i<var_cnt; i++) {
- sort * var_sort = q->get_decl_sort(i);
- unsigned var_idx = var_cnt-1-i;
- var_ref v(m.mk_var(var_idx, var_sort), m);
- expr_ref tmp(m), subst_result(m);
- s.apply(2, deltas, expr_offset(v.get(), var_offset), tmp);
- rwr(tmp, subst_result);
- tgt.push_back(subst_result);
- }
- }
-
-
- // just to be sure there's not misunderstanding with the caller, we require the res to be empty:)
- void get_literal_occurrences(app * lit, clause_vector& res) {
- SASSERT(res.empty());
- quantifier_ref_vector * occurrences = m_internalizer.find_occurs(lit);
- if(occurrences) {
- res.append(occurrences->size(), occurrences->c_ptr());
- }
- }
-
- /**
- check substitution wrt dismatching constraints of clause
- (variable offset is to deal with how variable banks are shifted on each
- other in the substitution)
- */
- bool is_allowed_instantiation(clause_type * clause, const inst& subst) {
- matching_set * ms;
- return !m_matching.find(clause, ms) || !ms->has_instance(subst);
- }
-
- class new_ms : public trail<smt::context> {
- matching_sets& m_ms;
- matching_set* m_s;
- quantifier* m_q;
- public:
- new_ms(matching_sets& m, matching_set* s, quantifier* q): m_ms(m), m_s(s), m_q(q) {}
- virtual void undo(smt::context& ctx) { dealloc(m_s); m_ms.remove(m_q); }
- };
-
- // add instantiating substitution among the dismatching constraints
- void record_instantiation(instantiation_result const& inst) {
- quantifier * cl = inst.clause();
- matching_set * ms;
- if(!m_matching.find(cl, ms)) {
- ms = alloc(matching_set, m);
- m_matching.insert(cl, ms);
- get_context().push_trail(new_ms(m_matching, ms, cl));
- }
- ms->insert(inst.subst());
- get_context().push_trail(matching_set::insert_inst(*ms));
- }
-
- void get_result_from_subst(clause_type * clause, const inst& subst, instantiation_result& res) {
- res.init(clause, subst);
- record_instantiation(res);
- }
-
- void display_vector(expr_ref_vector const& v, std::ostream& out) {
- for (unsigned i = 0; i < v.size(); ++i) {
- out << PP(v[i], m) << " ";
- }
- out << "\n";
- }
-
-
- void add_lit(literal lit) {
- ptr_vector<app> fo_lits;
- m_internalizer.get_literal_meanings(lit, fo_lits);
- expr_ref e(m);
- get_context().literal2expr(lit, e);
- if (is_ground(e.get())) {
- fo_lits.push_back(to_app(e));
- }
- for (unsigned i = 0; i < fo_lits.size(); ++i) {
- app * fol = fo_lits[i];
- m_unif_index.insert_literal(fol);
- }
- }
-
- void mk_folit_neg(app * lit, app_ref& res) {
- expr * arg;
- if(m.is_not(lit, arg)) {
- SASSERT(is_app(arg));
- res = to_app(arg);
- }
- else {
- res = m.mk_not(lit);
- }
- }
-
- ast_manager& get_manager() const;
- context& get_context() const;
-
- public:
- instantiator(fo_clause_internalizer& internalizer, theory_instgen_impl& parent, ast_manager& m) :
- m(m),
- m_parent(parent),
- m_internalizer(internalizer),
- m_unif_index(m),
- m_unifier(m) {}
-
- ~instantiator() {
- reset_dealloc_values(m_matching);
- }
-
- bool unif_is_empty() const {
- return m_unif_index.empty();
- }
-
- void display(std::ostream& out) {
- m_unif_index.display(out);
- }
-
- void add_true_lit(literal lit) {
- add_lit(lit);
- }
-
- void push() {
- m_unif_index.push();
- }
-
- void pop() {
- m_unif_index.pop();
- }
-
- void reserve_num_vars(unsigned num_vars) {
- m_unif_index.reserve_num_vars(num_vars);
- }
-
- bool instantiate_clauses(
- app * lit1, clause_type * clause1,
- app * lit2, clause_type * clause2,
- instantiation_result_vector& result);
-
- bool instantiate_clause(
- app * lit1, clause_type * clause1, app * lit2,
- instantiation_result_vector& result);
-
- void do_instantiating(literal lit, instantiation_result_vector& res) {
- ptr_vector<app> folits;
- clause_vector folit_clauses; // clauses in which the first-order literal appears
- app_ref_vector unifs(m); // unifying complementary literals
- clause_vector comp_clauses; // clauses in which the unifying complementary literal appears
-
- m_internalizer.get_literal_meanings(lit, folits);
-
- while(!folits.empty()) {
- app * folit = folits.back();
-
- folits.pop_back();
- folit_clauses.reset();
- get_literal_occurrences(folit, folit_clauses);
- SASSERT(!folit_clauses.empty()); //if we have a literal it should be in some clause (or not?)
-
- SASSERT(folit->get_ref_count() > 0);
- app_ref complementary(m);
- mk_folit_neg(folit, complementary);
- m_unif_index.get_unifications(complementary, unifs);
-
- while(!unifs.empty()) {
- app * comp_lit = unifs.back();
- unifs.pop_back();
- SASSERT(comp_lit->get_ref_count() > 0);
- comp_clauses.reset();
- get_literal_occurrences(comp_lit, comp_clauses);
- TRACE("theory_instgen", tout << "Literal " << lit << " meaning: " << PP(folit, m) << "\n";
- tout << "Unifies with: " << PP(comp_lit, m) << "\n";);
- //
- //if a literal is in the unification index (i.e. was assigned true sometime before),
- //it should be in some clause or it is a ground literal.
-
- //iterate through all clauses that contain the query literal
- //
- clause_vector::const_iterator fc_end = folit_clauses.end();
- for(clause_vector::const_iterator fc_it = folit_clauses.begin(); fc_it!=fc_end; ++fc_it) {
-
- //iterate through all clauses that contain the complementary unifying literal
- clause_vector::const_iterator end = comp_clauses.end();
- for(clause_vector::const_iterator it = comp_clauses.begin(); it!=end; ++it) {
-
- instantiate_clauses(folit, *fc_it, comp_lit, *it, res);
- }
- if (comp_clauses.empty()) {
- instantiate_clause(folit, *fc_it, comp_lit, res);
- }
- }
- }
- complementary.reset();
- }
- }
- };
-
-
- ///////////////////////////
- // theory_instgen_impl
- //
-
- class theory_instgen_impl : public theory_instgen {
-
- friend class instantiator;
- friend class fo_clause_internalizer;
-
- struct stats {
- unsigned m_num_axioms;
- unsigned m_num_subsumptions;
- unsigned m_num_pruned;
- stats() { memset(this, 0, sizeof(*this)); }
- };
-
- ast_manager& m_manager;
- smt_params& m_params;
- fo_clause_internalizer m_internalizer;
- instantiator m_instantiator;
- clause_subsumption m_subsumer;
- stats m_stats;
-
- final_check_status instantiate_all_possible() {
- // traverse instantiation queue and create initial instances.
-
- ast_manager& m = get_manager();
- context& ctx = get_context();
- instantiation_result_vector generated_clauses;
- unsigned bv_cnt = ctx.get_num_bool_vars();
-
- m_instantiator.push();
-
- TRACE("theory_instgen",
- tout << "Literals:\n";
- for (unsigned v = 0; v < bv_cnt; ++v) {
- if (l_undef == ctx.get_assignment(v)) continue;
- literal lit(v, ctx.get_assignment(v) == l_false);
- expr_ref e(m);
- ctx.literal2expr(lit, e);
- tout << PP(e.get(),m) << "\n";
- }
- );
-
- SASSERT(m_instantiator.unif_is_empty());
-
- for(unsigned bvi=0; bvi < bv_cnt; ++bvi) {
- lbool asgn_val = ctx.get_assignment(bvi);
- if(asgn_val==l_undef) {
- continue;
- }
- literal lit(bvi, asgn_val==l_false);
- m_instantiator.add_true_lit(lit);
- m_instantiator.do_instantiating(lit, generated_clauses);
- }
-
- bool change = !generated_clauses.empty();
-
- while(!generated_clauses.empty()) {
- m_internalizer.add_new_instance(generated_clauses.back());
- generated_clauses.pop_back();
- }
-
- m_instantiator.pop();
-
- return change?FC_CONTINUE:FC_DONE;
- }
-
-
- public:
- theory_instgen_impl(ast_manager& m, smt_params& p):
- theory_instgen(m.get_family_id("inst_gen")),
- m_manager(m),
- m_params(p),
- m_internalizer(*this),
- m_instantiator(m_internalizer, *this, m),
- m_subsumer(m, p)
- {}
-
- ast_manager& m() { return m_manager; }
-
- virtual void internalize_quantifier(quantifier* q) {
- TRACE("theory_instgen", tout << PP(q, m()) << "\n";);
- context& ctx = get_context();
- if (!ctx.b_internalized(q)) {
- bool_var v = ctx.mk_bool_var(q);
- ctx.set_var_theory(v, get_id());
- m_instantiator.reserve_num_vars(q->get_num_decls());
- }
- }
-
- virtual bool internalize_atom(app * atom, bool gate_ctx) {
- UNREACHABLE();
- return false;
- }
-
- virtual bool internalize_term(app * term) {
- UNREACHABLE();
- return false;
- }
-
- virtual void new_eq_eh(theory_var v1, theory_var v2) {}
-
- virtual void new_diseq_eh(theory_var v1, theory_var v2) {}
-
- virtual theory * mk_fresh(context * new_ctx) {
- return alloc(theory_instgen_impl, get_manager(), m_params);
- }
-
- virtual void assign_eh(bool_var v, bool is_true) {
- context& ctx = get_context();
- expr* e = ctx.bool_var2expr(v);
- if (is_quantifier(e)) {
- if (is_true) {
- m_internalizer.add_initial_clause(to_quantifier(e));
- }
- else {
- // TBD: handle existential force later.
- }
- }
- }
-
- virtual final_check_status final_check_eh() {
- TRACE("theory_instgen", tout << "Final check\n";);
- return instantiate_all_possible();
- }
-
- virtual void init_model(smt::model_generator & m) { }
-
- virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator & m) {
- UNREACHABLE();
- return 0;
- }
-
- virtual void relevant_eh(app * n) { }
-
- virtual void push_scope_eh() {
- m_subsumer.push();
- }
-
- virtual void pop_scope_eh(unsigned num_scopes) {
- m_subsumer.pop(num_scopes);
- }
-
- virtual void collect_statistics(::statistics & st) const {
- st.update("inst axiom", m_stats.m_num_axioms);
- st.update("inst subsump", m_stats.m_num_subsumptions);
- }
-
- void inc_subsumptions() {
- ++m_stats.m_num_subsumptions;
- }
-
- void inc_axioms() {
- ++m_stats.m_num_axioms;
- }
-
- void inc_pruned() {
- ++m_stats.m_num_pruned;
- }
-
- };
-
- theory_instgen* mk_theory_instgen(ast_manager& m, smt_params& p) {
- return alloc(theory_instgen_impl, m, p);
- }
-
- ast_manager& instantiator::get_manager() const {
- return m_parent.m();
- }
-
- smt::context& instantiator::get_context() const {
- return m_parent.get_context();
- }
-
- bool instantiator::instantiate_clauses(
- app * lit1, clause_type * clause1,
- app * lit2, clause_type * clause2,
- instantiation_result_vector& result) {
- TRACE("theory_instgen", tout << PP(lit1, m) << " " << PP(clause1, m) << "\n";
- tout << PP(lit2, m) << " " << PP(clause2, m) << "\n";);
- substitution subst(m);
- unsigned var_cnt = std::max(clause1->get_num_decls(), clause2->get_num_decls());
- subst.reserve(2, var_cnt);
- //don't trust there offset values too much, it's just what i expect the substitution does:)
- app_ref complementary(m);
- mk_folit_neg(lit1, complementary);
- TRUSTME(m_unifier(complementary, lit2, subst));
-
- inst subst1(m);
- extract_substitution(subst, clause1, var_cnt, true, subst1);
- inst subst2(m);
- extract_substitution(subst, clause2, var_cnt, false, subst2);
-
- bool s1_identity = matching_set::is_identity(subst1);
- bool s2_identity = matching_set::is_identity(subst2);
-
- if((!s1_identity && !is_allowed_instantiation(clause1, subst1)) ||
- (!s2_identity && !is_allowed_instantiation(clause2, subst2))) {
- TRACE("theory_instgen",
- tout << "Pruned instantiation\n";
- tout << PP(clause1, m) << "\n";
- display_vector(subst1, tout);
- tout << PP(clause2, m) << "\n";
- display_vector(subst2, tout);
- );
- m_parent.inc_pruned();
- return false;
- }
-
- //
- // both substitutions cannot be identity as then the two complementary
- // literals would correspond to the same SAT solver variable
- //
- SASSERT(!s1_identity || !s2_identity);
-
- if(!s1_identity) {
- instantiation_result res1(m);
- get_result_from_subst(clause1, subst1, res1);
- result.push_back(res1);
- }
-
- if(!s2_identity) {
- instantiation_result res2(m);
- get_result_from_subst(clause2, subst2, res2);
- result.push_back(res2);
- }
- return true;
- }
-
- // literal lit2 is ground. It is not associated with a clause.
- // literal lit1 is associatd with a non-ground clause.
- bool instantiator::instantiate_clause(
- app * lit1, clause_type * clause1, app * lit2,
- instantiation_result_vector& result) {
- TRACE("theory_instgen", tout << PP(lit1, m) << " " << PP(clause1, m) << "\n";
- tout << PP(lit2, m) << "\n";);
- if (!is_ground(lit2)) {
- // TBD: remove. Debug code.
- std::cout << PP(lit1, m) << " " << PP(clause1, m) << "\n";
- std::cout << PP(lit2, m) << "\n";
- m_unif_index.display(std::cout);
- }
- SASSERT(is_ground(lit2));
- substitution subst(m);
- unsigned var_cnt = clause1->get_num_decls();
- subst.reserve(2, var_cnt);
- app_ref complementary(m);
- mk_folit_neg(lit1, complementary);
-
- TRUSTME(m_unifier(complementary, lit2, subst));
-
- inst subst1(m);
- extract_substitution(subst, clause1, var_cnt, true, subst1);
-
- if(matching_set::is_identity(subst1) ||
- !is_allowed_instantiation(clause1, subst1)) {
- TRACE("theory_instgen",
- tout << "Pruned instantiation\n";
- tout << PP(clause1, m) << "\n";
- display_vector(subst1, tout);
- );
- m_parent.inc_pruned();
- return false;
- }
-
- instantiation_result res1(m);
- get_result_from_subst(clause1, subst1, res1);
- result.push_back(res1);
- return true;
- }
-
-
- //--------------------------
- //
- // fo_clause_internalizer
- //
- //--------------------------
-
- smt::context& fo_clause_internalizer::get_context() const {
- return m_parent.get_context();
- }
-
- ast_manager& fo_clause_internalizer::m() const {
- return m_parent.m();
- }
-
- bool fo_clause_internalizer::simplify_clause(quantifier * clause, expr_ref& result, ptr_vector<quantifier>& assumptions) {
- m_parent.m_subsumer.simplify(clause, result, assumptions);
- bool change = clause!=result.get();
- if (change) {
- m_parent.inc_subsumptions();
- }
- return change;
- }
-
- void fo_clause_internalizer::get_instance_clause(instantiation_result const& ir, expr_ref& res) {
- expr * orig_cl = ir.clause()->get_expr();
- SASSERT(is_app(orig_cl));
-
- expr_ref res_inner(m()); //the clause after substitution, we might still need to quantify it
- m_subst(orig_cl, ir.subst().size(), ir.subst().c_ptr(), res_inner);
- SASSERT(is_app(res_inner.get()));
-
- if(is_ground(res_inner.get())) {
- res = res_inner;
- return; //we made it ground!
- }
-
- ptr_vector<sort> free_var_sorts;
- svector<symbol> quant_names;
- get_free_vars(res_inner.get(), free_var_sorts);
- unsigned free_var_cnt = free_var_sorts.size();
- for(unsigned i=0; i<free_var_cnt; i++) {
- if(!free_var_sorts[i]) {
- free_var_sorts[i] = m().mk_bool_sort(); //get a dummy variable
- }
- quant_names.push_back(symbol(free_var_cnt-i-1));
- }
- free_var_sorts.reverse();
-
- quantifier_ref q_with_unused(m().mk_quantifier(true, free_var_cnt, free_var_sorts.c_ptr(), quant_names.c_ptr(), res_inner.get()), m());
- elim_unused_vars(m(), q_with_unused, res);
- }
-
- /**
- Clause can be either ground (app) or non-ground (quantifier). Root clause
- should be the original input clause from which the current clause was
- instantiated, or zero if this clause is initial
- */
- void fo_clause_internalizer::add_clause_to_smt(expr * clause, quantifier* root_clause, ptr_vector<quantifier> const& assumptions) {
- SASSERT(!root_clause || root_clause->is_forall());
- SASSERT(is_quantifier(clause) || root_clause);
- context& ctx = get_context();
- buffer<literal> lits;
- ptr_buffer<expr> todo;
-
- bool is_q_clause = is_quantifier(clause);
- quantifier * q_clause = is_q_clause ? to_quantifier(clause) : 0;
- if (!root_clause) root_clause = q_clause;
-
- lits.push_back(~get_root_clause_control_literal(root_clause));
-
- for(unsigned i=0; i<assumptions.size(); ++i) {
- lits.push_back(~get_root_clause_control_literal(assumptions[i]));
- }
-
- todo.push_back(is_q_clause?(q_clause->get_expr()):clause);
-
- while (!todo.empty()) {
- expr* e = todo.back();
- todo.pop_back();
- if (m().is_or(e)) {
- todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
- }
- else if (is_app(e)) {
- lits.push_back(ground_fo_literal(to_app(e), q_clause));
- }
- else {
- SASSERT(is_var(e) || is_quantifier(e));
- UNREACHABLE();
- //by skipping part of the disjunction we may get unsound
- }
- }
- TRACE("theory_instgen",
- tout << "Axiom: \n";
- for (unsigned i = 0; i < lits.size(); ++i) {
- expr_ref e(m());
- get_context().literal2expr(lits[i], e);
- tout << PP(e.get(), m()) << "\n";
- }
- );
- m_parent.inc_axioms();
- ctx.mk_th_axiom(m_parent.get_id(), lits.size(), lits.c_ptr());
- }
-
-
-};
diff --git a/src/smt/theory_instgen.h b/src/smt/theory_instgen.h
deleted file mode 100644
index c32636e9b..000000000
--- a/src/smt/theory_instgen.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- theory_instgen.h
-
-Abstract:
-
- InstGen (iProver) style theory solver.
- It provides an instantiation based engine
- based on InstGen methods together with
- unit propagation.
-
-
-Author:
-
- Krystof Hoder (t-khoder)
- Nikolaj Bjorner (nbjorner) 2011-10-6
-
-Revision History:
-
---*/
-#ifndef _THEORY_INST_GEN_H_
-#define _THEORY_INST_GEN_H_
-
-#include "smt_theory.h"
-#include "smt_params.h"
-
-namespace smt {
-
- class theory_instgen : public theory {
- public:
- theory_instgen(family_id fid) : theory(fid) {}
- virtual ~theory_instgen() {}
- virtual void internalize_quantifier(quantifier* q) = 0;
- virtual char const * get_name() const { return "instgen"; }
- };
-
- theory_instgen* mk_theory_instgen(ast_manager& m, smt_params& p);
-
-};
-
-#endif /* _THEORY_INST_GEN_H_ */
-
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index cca21b90e..831efa087 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -18,7 +18,7 @@ Notes:
--*/
#include"ctx_simplify_tactic.h"
#include"mk_simplified_app.h"
-#include"num_occurs_goal.h"
+#include"goal_num_occurs.h"
#include"cooperate.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
@@ -51,7 +51,7 @@ struct ctx_simplify_tactic::imp {
unsigned m_scope_lvl;
unsigned m_depth;
unsigned m_num_steps;
- num_occurs_goal m_occs;
+ goal_num_occurs m_occs;
mk_simplified_app m_mk_app;
unsigned long long m_max_memory;
unsigned m_max_depth;
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index a79a4ed06..19190c299 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -18,6 +18,7 @@ Revision History:
--*/
#include"nnf.h"
#include"tactical.h"
+#include"filter_model_converter.h"
class nnf_tactic : public tactic {
params_ref m_params;
@@ -100,6 +101,13 @@ public:
}
g->inc_depth();
result.push_back(g.get());
+ unsigned num_extra_names = dnames.get_num_names();
+ if (num_extra_names > 0) {
+ filter_model_converter * fmc = alloc(filter_model_converter, m);
+ mc = fmc;
+ for (unsigned i = 0; i < num_extra_names; i++)
+ fmc->insert(dnames.get_name_decl(i));
+ }
TRACE("nnf", g->display(tout););
SASSERT(g->is_well_sorted());
}
diff --git a/src/tactic/num_occurs_goal.cpp b/src/tactic/goal_num_occurs.cpp
similarity index 75%
rename from src/tactic/num_occurs_goal.cpp
rename to src/tactic/goal_num_occurs.cpp
index adc412434..6c94e307c 100644
--- a/src/tactic/num_occurs_goal.cpp
+++ b/src/tactic/goal_num_occurs.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
- num_occurs_goal.cpp
+ goal_num_occurs.cpp
Abstract:
@@ -15,10 +15,10 @@ Author:
Revision History:
--*/
-#include"num_occurs_goal.h"
+#include"goal_num_occurs.h"
#include"goal.h"
-void num_occurs_goal::operator()(goal const & g) {
+void goal_num_occurs::operator()(goal const & g) {
expr_fast_mark1 visited;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
diff --git a/src/tactic/num_occurs_goal.h b/src/tactic/goal_num_occurs.h
similarity index 64%
rename from src/tactic/num_occurs_goal.h
rename to src/tactic/goal_num_occurs.h
index 5e6e0cc94..33a25e03f 100644
--- a/src/tactic/num_occurs_goal.h
+++ b/src/tactic/goal_num_occurs.h
@@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
- num_occurs_goal.h
+ goal_num_occurs.h
Abstract:
@@ -15,16 +15,16 @@ Author:
Revision History:
--*/
-#ifndef _NUM_OCCURS_GOAL_H_
-#define _NUM_OCCURS_GOAL_H_
+#ifndef _GOAL_NUM_OCCURS_H_
+#define _GOAL_NUM_OCCURS_H_
#include"num_occurs.h"
class goal;
-class num_occurs_goal : public num_occurs {
+class goal_num_occurs : public num_occurs {
public:
- num_occurs_goal(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
+ goal_num_occurs(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
num_occurs(ignore_ref_count1, ignore_quantifiers) {
}