mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
merge interp/duality changes with unstable
This commit is contained in:
commit
732035bf63
|
@ -639,8 +639,8 @@ def is_CXX_gpp():
|
|||
return is_compiler(CXX, 'g++')
|
||||
|
||||
def is_clang_in_gpp_form(cc):
|
||||
version_string = subprocess.check_output([cc, '--version'])
|
||||
return version_string.find('clang') != -1
|
||||
version_string = check_output([cc, '--version'])
|
||||
return str(version_string).find('clang') != -1
|
||||
|
||||
def is_CXX_clangpp():
|
||||
if is_compiler(CXX, 'g++'):
|
||||
|
@ -1198,9 +1198,9 @@ class JavaDLLComponent(Component):
|
|||
deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile)
|
||||
out.write(deps)
|
||||
out.write('\n')
|
||||
if IS_WINDOWS:
|
||||
JAVAC = '"%s"' % JAVAC
|
||||
JAR = '"%s"' % JAR
|
||||
#if IS_WINDOWS:
|
||||
JAVAC = '"%s"' % JAVAC
|
||||
JAR = '"%s"' % JAR
|
||||
t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
|
||||
out.write(t)
|
||||
t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC,
|
||||
|
@ -1437,7 +1437,7 @@ def mk_config():
|
|||
'SO_EXT=.dll\n'
|
||||
'SLINK=cl\n'
|
||||
'SLINK_OUT_FLAG=/Fe\n'
|
||||
'OS_DEFINES=/D _WINDOWS\n')
|
||||
'OS_DEFINES=/D _WINDOWS\n')
|
||||
extra_opt = ''
|
||||
if GIT_HASH:
|
||||
extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
|
||||
|
@ -1485,7 +1485,7 @@ def mk_config():
|
|||
print('Java Compiler: %s' % JAVAC)
|
||||
else:
|
||||
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
|
||||
OS_DEFINES = ""
|
||||
OS_DEFINES = ""
|
||||
ARITH = "internal"
|
||||
check_ar()
|
||||
CXX = find_cxx_compiler()
|
||||
|
@ -1508,7 +1508,7 @@ def mk_config():
|
|||
SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
|
||||
CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
|
||||
else:
|
||||
print "FAILED\n"
|
||||
print("FAILED\n")
|
||||
FOCI2 = False
|
||||
if GIT_HASH:
|
||||
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
|
||||
|
@ -1536,21 +1536,21 @@ def mk_config():
|
|||
SLIBFLAGS = '-dynamiclib'
|
||||
elif sysname == 'Linux':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_LINUX'
|
||||
OS_DEFINES = '-D_LINUX'
|
||||
SO_EXT = '.so'
|
||||
LDFLAGS = '%s -lrt' % LDFLAGS
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
|
||||
elif sysname == 'FreeBSD':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_FREEBSD_'
|
||||
OS_DEFINES = '-D_FREEBSD_'
|
||||
SO_EXT = '.so'
|
||||
LDFLAGS = '%s -lrt' % LDFLAGS
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
|
||||
elif sysname[:6] == 'CYGWIN':
|
||||
CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS
|
||||
OS_DEFINES = '-D_CYGWIN'
|
||||
OS_DEFINES = '-D_CYGWIN'
|
||||
SO_EXT = '.dll'
|
||||
SLIBFLAGS = '-shared'
|
||||
else:
|
||||
|
@ -1586,7 +1586,7 @@ def mk_config():
|
|||
config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
|
||||
config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
|
||||
config.write('SLINK_OUT_FLAG=-o \n')
|
||||
config.write('OS_DEFINES=%s\n' % OS_DEFINES)
|
||||
config.write('OS_DEFINES=%s\n' % OS_DEFINES)
|
||||
if is_verbose():
|
||||
print('Host platform: %s' % sysname)
|
||||
print('C++ Compiler: %s' % CXX)
|
||||
|
|
|
@ -523,7 +523,7 @@ def mk_java():
|
|||
java_native.write(' public static class LongPtr { public long value; }\n')
|
||||
java_native.write(' public static class StringPtr { public String value; }\n')
|
||||
java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n')
|
||||
if IS_WINDOWS:
|
||||
if IS_WINDOWS or os.uname()[0]=="CYGWIN":
|
||||
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name)
|
||||
else:
|
||||
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
|
||||
|
@ -588,6 +588,9 @@ def mk_java():
|
|||
java_wrapper = open(java_wrapperf, 'w')
|
||||
pkg_str = get_component('java').package_name.replace('.', '_')
|
||||
java_wrapper.write('// Automatically generated file\n')
|
||||
java_wrapper.write('#ifdef _CYGWIN\n')
|
||||
java_wrapper.write('typedef long long __int64;\n')
|
||||
java_wrapper.write('#endif\n')
|
||||
java_wrapper.write('#include<jni.h>\n')
|
||||
java_wrapper.write('#include<stdlib.h>\n')
|
||||
java_wrapper.write('#include"z3.h"\n')
|
||||
|
|
|
@ -586,7 +586,7 @@ class FuncDeclRef(AstRef):
|
|||
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def as_func_decl(self):
|
||||
return self.ast
|
||||
return self.ast
|
||||
|
||||
def name(self):
|
||||
"""Return the name of the function declaration `self`.
|
||||
|
|
|
@ -472,6 +472,25 @@ class smt2_printer {
|
|||
ast_manager & m() const { return m_manager; }
|
||||
ast_manager & fm() const { return format_ns::fm(m()); }
|
||||
|
||||
std::string ensure_quote(symbol const& s) {
|
||||
std::string str;
|
||||
if (is_smt2_quoted_symbol(s))
|
||||
str = mk_smt2_quoted_symbol(s);
|
||||
else
|
||||
str = s.str();
|
||||
return str;
|
||||
}
|
||||
|
||||
symbol ensure_quote_sym(symbol const& s) {
|
||||
if (is_smt2_quoted_symbol(s)) {
|
||||
std::string str;
|
||||
str = mk_smt2_quoted_symbol(s);
|
||||
return symbol(str.c_str());
|
||||
}
|
||||
else
|
||||
return s;
|
||||
}
|
||||
|
||||
void pp_var(var * v) {
|
||||
format * f;
|
||||
if (v->get_idx() < m_var_names.size()) {
|
||||
|
@ -501,11 +520,7 @@ class smt2_printer {
|
|||
}
|
||||
|
||||
format * pp_simple_attribute(char const * attr, symbol const & s) {
|
||||
std::string str;
|
||||
if (is_smt2_quoted_symbol(s))
|
||||
str = mk_smt2_quoted_symbol(s);
|
||||
else
|
||||
str = s.str();
|
||||
std::string str = ensure_quote(s);
|
||||
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
|
||||
}
|
||||
|
||||
|
@ -773,7 +788,7 @@ class smt2_printer {
|
|||
void register_var_names(quantifier * q) {
|
||||
unsigned num_decls = q->get_num_decls();
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
symbol name = q->get_decl_name(i);
|
||||
symbol name = ensure_quote_sym(q->get_decl_name(i));
|
||||
if (name.is_numerical()) {
|
||||
unsigned idx = 1;
|
||||
name = next_name("x", idx);
|
||||
|
@ -997,6 +1012,7 @@ public:
|
|||
unsigned idx = 1;
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
symbol name = next_name(var_prefix, idx);
|
||||
name = ensure_quote_sym(name);
|
||||
var_names.push_back(name);
|
||||
m_var_names_set.insert(name);
|
||||
m_var_names.push_back(name);
|
||||
|
|
|
@ -753,12 +753,7 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
|
|||
}
|
||||
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
|
||||
if (is_add(arg1) || is_mul(arg1)) {
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num_args = to_app(arg1)->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++)
|
||||
new_args.push_back(m_util.mk_rem(to_app(arg1)->get_arg(i), arg2));
|
||||
result = m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
return BR_REWRITE2;
|
||||
return BR_FAILED;
|
||||
}
|
||||
else {
|
||||
if (v2.is_neg()) {
|
||||
|
|
|
@ -310,6 +310,8 @@ struct check_logic::imp {
|
|||
return false;
|
||||
non_numeral = arg;
|
||||
}
|
||||
if (non_numeral == 0)
|
||||
return true;
|
||||
if (is_diff_var(non_numeral))
|
||||
return true;
|
||||
if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))
|
||||
|
|
|
@ -515,6 +515,25 @@ bool pdatatype_decl::has_missing_refs(symbol & missing) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
|
||||
hashtable<symbol, symbol_hash_proc, symbol_eq_proc> names;
|
||||
ptr_vector<pconstructor_decl>::const_iterator it = m_constructors.begin();
|
||||
ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
|
||||
for (; it != end; ++it) {
|
||||
ptr_vector<paccessor_decl> const& acc = (*it)->m_accessors;
|
||||
for (unsigned i = 0; i < acc.size(); ++i) {
|
||||
symbol const& name = acc[i]->get_name();
|
||||
if (names.contains(name)) {
|
||||
duplicated = name;
|
||||
return true;
|
||||
}
|
||||
names.insert(name);
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
|
||||
ptr_vector<pconstructor_decl>::iterator it = m_constructors.begin();
|
||||
ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
|
||||
|
|
|
@ -169,6 +169,7 @@ public:
|
|||
class paccessor_decl : public pdecl {
|
||||
friend class pdecl_manager;
|
||||
friend class pconstructor_decl;
|
||||
friend class pdatatype_decl;
|
||||
symbol m_name;
|
||||
ptype m_type;
|
||||
paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r);
|
||||
|
@ -222,6 +223,7 @@ public:
|
|||
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
|
||||
virtual void display(std::ostream & out) const;
|
||||
bool has_missing_refs(symbol & missing) const;
|
||||
bool has_duplicate_accessors(symbol & repeated) const;
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
@ -801,7 +801,7 @@ protected:
|
|||
};
|
||||
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
__declspec(dllexport)
|
||||
#endif
|
||||
void FromClauses(const std::vector<Term> &clauses);
|
||||
|
|
|
@ -1,169 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
iz3hash.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Wrapper for stl hash tables
|
||||
|
||||
Author:
|
||||
|
||||
Ken McMillan (kenmcmil)
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
// pull in the headers for has_map and hash_set
|
||||
// these live in non-standard places
|
||||
|
||||
#ifndef IZ3_HASH_H
|
||||
#define IZ3_HASH_H
|
||||
|
||||
//#define USE_UNORDERED_MAP
|
||||
#ifdef USE_UNORDERED_MAP
|
||||
|
||||
#define stl_ext std
|
||||
#define hash_space std
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
#define hash_map unordered_map
|
||||
#define hash_set unordered_set
|
||||
|
||||
#else
|
||||
|
||||
#if __GNUC__ >= 3
|
||||
#undef __DEPRECATED
|
||||
#define stl_ext __gnu_cxx
|
||||
#define hash_space stl_ext
|
||||
#include <ext/hash_map>
|
||||
#include <ext/hash_set>
|
||||
#else
|
||||
#ifdef WIN32
|
||||
#define stl_ext stdext
|
||||
#define hash_space std
|
||||
#include <hash_map>
|
||||
#include <hash_set>
|
||||
#else
|
||||
#define stl_ext std
|
||||
#define hash_space std
|
||||
#include <hash_map>
|
||||
#include <hash_set>
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
#include <string>
|
||||
|
||||
// stupid STL doesn't include hash function for class string
|
||||
|
||||
#ifndef WIN32
|
||||
|
||||
namespace stl_ext {
|
||||
template <>
|
||||
class hash<std::string> {
|
||||
stl_ext::hash<char *> H;
|
||||
public:
|
||||
size_t operator()(const std::string &s) const {
|
||||
return H(s.c_str());
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
namespace hash_space {
|
||||
template <>
|
||||
class hash<std::pair<int,int> > {
|
||||
public:
|
||||
size_t operator()(const std::pair<int,int> &p) const {
|
||||
return p.first + p.second;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#ifdef WIN32
|
||||
template <> inline
|
||||
size_t stdext::hash_value<std::pair<int,int> >(const std::pair<int,int>& p)
|
||||
{ // hash _Keyval to size_t value one-to-one
|
||||
return p.first + p.second;
|
||||
}
|
||||
#endif
|
||||
|
||||
namespace hash_space {
|
||||
template <class T>
|
||||
class hash<std::pair<T *, T *> > {
|
||||
public:
|
||||
size_t operator()(const std::pair<T *,T *> &p) const {
|
||||
return (size_t)p.first + (size_t)p.second;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#if 0
|
||||
template <class T> inline
|
||||
size_t stdext::hash_value<std::pair<T *, T *> >(const std::pair<T *, T *>& p)
|
||||
{ // hash _Keyval to size_t value one-to-one
|
||||
return (size_t)p.first + (size_t)p.second;
|
||||
}
|
||||
#endif
|
||||
|
||||
#ifdef WIN32
|
||||
|
||||
namespace std {
|
||||
template <>
|
||||
class less<std::pair<int,int> > {
|
||||
public:
|
||||
bool operator()(const pair<int,int> &x, const pair<int,int> &y) const {
|
||||
return x.first < y.first || x.first == y.first && x.second < y.second;
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
namespace std {
|
||||
template <class T>
|
||||
class less<std::pair<T *,T *> > {
|
||||
public:
|
||||
bool operator()(const pair<T *,T *> &x, const pair<T *,T *> &y) const {
|
||||
return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second;
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
#ifndef WIN32
|
||||
|
||||
namespace stl_ext {
|
||||
template <class T>
|
||||
class hash<T *> {
|
||||
public:
|
||||
size_t operator()(const T *p) const {
|
||||
return (size_t) p;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
#ifdef WIN32
|
||||
|
||||
|
||||
|
||||
|
||||
template <class K, class T>
|
||||
class hash_map : public stl_ext::hash_map<K,T,stl_ext::hash_compare<K,std::less<K> > > {};
|
||||
|
||||
template <class K>
|
||||
class hash_set : public stl_ext::hash_set<K,stl_ext::hash_compare<K,std::less<K> > > {};
|
||||
|
||||
#endif
|
||||
|
||||
#endif
|
|
@ -25,7 +25,7 @@ Revision History:
|
|||
#include <string.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -21,7 +21,7 @@ Revision History:
|
|||
|
||||
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
@ -36,10 +36,6 @@ Revision History:
|
|||
#include "duality.h"
|
||||
#include "duality_profiling.h"
|
||||
|
||||
#ifndef WIN32
|
||||
// #define Z3OPS
|
||||
#endif
|
||||
|
||||
// TODO: do we need these?
|
||||
#ifdef Z3OPS
|
||||
|
||||
|
|
|
@ -19,7 +19,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -23,7 +23,7 @@ Revision History:
|
|||
#include <vector>
|
||||
#include <string>
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#define FOCI2_EXPORT __declspec(dllexport)
|
||||
#else
|
||||
#define FOCI2_EXPORT __attribute__ ((visibility ("default")))
|
||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -17,7 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -19,7 +19,7 @@ Revision History:
|
|||
|
||||
/* Copyright 2011 Microsoft Research. */
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
--*/
|
||||
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -17,7 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
--*/
|
||||
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -17,7 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -17,7 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -20,7 +20,7 @@ Revision History:
|
|||
--*/
|
||||
|
||||
|
||||
#ifdef WIN32
|
||||
#ifdef _WINDOWS
|
||||
#pragma warning(disable:4996)
|
||||
#pragma warning(disable:4800)
|
||||
#pragma warning(disable:4267)
|
||||
|
|
|
@ -1465,6 +1465,10 @@ namespace datalog {
|
|||
if (m_rules.get_num_rules() == 0) {
|
||||
return l_false;
|
||||
}
|
||||
if (m_rules.get_predicate_rules(m_query_pred).empty()) {
|
||||
return l_false;
|
||||
}
|
||||
|
||||
|
||||
if (is_linear()) {
|
||||
if (m_ctx.get_engine() == QBMC_ENGINE) {
|
||||
|
|
|
@ -850,6 +850,13 @@ namespace smt2 {
|
|||
for (unsigned i = 0; i < sz; i++) {
|
||||
pdatatype_decl * d = new_dt_decls[i];
|
||||
SASSERT(d != 0);
|
||||
symbol duplicated;
|
||||
if (d->has_duplicate_accessors(duplicated)) {
|
||||
std::string err_msg = "invalid datatype declaration, repeated accessor identifier '";
|
||||
err_msg += duplicated.str();
|
||||
err_msg += "'";
|
||||
throw parser_exception(err_msg, line, pos);
|
||||
}
|
||||
m_ctx.insert(d);
|
||||
if (d->get_num_params() == 0) {
|
||||
// if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors...
|
||||
|
@ -2070,6 +2077,7 @@ namespace smt2 {
|
|||
|
||||
void parse_option_value() {
|
||||
switch (curr()) {
|
||||
case scanner::BV_TOKEN:
|
||||
case scanner::INT_TOKEN:
|
||||
case scanner::FLOAT_TOKEN:
|
||||
m_curr_cmd->set_next_arg(m_ctx, m_scanner.get_number());
|
||||
|
|
|
@ -87,7 +87,7 @@ void display_usage() {
|
|||
std::cout << "\nResources:\n";
|
||||
// timeout and memout are now available on Linux and OSX too.
|
||||
std::cout << " -T:timeout set the timeout (in seconds).\n";
|
||||
std::cout << " -t:timeout set the soft timeout (in seconds). It only kills the current query.\n";
|
||||
std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n";
|
||||
std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n";
|
||||
//
|
||||
std::cout << "\nOutput:\n";
|
||||
|
|
|
@ -27,8 +27,7 @@ enum arith_solver_id {
|
|||
AS_DIFF_LOGIC,
|
||||
AS_ARITH,
|
||||
AS_DENSE_DIFF_LOGIC,
|
||||
AS_UTVPI,
|
||||
AS_HORN
|
||||
AS_UTVPI
|
||||
};
|
||||
|
||||
enum bound_prop_mode {
|
||||
|
|
|
@ -439,12 +439,12 @@ namespace smt {
|
|||
virtual bool model_based() const { return m_fparams->m_mbqi; }
|
||||
|
||||
virtual bool mbqi_enabled(quantifier *q) const {
|
||||
if(!m_fparams->m_mbqi_id) return true;
|
||||
const symbol &s = q->get_qid();
|
||||
unsigned len = strlen(m_fparams->m_mbqi_id);
|
||||
if(s == symbol::null || s.is_numerical())
|
||||
return len == 0;
|
||||
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
|
||||
if(!m_fparams->m_mbqi_id) return true;
|
||||
const symbol &s = q->get_qid();
|
||||
size_t len = strlen(m_fparams->m_mbqi_id);
|
||||
if(s == symbol::null || s.is_numerical())
|
||||
return len == 0;
|
||||
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
|
||||
}
|
||||
|
||||
/* Quantifier id's must begin with the prefix specified by
|
||||
|
|
|
@ -22,7 +22,6 @@ Revision History:
|
|||
#include"theory_arith.h"
|
||||
#include"theory_dense_diff_logic.h"
|
||||
#include"theory_diff_logic.h"
|
||||
#include"theory_horn_ineq.h"
|
||||
#include"theory_utvpi.h"
|
||||
#include"theory_array.h"
|
||||
#include"theory_array_full.h"
|
||||
|
@ -725,12 +724,6 @@ namespace smt {
|
|||
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
|
||||
}
|
||||
break;
|
||||
case AS_HORN:
|
||||
if (m_params.m_arith_int_only)
|
||||
m_context.register_plugin(alloc(smt::theory_ihi, m_manager));
|
||||
else
|
||||
m_context.register_plugin(alloc(smt::theory_rhi, m_manager));
|
||||
break;
|
||||
case AS_UTVPI:
|
||||
if (m_params.m_arith_int_only)
|
||||
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));
|
||||
|
|
|
@ -139,22 +139,32 @@ protected:
|
|||
SASSERT(g.is_well_sorted());
|
||||
}
|
||||
|
||||
struct expr_pos {
|
||||
unsigned m_parent;
|
||||
unsigned m_self;
|
||||
unsigned m_idx;
|
||||
expr* m_expr;
|
||||
expr_pos(unsigned p, unsigned s, unsigned i, expr* e):
|
||||
m_parent(p), m_self(s), m_idx(i), m_expr(e)
|
||||
{}
|
||||
expr_pos():
|
||||
m_parent(0), m_self(0), m_idx(0), m_expr(0)
|
||||
{}
|
||||
};
|
||||
|
||||
void reduce(expr_ref& result){
|
||||
SASSERT(m.is_bool(result));
|
||||
ptr_vector<expr> todo;
|
||||
ptr_vector<expr> names;
|
||||
svector<bool> is_checked;
|
||||
svector<unsigned> parent_ids, self_ids;
|
||||
svector<expr_pos> todo;
|
||||
expr_ref_vector fresh_vars(m), trail(m);
|
||||
expr_ref res(m), tmp(m);
|
||||
obj_map<expr,std::pair<unsigned, expr*> > cache;
|
||||
unsigned id = 1;
|
||||
obj_map<expr, expr_pos> cache;
|
||||
unsigned id = 1, child_id = 0;
|
||||
expr_ref n2(m), fml(m);
|
||||
unsigned path_id = 0, self_pos = 0;
|
||||
unsigned parent_pos = 0, self_pos = 0, self_idx = 0;
|
||||
app * a;
|
||||
unsigned sz;
|
||||
std::pair<unsigned,expr*> path_r;
|
||||
ptr_vector<expr> found;
|
||||
expr_pos path_r;
|
||||
expr_ref_vector args(m);
|
||||
expr_ref n = mk_fresh(id, m.mk_bool_sort());
|
||||
trail.push_back(n);
|
||||
|
@ -163,26 +173,25 @@ protected:
|
|||
tmp = m.mk_not(m.mk_iff(fml, n));
|
||||
m_solver.assert_expr(tmp);
|
||||
|
||||
todo.push_back(fml);
|
||||
todo.push_back(expr_pos(0,0,0,fml));
|
||||
names.push_back(n);
|
||||
is_checked.push_back(false);
|
||||
parent_ids.push_back(0);
|
||||
self_ids.push_back(0);
|
||||
m_solver.push();
|
||||
|
||||
while (!todo.empty() && !m_cancel) {
|
||||
expr_ref res(m);
|
||||
args.reset();
|
||||
expr* e = todo.back();
|
||||
unsigned pos = parent_ids.back();
|
||||
expr* e = todo.back().m_expr;
|
||||
self_pos = todo.back().m_self;
|
||||
parent_pos = todo.back().m_parent;
|
||||
self_idx = todo.back().m_idx;
|
||||
n = names.back();
|
||||
bool checked = is_checked.back();
|
||||
|
||||
if (cache.contains(e)) {
|
||||
goto done;
|
||||
}
|
||||
if (m.is_bool(e) && !checked && simplify_bool(n, res)) {
|
||||
TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
|
||||
if (m.is_bool(e) && simplify_bool(n, res)) {
|
||||
TRACE("ctx_solver_simplify_tactic",
|
||||
tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
|
||||
goto done;
|
||||
}
|
||||
if (!is_app(e)) {
|
||||
|
@ -191,49 +200,31 @@ protected:
|
|||
}
|
||||
|
||||
a = to_app(e);
|
||||
if (!is_checked.back()) {
|
||||
self_ids.back() = ++path_id;
|
||||
is_checked.back() = true;
|
||||
}
|
||||
self_pos = self_ids.back();
|
||||
sz = a->get_num_args();
|
||||
|
||||
sz = a->get_num_args();
|
||||
n2 = 0;
|
||||
|
||||
found.reset(); // arguments already simplified.
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr* arg = a->get_arg(i);
|
||||
if (cache.find(arg, path_r) && !found.contains(arg)) {
|
||||
if (cache.find(arg, path_r)) {
|
||||
//
|
||||
// This is a single traversal version of the context
|
||||
// simplifier. It simplifies only the first occurrence of
|
||||
// a sub-term with respect to the context.
|
||||
//
|
||||
|
||||
found.push_back(arg);
|
||||
if (path_r.first == self_pos) {
|
||||
TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";);
|
||||
args.push_back(path_r.second);
|
||||
}
|
||||
else if (m.is_bool(arg)) {
|
||||
res = local_simplify(a, n, id, i);
|
||||
TRACE("ctx_solver_simplify_tactic",
|
||||
tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
|
||||
args.push_back(res);
|
||||
if (path_r.m_parent == self_pos && path_r.m_idx == i) {
|
||||
args.push_back(path_r.m_expr);
|
||||
}
|
||||
else {
|
||||
args.push_back(arg);
|
||||
}
|
||||
}
|
||||
else if (!n2 && !found.contains(arg)) {
|
||||
else if (!n2) {
|
||||
n2 = mk_fresh(id, m.get_sort(arg));
|
||||
trail.push_back(n2);
|
||||
todo.push_back(arg);
|
||||
parent_ids.push_back(self_pos);
|
||||
self_ids.push_back(0);
|
||||
todo.push_back(expr_pos(self_pos, child_id++, i, arg));
|
||||
names.push_back(n2);
|
||||
args.push_back(n2);
|
||||
is_checked.push_back(false);
|
||||
}
|
||||
else {
|
||||
args.push_back(arg);
|
||||
|
@ -251,22 +242,16 @@ protected:
|
|||
|
||||
done:
|
||||
if (res) {
|
||||
cache.insert(e, std::make_pair(pos, res));
|
||||
}
|
||||
|
||||
TRACE("ctx_solver_simplify_tactic",
|
||||
tout << mk_pp(e, m) << " checked: " << checked << " cached: " << mk_pp(res?res.get():e, m) << "\n";);
|
||||
cache.insert(e, expr_pos(parent_pos, self_pos, self_idx, res));
|
||||
}
|
||||
|
||||
todo.pop_back();
|
||||
parent_ids.pop_back();
|
||||
self_ids.pop_back();
|
||||
names.pop_back();
|
||||
is_checked.pop_back();
|
||||
m_solver.pop(1);
|
||||
}
|
||||
if (!m_cancel) {
|
||||
VERIFY(cache.find(fml, path_r));
|
||||
result = path_r.second;
|
||||
result = path_r.m_expr;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -306,32 +291,6 @@ protected:
|
|||
}
|
||||
return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m);
|
||||
}
|
||||
|
||||
|
||||
expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) {
|
||||
SASSERT(index < a->get_num_args());
|
||||
SASSERT(m.is_bool(a->get_arg(index)));
|
||||
expr_ref n2(m), result(m), tmp(m);
|
||||
n2 = mk_fresh(id, m.get_sort(a->get_arg(index)));
|
||||
ptr_buffer<expr> args;
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
if (i == index) {
|
||||
args.push_back(n2);
|
||||
}
|
||||
else {
|
||||
args.push_back(a->get_arg(i));
|
||||
}
|
||||
}
|
||||
m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result);
|
||||
m_solver.push();
|
||||
tmp = m.mk_eq(result, n);
|
||||
m_solver.assert_expr(tmp);
|
||||
if (!simplify_bool(n2, result)) {
|
||||
result = a->get_arg(index);
|
||||
}
|
||||
m_solver.pop(1);
|
||||
return result;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -1,236 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_horn_ineq.h
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-04-18
|
||||
|
||||
Revision History:
|
||||
|
||||
The implementaton is derived from theory_diff_logic.
|
||||
|
||||
--*/
|
||||
#include "theory_horn_ineq.h"
|
||||
#include "theory_horn_ineq_def.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
template class theory_horn_ineq<ihi_ext>;
|
||||
template class theory_horn_ineq<rhi_ext>;
|
||||
|
||||
// similar to test_diff_logic:
|
||||
|
||||
horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {}
|
||||
|
||||
bool horn_ineq_tester::operator()(expr* e) {
|
||||
m_todo.reset();
|
||||
m_pols.reset();
|
||||
pos_mark.reset();
|
||||
neg_mark.reset();
|
||||
m_todo.push_back(e);
|
||||
m_pols.push_back(l_true);
|
||||
while (!m_todo.empty()) {
|
||||
expr* e = m_todo.back();
|
||||
lbool p = m_pols.back();
|
||||
m_todo.pop_back();
|
||||
m_pols.pop_back();
|
||||
switch (p) {
|
||||
case l_true:
|
||||
if (pos_mark.is_marked(e)) {
|
||||
continue;
|
||||
}
|
||||
pos_mark.mark(e, true);
|
||||
break;
|
||||
case l_false:
|
||||
if (neg_mark.is_marked(e)) {
|
||||
continue;
|
||||
}
|
||||
neg_mark.mark(e, true);
|
||||
break;
|
||||
case l_undef:
|
||||
if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) {
|
||||
continue;
|
||||
}
|
||||
pos_mark.mark(e, true);
|
||||
neg_mark.mark(e, true);
|
||||
break;
|
||||
}
|
||||
if (!test_expr(p, e)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
vector<std::pair<expr*,rational> > const& horn_ineq_tester::get_linearization() const {
|
||||
return m_terms;
|
||||
}
|
||||
|
||||
bool horn_ineq_tester::test_expr(lbool p, expr* e) {
|
||||
expr* e1, *e2, *e3;
|
||||
if (is_var(e)) {
|
||||
return true;
|
||||
}
|
||||
if (!is_app(e)) {
|
||||
return false;
|
||||
}
|
||||
app* ap = to_app(e);
|
||||
if (m.is_and(ap) || m.is_or(ap)) {
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
m_todo.push_back(ap->get_arg(i));
|
||||
m_pols.push_back(p);
|
||||
}
|
||||
}
|
||||
else if (m.is_not(e, e1)) {
|
||||
m_todo.push_back(e);
|
||||
m_pols.push_back(~p);
|
||||
}
|
||||
else if (m.is_ite(e, e1, e2, e3)) {
|
||||
m_todo.push_back(e1);
|
||||
m_pols.push_back(l_undef);
|
||||
m_todo.push_back(e2);
|
||||
m_pols.push_back(p);
|
||||
m_todo.push_back(e3);
|
||||
m_pols.push_back(p);
|
||||
}
|
||||
else if (m.is_iff(e, e1, e2)) {
|
||||
m_todo.push_back(e1);
|
||||
m_pols.push_back(l_undef);
|
||||
m_todo.push_back(e2);
|
||||
m_pols.push_back(l_undef);
|
||||
m_todo.push_back(e2);
|
||||
}
|
||||
else if (m.is_implies(e, e1, e2)) {
|
||||
m_todo.push_back(e1);
|
||||
m_pols.push_back(~p);
|
||||
m_todo.push_back(e2);
|
||||
m_pols.push_back(p);
|
||||
}
|
||||
else if (m.is_eq(e, e1, e2)) {
|
||||
return linearize(e1, e2) == diff;
|
||||
}
|
||||
else if (m.is_true(e) || m.is_false(e)) {
|
||||
// no-op
|
||||
}
|
||||
else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) ||
|
||||
a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) {
|
||||
if (p == l_false) {
|
||||
std::swap(e2, e1);
|
||||
}
|
||||
classify_t cl = linearize(e1, e2);
|
||||
switch(p) {
|
||||
case l_undef:
|
||||
return cl == diff;
|
||||
case l_true:
|
||||
case l_false:
|
||||
return cl == horn || cl == diff;
|
||||
}
|
||||
}
|
||||
else if (!is_uninterp_const(e)) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) {
|
||||
for (unsigned i = 0; i < num_fmls; ++i) {
|
||||
if (!(*this)(fmls[i])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) {
|
||||
m_terms.reset();
|
||||
m_terms.push_back(std::make_pair(e, rational(1)));
|
||||
return linearize();
|
||||
}
|
||||
|
||||
horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) {
|
||||
m_terms.reset();
|
||||
m_terms.push_back(std::make_pair(e1, rational(1)));
|
||||
m_terms.push_back(std::make_pair(e2, rational(-1)));
|
||||
return linearize();
|
||||
}
|
||||
|
||||
horn_ineq_tester::classify_t horn_ineq_tester::linearize() {
|
||||
|
||||
m_weight.reset();
|
||||
m_coeff_map.reset();
|
||||
|
||||
while (!m_terms.empty()) {
|
||||
expr* e1, *e2;
|
||||
rational num;
|
||||
rational mul = m_terms.back().second;
|
||||
expr* e = m_terms.back().first;
|
||||
m_terms.pop_back();
|
||||
if (a.is_add(e)) {
|
||||
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
|
||||
m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul));
|
||||
}
|
||||
}
|
||||
else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) {
|
||||
m_terms.push_back(std::make_pair(e2, mul*num));
|
||||
}
|
||||
else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) {
|
||||
m_terms.push_back(std::make_pair(e2, mul*num));
|
||||
}
|
||||
else if (a.is_sub(e, e1, e2)) {
|
||||
m_terms.push_back(std::make_pair(e1, mul));
|
||||
m_terms.push_back(std::make_pair(e2, -mul));
|
||||
}
|
||||
else if (a.is_uminus(e, e1)) {
|
||||
m_terms.push_back(std::make_pair(e1, -mul));
|
||||
}
|
||||
else if (a.is_numeral(e, num)) {
|
||||
m_weight += num*mul;
|
||||
}
|
||||
else if (a.is_to_real(e, e1)) {
|
||||
m_terms.push_back(std::make_pair(e1, mul));
|
||||
}
|
||||
else if (!is_uninterp_const(e)) {
|
||||
return non_horn;
|
||||
}
|
||||
else {
|
||||
m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
|
||||
}
|
||||
}
|
||||
unsigned num_negative = 0;
|
||||
unsigned num_positive = 0;
|
||||
bool is_unit_pos = true, is_unit_neg = true;
|
||||
obj_map<expr, rational>::iterator it = m_coeff_map.begin();
|
||||
obj_map<expr, rational>::iterator end = m_coeff_map.end();
|
||||
for (; it != end; ++it) {
|
||||
rational r = it->m_value;
|
||||
if (r.is_zero()) {
|
||||
continue;
|
||||
}
|
||||
m_terms.push_back(std::make_pair(it->m_key, r));
|
||||
if (r.is_pos()) {
|
||||
is_unit_pos = is_unit_pos && r.is_one();
|
||||
num_positive++;
|
||||
}
|
||||
else {
|
||||
is_unit_neg = is_unit_neg && r.is_minus_one();
|
||||
num_negative++;
|
||||
}
|
||||
}
|
||||
if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) {
|
||||
return diff;
|
||||
}
|
||||
if (num_positive <= 1 && is_unit_pos) {
|
||||
return horn;
|
||||
}
|
||||
if (num_negative <= 1 && is_unit_neg) {
|
||||
return co_horn;
|
||||
}
|
||||
return non_horn;
|
||||
}
|
||||
|
||||
|
||||
}
|
|
@ -1,328 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_horn_ineq.h
|
||||
|
||||
Abstract:
|
||||
|
||||
A*x <= weight + D*x, coefficients to A and D are non-negative,
|
||||
D is a diagonal matrix.
|
||||
Coefficients to weight may have both signs.
|
||||
|
||||
Label variables by weight.
|
||||
Select inequality that is not satisfied.
|
||||
Set delta(LHS) := 0
|
||||
Set delta(RHS(x)) := weight(x) - b
|
||||
Propagate weight increment through inequalities.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-04-18
|
||||
|
||||
Revision History:
|
||||
|
||||
The implementaton is derived from theory_diff_logic.
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _THEORY_HORN_INEQ_H_
|
||||
#define _THEORY_HORN_INEQ_H_
|
||||
|
||||
#include"rational.h"
|
||||
#include"inf_rational.h"
|
||||
#include"inf_int_rational.h"
|
||||
#include"inf_eps_rational.h"
|
||||
#include"smt_theory.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
#include"smt_justification.h"
|
||||
#include"map.h"
|
||||
#include"smt_params.h"
|
||||
#include"arith_eq_adapter.h"
|
||||
#include"smt_model_generator.h"
|
||||
#include"numeral_factory.h"
|
||||
#include"smt_clause.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class horn_ineq_tester {
|
||||
ast_manager& m;
|
||||
arith_util a;
|
||||
ptr_vector<expr> m_todo;
|
||||
svector<lbool> m_pols;
|
||||
ast_mark pos_mark, neg_mark;
|
||||
obj_map<expr, rational> m_coeff_map;
|
||||
rational m_weight;
|
||||
vector<std::pair<expr*, rational> > m_terms;
|
||||
|
||||
public:
|
||||
enum classify_t {
|
||||
co_horn,
|
||||
horn,
|
||||
diff,
|
||||
non_horn
|
||||
};
|
||||
horn_ineq_tester(ast_manager& m);
|
||||
|
||||
// test if formula is in the Horn inequality fragment:
|
||||
bool operator()(expr* fml);
|
||||
bool operator()(unsigned num_fmls, expr* const* fmls);
|
||||
|
||||
// linearize inequality/equality
|
||||
classify_t linearize(expr* e);
|
||||
classify_t linearize(expr* e1, expr* e2);
|
||||
|
||||
// retrieve linearization
|
||||
vector<std::pair<expr*,rational> > const& get_linearization() const;
|
||||
rational const& get_weight() const { return m_weight; }
|
||||
private:
|
||||
bool test_expr(lbool p, expr* e);
|
||||
classify_t linearize();
|
||||
};
|
||||
|
||||
template<typename Ext>
|
||||
class theory_horn_ineq : public theory, private Ext {
|
||||
|
||||
typedef typename Ext::numeral numeral;
|
||||
typedef typename Ext::inf_numeral inf_numeral;
|
||||
typedef literal explanation;
|
||||
typedef theory_var th_var;
|
||||
typedef svector<th_var> th_var_vector;
|
||||
typedef unsigned clause_id;
|
||||
typedef vector<std::pair<th_var, rational> > coeffs;
|
||||
|
||||
class clause;
|
||||
class graph;
|
||||
class assignment_trail;
|
||||
class parent_trail;
|
||||
|
||||
class atom {
|
||||
protected:
|
||||
bool_var m_bvar;
|
||||
bool m_true;
|
||||
int m_pos;
|
||||
int m_neg;
|
||||
public:
|
||||
atom(bool_var bv, int pos, int neg) :
|
||||
m_bvar(bv), m_true(false),
|
||||
m_pos(pos), m_neg(neg) {}
|
||||
~atom() {}
|
||||
bool_var get_bool_var() const { return m_bvar; }
|
||||
bool is_true() const { return m_true; }
|
||||
void assign_eh(bool is_true) { m_true = is_true; }
|
||||
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
|
||||
int get_pos() const { return m_pos; }
|
||||
int get_neg() const { return m_neg; }
|
||||
std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const;
|
||||
};
|
||||
typedef svector<atom> atoms;
|
||||
|
||||
struct scope {
|
||||
unsigned m_atoms_lim;
|
||||
unsigned m_asserted_atoms_lim;
|
||||
unsigned m_asserted_qhead_old;
|
||||
};
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_conflicts;
|
||||
unsigned m_num_assertions;
|
||||
unsigned m_num_core2th_eqs;
|
||||
unsigned m_num_core2th_diseqs;
|
||||
|
||||
void reset() {
|
||||
memset(this, 0, sizeof(*this));
|
||||
}
|
||||
|
||||
stats() {
|
||||
reset();
|
||||
}
|
||||
};
|
||||
|
||||
stats m_stats;
|
||||
smt_params m_params;
|
||||
arith_util a;
|
||||
arith_eq_adapter m_arith_eq_adapter;
|
||||
th_var m_zero_int; // cache the variable representing the zero variable.
|
||||
th_var m_zero_real; // cache the variable representing the zero variable.
|
||||
|
||||
graph* m_graph;
|
||||
atoms m_atoms;
|
||||
unsigned_vector m_asserted_atoms; // set of asserted atoms
|
||||
unsigned m_asserted_qhead;
|
||||
u_map<unsigned> m_bool_var2atom;
|
||||
svector<scope> m_scopes;
|
||||
|
||||
double m_agility;
|
||||
bool m_lia;
|
||||
bool m_lra;
|
||||
bool m_non_horn_ineq_exprs;
|
||||
|
||||
horn_ineq_tester m_test;
|
||||
|
||||
|
||||
arith_factory * m_factory;
|
||||
rational m_delta;
|
||||
rational m_lambda;
|
||||
|
||||
|
||||
// Set a conflict due to a negative cycle.
|
||||
void set_neg_cycle_conflict();
|
||||
|
||||
// Create a new theory variable.
|
||||
virtual th_var mk_var(enode* n);
|
||||
|
||||
virtual th_var mk_var(expr* n);
|
||||
|
||||
void compute_delta();
|
||||
|
||||
void found_non_horn_ineq_expr(expr * n);
|
||||
|
||||
bool is_interpreted(app* n) const {
|
||||
return n->get_family_id() == get_family_id();
|
||||
}
|
||||
|
||||
public:
|
||||
theory_horn_ineq(ast_manager& m);
|
||||
|
||||
virtual ~theory_horn_ineq();
|
||||
|
||||
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); }
|
||||
|
||||
virtual char const * get_name() const { return "horn-inequality-logic"; }
|
||||
|
||||
/**
|
||||
\brief See comment in theory::mk_eq_atom
|
||||
*/
|
||||
virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); }
|
||||
|
||||
virtual void init(context * ctx);
|
||||
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
|
||||
virtual bool internalize_term(app * term);
|
||||
|
||||
virtual void internalize_eq_eh(app * atom, bool_var v);
|
||||
|
||||
virtual void assign_eh(bool_var v, bool is_true);
|
||||
|
||||
virtual void new_eq_eh(th_var v1, th_var v2) {
|
||||
m_arith_eq_adapter.new_eq_eh(v1, v2);
|
||||
}
|
||||
|
||||
virtual bool use_diseqs() const { return true; }
|
||||
|
||||
virtual void new_diseq_eh(th_var v1, th_var v2) {
|
||||
m_arith_eq_adapter.new_diseq_eh(v1, v2);
|
||||
}
|
||||
|
||||
virtual void push_scope_eh();
|
||||
|
||||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
|
||||
virtual void restart_eh() {
|
||||
m_arith_eq_adapter.restart_eh();
|
||||
}
|
||||
|
||||
virtual void relevant_eh(app* e) {}
|
||||
|
||||
virtual void init_search_eh() {
|
||||
m_arith_eq_adapter.init_search_eh();
|
||||
}
|
||||
|
||||
virtual final_check_status final_check_eh();
|
||||
|
||||
virtual bool is_shared(th_var v) const {
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual bool can_propagate() {
|
||||
SASSERT(m_asserted_qhead <= m_asserted_atoms.size());
|
||||
return m_asserted_qhead != m_asserted_atoms.size();
|
||||
}
|
||||
|
||||
virtual void propagate();
|
||||
|
||||
virtual justification * why_is_diseq(th_var v1, th_var v2) {
|
||||
UNREACHABLE();
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual void reset_eh();
|
||||
|
||||
virtual void init_model(model_generator & m);
|
||||
|
||||
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
|
||||
|
||||
virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const {
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void display(std::ostream & out) const;
|
||||
|
||||
virtual void collect_statistics(::statistics & st) const;
|
||||
|
||||
private:
|
||||
|
||||
virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
|
||||
m_stats.m_num_core2th_eqs++;
|
||||
new_eq_or_diseq(true, v1, v2, j);
|
||||
}
|
||||
|
||||
virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) {
|
||||
m_stats.m_num_core2th_diseqs++;
|
||||
new_eq_or_diseq(false, v1, v2, j);
|
||||
}
|
||||
|
||||
void negate(coeffs& coeffs, rational& weight);
|
||||
numeral mk_weight(bool is_real, bool is_strict, rational const& w) const;
|
||||
void mk_coeffs(vector<std::pair<expr*,rational> >const& terms, coeffs& coeffs, rational& w);
|
||||
|
||||
void del_atoms(unsigned old_size);
|
||||
|
||||
void propagate_core();
|
||||
|
||||
bool propagate_atom(atom const& a);
|
||||
|
||||
th_var mk_term(app* n);
|
||||
|
||||
th_var mk_num(app* n, rational const& r);
|
||||
|
||||
bool is_consistent() const;
|
||||
|
||||
th_var expand(bool pos, th_var v, rational & k);
|
||||
|
||||
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
|
||||
|
||||
th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
|
||||
|
||||
th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
|
||||
|
||||
void inc_conflicts();
|
||||
|
||||
};
|
||||
|
||||
struct rhi_ext {
|
||||
typedef inf_rational inf_numeral;
|
||||
typedef inf_eps_rational<inf_rational> numeral;
|
||||
numeral m_epsilon;
|
||||
numeral m_minus_infty;
|
||||
rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {}
|
||||
};
|
||||
|
||||
struct ihi_ext {
|
||||
typedef rational inf_numeral;
|
||||
typedef inf_eps_rational<rational> numeral;
|
||||
numeral m_epsilon;
|
||||
numeral m_minus_infty;
|
||||
ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {}
|
||||
};
|
||||
|
||||
typedef theory_horn_ineq<rhi_ext> theory_rhi;
|
||||
typedef theory_horn_ineq<ihi_ext> theory_ihi;
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
#endif /* _THEORY_HORN_INEQ_H_ */
|
File diff suppressed because it is too large
Load diff
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include"bv_decl_plugin.h"
|
||||
#include"expr_replacer.h"
|
||||
#include"extension_model_converter.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
class bv_size_reduction_tactic : public tactic {
|
||||
|
@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
obj_map<app, numeral> m_unsigned_lowers;
|
||||
obj_map<app, numeral> m_unsigned_uppers;
|
||||
ref<bv_size_reduction_mc> m_mc;
|
||||
ref<filter_model_converter> m_fmc;
|
||||
scoped_ptr<expr_replacer> m_replacer;
|
||||
bool m_produce_models;
|
||||
volatile bool m_cancel;
|
||||
|
@ -121,21 +123,41 @@ struct bv_size_reduction_tactic::imp {
|
|||
negated = true;
|
||||
f = to_app(f)->get_arg(0);
|
||||
}
|
||||
|
||||
|
||||
if (m_util.is_bv_sle(f, lhs, rhs)) {
|
||||
bv_sz = m_util.get_bv_size(lhs);
|
||||
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
|
||||
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
|
||||
// v <= k
|
||||
if (negated) update_signed_lower(to_app(lhs), val+numeral(1));
|
||||
val = m_util.norm(val, bv_sz, true);
|
||||
if (negated) {
|
||||
val += numeral(1);
|
||||
if (m_util.norm(val, bv_sz, true) != val) {
|
||||
// bound is infeasible.
|
||||
}
|
||||
else {
|
||||
update_signed_lower(to_app(lhs), val);
|
||||
}
|
||||
}
|
||||
else update_signed_upper(to_app(lhs), val);
|
||||
}
|
||||
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
|
||||
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
|
||||
// k <= v
|
||||
if (negated) update_signed_upper(to_app(rhs), val-numeral(1));
|
||||
val = m_util.norm(val, bv_sz, true);
|
||||
if (negated) {
|
||||
val -= numeral(1);
|
||||
if (m_util.norm(val, bv_sz, true) != val) {
|
||||
// bound is infeasible.
|
||||
}
|
||||
else {
|
||||
update_signed_upper(to_app(lhs), val);
|
||||
}
|
||||
}
|
||||
else update_signed_lower(to_app(rhs), val);
|
||||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
else if (m_util.is_bv_ule(f, lhs, rhs)) {
|
||||
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
|
||||
|
@ -196,6 +218,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
|
||||
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
|
||||
expr * new_def = 0;
|
||||
app * new_const = 0;
|
||||
if (l > u) {
|
||||
g.assert_expr(m.mk_false());
|
||||
return;
|
||||
|
@ -208,15 +231,19 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (l.is_neg()) {
|
||||
unsigned i_nb = (u - l).get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (i_nb < v_nb)
|
||||
new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb)));
|
||||
if (i_nb < v_nb) {
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
|
||||
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// 0 <= l <= v <= u
|
||||
unsigned u_nb = u.get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (u_nb < v_nb)
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
|
||||
if (u_nb < v_nb) {
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -226,6 +253,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (!m_mc)
|
||||
m_mc = alloc(bv_size_reduction_mc, m);
|
||||
m_mc->insert(v->get_decl(), new_def);
|
||||
if (!m_fmc && new_const)
|
||||
m_fmc = alloc(filter_model_converter, m);
|
||||
if (new_const)
|
||||
m_fmc->insert(new_const->get_decl());
|
||||
}
|
||||
num_reduced++;
|
||||
}
|
||||
|
@ -264,6 +295,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
|
||||
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
|
||||
expr * new_def = 0;
|
||||
app * new_const = 0;
|
||||
if (l > u) {
|
||||
g.assert_expr(m.mk_false());
|
||||
return;
|
||||
|
@ -275,8 +307,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
// 0 <= l <= v <= u
|
||||
unsigned u_nb = u.get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (u_nb < v_nb)
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
|
||||
if (u_nb < v_nb) {
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
|
||||
}
|
||||
}
|
||||
|
||||
if (new_def) {
|
||||
|
@ -285,6 +319,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (!m_mc)
|
||||
m_mc = alloc(bv_size_reduction_mc, m);
|
||||
m_mc->insert(v->get_decl(), new_def);
|
||||
if (!m_fmc && new_const)
|
||||
m_fmc = alloc(filter_model_converter, m);
|
||||
if (new_const)
|
||||
m_fmc->insert(new_const->get_decl());
|
||||
}
|
||||
num_reduced++;
|
||||
TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
|
||||
|
@ -309,7 +347,11 @@ struct bv_size_reduction_tactic::imp {
|
|||
g.update(i, new_f);
|
||||
}
|
||||
mc = m_mc.get();
|
||||
if (m_fmc) {
|
||||
mc = concat(m_fmc.get(), mc.get());
|
||||
}
|
||||
m_mc = 0;
|
||||
m_fmc = 0;
|
||||
}
|
||||
report_tactic_progress(":bv-reduced", num_reduced);
|
||||
TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););
|
||||
|
|
|
@ -42,7 +42,7 @@ struct is_non_qffpa_predicate {
|
|||
ast_manager & m;
|
||||
float_util u;
|
||||
|
||||
is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {}
|
||||
is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
|
@ -50,13 +50,15 @@ struct is_non_qffpa_predicate {
|
|||
|
||||
void operator()(app * n) {
|
||||
sort * s = get_sort(n);
|
||||
if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s)))
|
||||
if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s))
|
||||
throw found();
|
||||
family_id fid = s->get_family_id();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == u.get_family_id())
|
||||
return;
|
||||
if (is_uninterp_const(n))
|
||||
return;
|
||||
|
||||
throw found();
|
||||
}
|
||||
|
@ -68,7 +70,7 @@ struct is_non_qffpabv_predicate {
|
|||
bv_util bu;
|
||||
float_util fu;
|
||||
|
||||
is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {}
|
||||
is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {}
|
||||
|
||||
void operator()(var *) { throw found(); }
|
||||
|
||||
|
@ -76,13 +78,15 @@ struct is_non_qffpabv_predicate {
|
|||
|
||||
void operator()(app * n) {
|
||||
sort * s = get_sort(n);
|
||||
if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s)))
|
||||
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s))
|
||||
throw found();
|
||||
family_id fid = s->get_family_id();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == fu.get_family_id() || fid == bu.get_family_id())
|
||||
return;
|
||||
if (is_uninterp_const(n))
|
||||
return;
|
||||
|
||||
throw found();
|
||||
}
|
||||
|
|
|
@ -331,22 +331,13 @@ public:
|
|||
return target;
|
||||
}
|
||||
|
||||
friend inline rational gcd(rational const & r1, rational const & r2) {
|
||||
rational result;
|
||||
m().gcd(r1.m_val, r2.m_val, result.m_val);
|
||||
return result;
|
||||
}
|
||||
friend inline rational gcd(rational const & r1, rational const & r2);
|
||||
|
||||
//
|
||||
// extended Euclid:
|
||||
// r1*a + r2*b = gcd
|
||||
//
|
||||
friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) {
|
||||
rational result;
|
||||
m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
|
||||
return result;
|
||||
}
|
||||
|
||||
friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b);
|
||||
|
||||
friend inline rational lcm(rational const & r1, rational const & r2) {
|
||||
rational result;
|
||||
|
@ -378,11 +369,7 @@ public:
|
|||
return result;
|
||||
}
|
||||
|
||||
friend inline rational abs(rational const & r) {
|
||||
rational result(r);
|
||||
m().abs(result.m_val);
|
||||
return result;
|
||||
}
|
||||
friend inline rational abs(rational const & r);
|
||||
|
||||
rational to_rational() const { return *this; }
|
||||
|
||||
|
@ -446,5 +433,24 @@ inline rational power(rational const & r, unsigned p) {
|
|||
return r.expt(p);
|
||||
}
|
||||
|
||||
inline rational abs(rational const & r) {
|
||||
rational result(r);
|
||||
rational::m().abs(result.m_val);
|
||||
return result;
|
||||
}
|
||||
|
||||
inline rational gcd(rational const & r1, rational const & r2) {
|
||||
rational result;
|
||||
rational::m().gcd(r1.m_val, r2.m_val, result.m_val);
|
||||
return result;
|
||||
}
|
||||
|
||||
inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) {
|
||||
rational result;
|
||||
rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
#endif /* _RATIONAL_H_ */
|
||||
|
||||
|
|
Loading…
Reference in a new issue