mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls

Browse source 
Conflicts:
	src/tactic/sls/sls_engine.cpp
	src/tactic/sls/sls_engine.h
	src/tactic/sls/sls_evaluator.h
	src/tactic/sls/sls_tracker.h
This commit is contained in:
Andreas Froehlich 2014-04-21 17:05:19 +01:00
parent ef1d8f2acc f8ee58b301
commit 5ab65d52a6
53 changed files with 2315 additions and 4466 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
scripts/mk_util.py
View file

@ -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)

5
scripts/update_api.py
View file

@ -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')

4
src/api/api_interp.cpp
View file

@ -39,11 +39,8 @@ Revision History:
#include"iz3pp.h"
#include"iz3checker.h"
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
// WARNING: don't make a hash_map with this if the range type
// has a destructor: you'll get an address dependency!!!
namespace stl_ext {
@ -55,7 +52,6 @@ namespace stl_ext {
}
};
}
#endif
typedef interpolation_options_struct *Z3_interpolation_options;

38
src/api/dotnet/Properties/AssemblyInfo.cs Normal file
View file

@ -0,0 +1,38 @@
using System;
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
using System.Security.Permissions;
// General Information about an assembly is controlled through the following
// set of attributes. Change these attribute values to modify the information
// associated with an assembly.
[assembly: AssemblyTitle("Z3 .NET Interface")]
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
[assembly: AssemblyConfiguration("")]
[assembly: AssemblyCompany("Microsoft Corporation")]
[assembly: AssemblyProduct("Z3")]
[assembly: AssemblyCopyright("Copyright © Microsoft Corporation 2006")]
[assembly: AssemblyTrademark("")]
[assembly: AssemblyCulture("")]
// Setting ComVisible to false makes the types in this assembly not visible
// to COM components. If you need to access a type in this assembly from
// COM, set the ComVisible attribute to true on that type.
[assembly: ComVisible(false)]
// The following GUID is for the ID of the typelib if this project is exposed to COM
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
// Version information for an assembly consists of the following four values:
//
// Major Version
// Minor Version
// Build Number
// Revision
//
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")]
[assembly: AssemblyVersion("4.3.2.0")]
[assembly: AssemblyFileVersion("4.3.2.0")]

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

@ -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`.

28
src/ast/ast_smt2_pp.cpp
View file

@ -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);

7
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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()) {

2
src/cmd_context/check_logic.cpp
View file

@ -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))

19
src/cmd_context/pdecl.cpp
View file

@ -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();

2
src/cmd_context/pdecl.h
View file

@ -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;
};
/**

90
src/duality/duality.h Normal file → Executable file
View file

@ -25,12 +25,12 @@ Revision History:
#include <map>
// make hash_map and hash_set available
#ifndef WIN32
using namespace stl_ext;
#endif
namespace Duality {
class implicant_solver;
/* Generic operations on Z3 formulas */
struct Z3User {
@ -82,6 +82,8 @@ namespace Duality {
Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);
Term CloneQuantAndSimp(const expr &t, const expr &body);
Term RemoveRedundancy(const Term &t);
Term IneqToEq(const Term &t);
@ -102,6 +104,9 @@ namespace Duality {
FuncDecl RenumberPred(const FuncDecl &f, int n);
Term ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming);
protected:
void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
@ -197,6 +202,9 @@ protected:
/** Is this a background constant? */
virtual bool is_constant(const func_decl &f) = 0;
/** Get the constants in the background vocabulary */
virtual hash_set<func_decl> &get_constants() = 0;
/** Assert a background axiom. */
virtual void assert_axiom(const expr &axiom) = 0;
@ -290,6 +298,11 @@ protected:
return bckg.find(f) != bckg.end();
}
/** Get the constants in the background vocabulary */
virtual hash_set<func_decl> &get_constants(){
return bckg;
}
~iZ3LogicSolver(){
// delete ictx;
delete islvr;
@ -600,6 +613,8 @@ protected:
void FixCurrentState(Edge *root);
void FixCurrentStateFull(Edge *edge, const expr &extra);
void FixCurrentStateFull(Edge *edge, const std::vector<expr> &assumps, const hash_map<ast,expr> &renaming);
/** Declare a constant in the background theory. */
@ -731,6 +746,10 @@ protected:
struct bad_format {
};
// thrown on internal error
struct Bad {
};
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void Pop(int num_scopes);
@ -782,7 +801,7 @@ protected:
};
#ifdef WIN32
#ifdef _WINDOWS
__declspec(dllexport)
#endif
void FromClauses(const std::vector<Term> &clauses);
@ -942,10 +961,12 @@ protected:
Term UnderapproxFormula(const Term &f, hash_set<ast> &dont_cares);
void ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
hash_set<ast> &done, hash_set<ast> &dont_cares);
hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional = true);
Term UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares);
public:
Term UnderapproxFullFormula(const Term &f, bool extensional = true);
protected:
Term ToRuleRec(Edge *e, hash_map<ast,Term> &memo, const Term &t, std::vector<expr> &quants);
hash_map<ast,Term> resolve_ite_memo;
@ -986,6 +1007,8 @@ protected:
void AddEdgeToSolver(Edge *edge);
void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge);
void AddToProofCore(hash_set<ast> &core);
void GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under);
@ -1051,13 +1074,40 @@ protected:
public:
struct Counterexample {
class Counterexample {
private:
RPFP *tree;
RPFP::Node *root;
public:
Counterexample(){
tree = 0;
root = 0;
}
Counterexample(RPFP *_tree, RPFP::Node *_root){
tree = _tree;
root = _root;
}
~Counterexample(){
if(tree) delete tree;
}
void swap(Counterexample &other){
std::swap(tree,other.tree);
std::swap(root,other.root);
}
void set(RPFP *_tree, RPFP::Node *_root){
if(tree) delete tree;
tree = _tree;
root = _root;
}
void clear(){
if(tree) delete tree;
tree = 0;
}
RPFP *get_tree() const {return tree;}
RPFP::Node *get_root() const {return root;}
private:
Counterexample &operator=(const Counterexample &);
Counterexample(const Counterexample &);
};
/** Solve the problem. You can optionally give an old
@ -1067,7 +1117,7 @@ protected:
virtual bool Solve() = 0;
virtual Counterexample GetCounterexample() = 0;
virtual Counterexample &GetCounterexample() = 0;
virtual bool SetOption(const std::string &option, const std::string &value) = 0;
@ -1075,7 +1125,7 @@ protected:
is chiefly useful for abstraction refinement, when we want to
solve a series of similar problems. */
virtual void LearnFrom(Counterexample &old_cex) = 0;
virtual void LearnFrom(Solver *old_solver) = 0;
virtual ~Solver(){}
@ -1184,7 +1234,13 @@ namespace Duality {
hash_map<Edge *, Edge *> EdgeCloneMap;
std::vector<expr> alit_stack;
std::vector<unsigned> alit_stack_sizes;
hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
// to let us use one solver per edge
struct edge_solver {
hash_map<ast,expr> AssumptionLits;
uptr<solver> slvr;
};
hash_map<Edge *, edge_solver > edge_solvers;
#ifdef LIMIT_STACK_WEIGHT
struct weight_counter {
@ -1236,19 +1292,23 @@ namespace Duality {
void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
LogicSolver *SolverForEdge(Edge *edge, bool models);
edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms);
public:
struct scoped_solver_for_edge {
LogicSolver *orig_ls;
solver *orig_slvr;
RPFP_caching *rpfp;
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
edge_solver *es;
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
rpfp = _rpfp;
orig_ls = rpfp->ls;
rpfp->ls = rpfp->SolverForEdge(edge,models);
orig_slvr = rpfp->ls->slvr;
es = &(rpfp->SolverForEdge(edge,models,axioms));
rpfp->ls->slvr = es->slvr.get();
rpfp->AssumptionLits.swap(es->AssumptionLits);
}
~scoped_solver_for_edge(){
rpfp->ls = orig_ls;
rpfp->ls->slvr = orig_slvr;
rpfp->AssumptionLits.swap(es->AssumptionLits);
}
};

169
src/duality/duality_hash.h
View file

@ -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

2
src/duality/duality_profiling.cpp
View file

@ -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)

342
src/duality/duality_rpfp.cpp Normal file → Executable file
View file

@ -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
@ -150,8 +146,10 @@ namespace Duality {
}
return 0;
}
if(t.is_quantifier())
return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier
if(t.is_quantifier()){
int nbv = t.get_quantifier_num_bound();
return CountOperatorsRec(memo,t.body()) + 2 * nbv; // count 2 for each quantifier
}
return 0;
}
@ -410,6 +408,33 @@ namespace Duality {
return res;
}
Z3User::Term Z3User::ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming)
{
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
Term &res = bar.first->second;
if(!bar.second) return res;
if (t.is_app()) {
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
for(int i = 0; i < nargs; i++)
args.push_back(ExtractStores(memo, t.arg(i),cnstrs,renaming));
res = f(args.size(),&args[0]);
if(f.get_decl_kind() == Store){
func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort());
expr y = fresh();
expr equ = ctx.make(Equal,y,res);
cnstrs.push_back(equ);
renaming[y] = res;
res = y;
}
}
else res = t;
return res;
}
bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){
if(!(lit.is_quantifier() && IsClosedFormula(lit))){
if(!lit.is_app())
@ -523,6 +548,25 @@ namespace Duality {
return foo;
}
Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
if(t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == And){
int nargs = body.num_args();
std::vector<expr> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = CloneQuantAndSimp(t, body.arg(i));
return ctx.make(And,args);
}
if(!t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == Or){
int nargs = body.num_args();
std::vector<expr> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = CloneQuantAndSimp(t, body.arg(i));
return ctx.make(Or,args);
}
return clone_quantifier(t,body);
}
Z3User::Term Z3User::SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val){
std::pair<ast,Term> foo(t,expr(ctx));
std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
@ -1832,7 +1876,7 @@ namespace Duality {
}
void RPFP::ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
hash_set<ast> &done, hash_set<ast> &dont_cares){
hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional){
if(done.find(f) != done.end())
return; /* already processed */
if(f.is_app()){
@ -1840,7 +1884,7 @@ namespace Duality {
decl_kind k = f.decl().get_decl_kind();
if(k == Implies || k == Iff || k == And || k == Or || k == Not){
for(int i = 0; i < nargs; i++)
ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares);
ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares, extensional);
goto done;
}
}
@ -1848,6 +1892,15 @@ namespace Duality {
if(dont_cares.find(f) == dont_cares.end()){
int b = SubtermTruth(memo,f);
if(b != 0 && b != 1) goto done;
if(f.is_app() && f.decl().get_decl_kind() == Equal && f.arg(0).is_array()){
if(b == 1 && !extensional){
expr x = dualModel.eval(f.arg(0)); expr y = dualModel.eval(f.arg(1));
if(!eq(x,y))
b = 0;
}
if(b == 0)
goto done;
}
expr bv = (b==1) ? f : !f;
lits.push_back(bv);
}
@ -1969,12 +2022,16 @@ namespace Duality {
return conjoin(lits);
}
RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares){
RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, bool extensional){
hash_set<ast> dont_cares;
resolve_ite_memo.clear();
timer_start("UnderapproxFormula");
/* first compute truth values of subterms */
hash_map<ast,int> memo;
hash_set<ast> done;
std::vector<Term> lits;
ImplicantFullRed(memo,f,lits,done,dont_cares);
ImplicantFullRed(memo,f,lits,done,dont_cares, extensional);
timer_stop("UnderapproxFormula");
/* return conjunction of literals */
return conjoin(lits);
}
@ -2519,22 +2576,6 @@ namespace Duality {
ConstrainEdgeLocalized(edge,eu);
}
void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){
hash_set<ast> dont_cares;
resolve_ite_memo.clear();
timer_start("UnderapproxFormula");
Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual;
for(unsigned i = 0; i < edge->constraints.size(); i++)
dual = dual && edge->constraints[i];
// dual = dual && extra;
Term eu = UnderapproxFullFormula(dual,dont_cares);
timer_stop("UnderapproxFormula");
ConstrainEdgeLocalized(edge,eu);
}
void RPFP::GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under){
if(memo[under].find(f) != memo[under].end())
return;
@ -2711,10 +2752,12 @@ namespace Duality {
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
s.add(theory[i]);
if(s.check(lits.size(),&lits[0]) != unsat)
throw "should be unsat";
for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
if(s.check(lits.size(),&lits[0]) == unsat)
goto is_unsat;
throw "should be unsat";
}
is_unsat:
for(unsigned i = 0; i < conjuncts.size(); ){
std::swap(conjuncts[i],conjuncts.back());
std::swap(lits[i],lits.back());
@ -2747,8 +2790,20 @@ namespace Duality {
// verify
check_result res = CheckCore(lits,full_core);
if(res != unsat)
if(res != unsat){
// add the axioms in the off chance they are useful
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
GetAssumptionLits(theory[i],assumps);
lits = assumps;
std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
if((res = CheckCore(lits,full_core)) == unsat)
goto is_unsat;
throw "should be unsat";
}
is_unsat:
FilterCore(core,full_core);
std::vector<expr> dummy;
@ -2803,7 +2858,91 @@ namespace Duality {
return ctx.make(And,lits);
}
// set up edge constraint in aux solver
/* This is a wrapper for a solver that is intended to compute
implicants from models. It works around a problem in Z3 with
models in the non-extensional array theory. It does this by
naming all of the store terms in a formula. That is, (store ...)
is replaced by "name" with an added constraint name = (store
...). This allows us to determine from the model whether an array
equality is true or false (it is false if the two sides are
mapped to different function symbols, even if they have the same
contents).
*/
struct implicant_solver {
RPFP *owner;
solver &aux_solver;
std::vector<expr> assumps, namings;
std::vector<int> assump_stack, naming_stack;
hash_map<ast,expr> renaming, renaming_memo;
void add(const expr &e){
expr t = e;
if(!aux_solver.extensional_array_theory()){
unsigned i = namings.size();
t = owner->ExtractStores(renaming_memo,t,namings,renaming);
for(; i < namings.size(); i++)
aux_solver.add(namings[i]);
}
assumps.push_back(t);
aux_solver.add(t);
}
void push() {
assump_stack.push_back(assumps.size());
naming_stack.push_back(namings.size());
aux_solver.push();
}
// When we pop the solver, we have to re-add any namings that were lost
void pop(int n) {
aux_solver.pop(n);
int new_assumps = assump_stack[assump_stack.size()-n];
int new_namings = naming_stack[naming_stack.size()-n];
for(unsigned i = new_namings; i < namings.size(); i++)
aux_solver.add(namings[i]);
assumps.resize(new_assumps);
namings.resize(new_namings);
assump_stack.resize(assump_stack.size()-1);
naming_stack.resize(naming_stack.size()-1);
}
check_result check() {
return aux_solver.check();
}
model get_model() {
return aux_solver.get_model();
}
expr get_implicant() {
owner->dualModel = aux_solver.get_model();
expr dual = owner->ctx.make(And,assumps);
bool ext = aux_solver.extensional_array_theory();
expr eu = owner->UnderapproxFullFormula(dual,ext);
// if we renamed store terms, we have to undo
if(!ext)
eu = owner->SubstRec(renaming,eu);
return eu;
}
implicant_solver(RPFP *_owner, solver &_aux_solver)
: owner(_owner), aux_solver(_aux_solver)
{}
};
// set up edge constraint in aux solver
void RPFP::AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge){
if(!edge->dual.null())
aux_solver.add(edge->dual);
for(unsigned i = 0; i < edge->constraints.size(); i++){
expr tl = edge->constraints[i];
aux_solver.add(tl);
}
}
void RPFP::AddEdgeToSolver(Edge *edge){
if(!edge->dual.null())
aux_solver.add(edge->dual);
@ -2813,57 +2952,132 @@ namespace Duality {
}
}
static int by_case_counter = 0;
void RPFP::InterpolateByCases(Node *root, Node *node){
timer_start("InterpolateByCases");
bool axioms_added = false;
aux_solver.push();
AddEdgeToSolver(node->Outgoing);
hash_set<ast> axioms_needed;
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
axioms_needed.insert(theory[i]);
implicant_solver is(this,aux_solver);
is.push();
AddEdgeToSolver(is,node->Outgoing);
node->Annotation.SetEmpty();
hash_set<ast> *core = new hash_set<ast>;
core->insert(node->Outgoing->dual);
while(1){
aux_solver.push();
by_case_counter++;
is.push();
expr annot = !GetAnnotation(node);
aux_solver.add(annot);
if(aux_solver.check() == unsat){
aux_solver.pop(1);
is.add(annot);
if(is.check() == unsat){
is.pop(1);
break;
}
dualModel = aux_solver.get_model();
aux_solver.pop(1);
is.pop(1);
Push();
FixCurrentStateFull(node->Outgoing,annot);
ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
check_result foo = Check(root);
if(foo != unsat)
if(foo != unsat){
slvr().print("should_be_unsat.smt2");
throw "should be unsat";
AddToProofCore(*core);
}
std::vector<expr> assumps, axioms_to_add;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++){
(*core).insert(assumps[i]);
if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
axioms_to_add.push_back(assumps[i]);
axioms_needed.erase(assumps[i]);
}
}
// AddToProofCore(*core);
Transformer old_annot = node->Annotation;
SolveSingleNode(root,node);
{
expr itp = GetAnnotation(node);
dualModel = aux_solver.get_model();
dualModel = is.get_model(); // TODO: what does this mean?
std::vector<expr> case_lits;
itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
SetAnnotation(node,itp);
node->Annotation.Formula = node->Annotation.Formula.simplify();
}
for(unsigned i = 0; i < axioms_to_add.size(); i++)
is.add(axioms_to_add[i]);
#define TEST_BAD
#ifdef TEST_BAD
{
static int bad_count = 0, num_bads = 1;
if(bad_count >= num_bads){
bad_count = 0;
num_bads = num_bads * 2;
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
bad_count++;
}
#endif
if(node->Annotation.IsEmpty()){
if(!axioms_added){
// add the axioms in the off chance they are useful
const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++)
aux_solver.add(theory[i]);
is.add(theory[i]);
axioms_added = true;
}
else {
#ifdef KILL_ON_BAD_INTERPOLANT
std::cout << "bad in InterpolateByCase -- core:\n";
#if 0
std::vector<expr> assumps;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++)
assumps[i].show();
#endif
std::cout << "checking for inconsistency\n";
std::cout << "model:\n";
is.get_model().show();
expr impl = is.get_implicant();
std::vector<expr> conjuncts;
CollectConjuncts(impl,conjuncts,true);
std::cout << "impl:\n";
for(unsigned i = 0; i < conjuncts.size(); i++)
conjuncts[i].show();
std::cout << "annot:\n";
annot.show();
is.add(annot);
for(unsigned i = 0; i < conjuncts.size(); i++)
is.add(conjuncts[i]);
if(is.check() == unsat){
std::cout << "inconsistent!\n";
std::vector<expr> is_assumps;
is.aux_solver.get_proof().get_assumptions(is_assumps);
std::cout << "core:\n";
for(unsigned i = 0; i < is_assumps.size(); i++)
is_assumps[i].show();
}
else {
std::cout << "consistent!\n";
is.aux_solver.print("should_be_inconsistent.smt2");
}
std::cout << "by_case_counter = " << by_case_counter << "\n";
throw "ack!";
#endif
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
}
Pop(1);
@ -2872,7 +3086,8 @@ namespace Duality {
if(proof_core)
delete proof_core; // shouldn't happen
proof_core = core;
aux_solver.pop(1);
is.pop(1);
timer_stop("InterpolateByCases");
}
void RPFP::Generalize(Node *root, Node *node){
@ -2889,13 +3104,20 @@ namespace Duality {
timer_stop("Generalize");
}
RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){
uptr<LogicSolver> &p = edge_solvers[edge];
RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){
edge_solver &es = edge_solvers[edge];
uptr<solver> &p = es.slvr;
if(!p.get()){
scoped_no_proof no_proofs_please(ctx.m()); // no proofs
p.set(new iZ3LogicSolver(ctx,models)); // no models
p.set(new solver(ctx,true,models)); // no models
if(axioms){
RPFP::LogicSolver *ls = edge->owner->ls;
const std::vector<expr> &axs = ls->get_axioms();
for(unsigned i = 0; i < axs.size(); i++)
p.get()->add(axs[i]);
}
}
return p.get();
return es;
}
@ -3166,7 +3388,7 @@ namespace Duality {
func_decl f = t.decl();
std::vector<Term> args;
int nargs = t.num_args();
if(nargs == 0)
if(nargs == 0 && f.get_decl_kind() == Uninterpreted)
ls->declare_constant(f); // keep track of background constants
for(int i = 0; i < nargs; i++)
args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
@ -3362,6 +3584,8 @@ namespace Duality {
}
}
bool some_labels = false;
// create the edges
for(unsigned i = 0; i < clauses.size(); i++){
@ -3397,17 +3621,23 @@ namespace Duality {
Term labeled = body;
std::vector<label_struct > lbls; // TODO: throw this away for now
body = RemoveLabels(body,lbls);
if(!eq(labeled,body))
some_labels = true; // remember if there are labels, as we then can't do qe_lite
// body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this.
body = body.simplify();
#ifdef USE_QE_LITE
std::set<int> idxs;
for(unsigned j = 0; j < Indparams.size(); j++)
if(Indparams[j].is_var())
idxs.insert(Indparams[j].get_index_value());
body = body.qe_lite(idxs,false);
if(!some_labels){ // can't do qe_lite if we have to reconstruct labels
for(unsigned j = 0; j < Indparams.size(); j++)
if(Indparams[j].is_var())
idxs.insert(Indparams[j].get_index_value());
body = body.qe_lite(idxs,false);
}
hash_map<int,hash_map<ast,Term> > sb_memo;
body = SubstBoundRec(sb_memo,substs[i],0,body);
if(some_labels)
labeled = SubstBoundRec(sb_memo,substs[i],0,labeled);
for(unsigned j = 0; j < Indparams.size(); j++)
Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
#endif

566
src/duality/duality_solver.cpp Normal file → Executable file
View file

@ -19,7 +19,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -51,12 +51,18 @@ Revision History:
// #define TOP_DOWN
// #define EFFORT_BOUNDED_STRAT
#define SKIP_UNDERAPPROX_NODES
#define USE_RPFP_CLONE
// #define KEEP_EXPANSIONS
// #define USE_CACHING_RPFP
// #define PROPAGATE_BEFORE_CHECK
#define NEW_STRATIFIED_INLINING
#define USE_RPFP_CLONE
#define USE_NEW_GEN_CANDS
//#define NO_PROPAGATE
//#define NO_GENERALIZE
//#define NO_DECISIONS
namespace Duality {
// TODO: must be a better place for this...
@ -77,7 +83,7 @@ namespace Duality {
rpfp = _rpfp;
}
virtual void Extend(RPFP::Node *node){}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){}
virtual void Bound(RPFP::Node *node){}
virtual void Expand(RPFP::Edge *edge){}
virtual void AddCover(RPFP::Node *covered, std::vector<RPFP::Node *> &covering){}
@ -89,6 +95,7 @@ namespace Duality {
virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Reject(RPFP::Edge *edge, const std::vector<RPFP::Node *> &Children){}
virtual void Message(const std::string &msg){}
virtual void Depth(int){}
virtual ~Reporter(){}
};
@ -119,6 +126,7 @@ namespace Duality {
rpfp = _rpfp;
reporter = 0;
heuristic = 0;
unwinding = 0;
FullExpand = false;
NoConj = false;
FeasibleEdges = true;
@ -126,16 +134,15 @@ namespace Duality {
Report = false;
StratifiedInlining = false;
RecursionBound = -1;
BatchExpand = false;
{
scoped_no_proof no_proofs_please(ctx.m());
#ifdef USE_RPFP_CLONE
clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one
clone_rpfp = new RPFP_caching(clone_ls);
clone_rpfp = new RPFP_caching(rpfp->ls);
clone_rpfp->Clone(rpfp);
#endif
#ifdef USE_NEW_GEN_CANDS
gen_cands_ls = new RPFP::iZ3LogicSolver(ctx);
gen_cands_rpfp = new RPFP_caching(gen_cands_ls);
gen_cands_rpfp = new RPFP_caching(rpfp->ls);
gen_cands_rpfp->Clone(rpfp);
#endif
}
@ -144,20 +151,17 @@ namespace Duality {
~Duality(){
#ifdef USE_RPFP_CLONE
delete clone_rpfp;
delete clone_ls;
#endif
#ifdef USE_NEW_GEN_CANDS
delete gen_cands_rpfp;
delete gen_cands_ls;
#endif
if(unwinding) delete unwinding;
}
#ifdef USE_RPFP_CLONE
RPFP::LogicSolver *clone_ls;
RPFP_caching *clone_rpfp;
#endif
#ifdef USE_NEW_GEN_CANDS
RPFP::LogicSolver *gen_cands_ls;
RPFP_caching *gen_cands_rpfp;
#endif
@ -250,6 +254,19 @@ namespace Duality {
virtual void Done() {}
};
/** The Proposer class proposes conjectures eagerly. These can come
from any source, including predicate abstraction, templates, or
previous solver runs. The proposed conjectures are checked
with low effort when the unwinding is expanded.
*/
class Proposer {
public:
/** Given a node in the unwinding, propose some conjectures */
virtual std::vector<RPFP::Transformer> &Propose(Node *node) = 0;
virtual ~Proposer(){};
};
class Covering; // see below
@ -279,6 +296,7 @@ namespace Duality {
hash_map<Node *, Node *> underapprox_map; // maps underapprox nodes to the nodes they approximate
int last_decisions;
hash_set<Node *> overapproxes;
std::vector<Proposer *> proposers;
#ifdef BOUNDED
struct Counter {
@ -293,24 +311,22 @@ namespace Duality {
virtual bool Solve(){
reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
#ifndef LOCALIZE_CONJECTURES
heuristic = !cex.tree ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
#else
heuristic = !cex.tree ? (Heuristic *)(new LocalHeuristic(rpfp))
heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp))
: (Heuristic *)(new ReplayHeuristic(rpfp,cex));
#endif
cex.tree = 0; // heuristic now owns it
cex.clear(); // in case we didn't use it for heuristic
if(unwinding) delete unwinding;
unwinding = new RPFP(rpfp->ls);
unwinding->HornClauses = rpfp->HornClauses;
indset = new Covering(this);
last_decisions = 0;
CreateEdgesByChildMap();
CreateLeaves();
#ifndef TOP_DOWN
if(!StratifiedInlining){
if(FeasibleEdges)NullaryCandidates();
else InstantiateAllEdges();
}
CreateInitialUnwinding();
#else
CreateLeaves();
for(unsigned i = 0; i < leaves.size(); i++)
if(!SatisfyUpperBound(leaves[i]))
return false;
@ -322,11 +338,29 @@ namespace Duality {
// print_profile(std::cout);
delete indset;
delete heuristic;
delete unwinding;
// delete unwinding; // keep the unwinding for future mining of predicates
delete reporter;
for(unsigned i = 0; i < proposers.size(); i++)
delete proposers[i];
return res;
}
void CreateInitialUnwinding(){
if(!StratifiedInlining){
CreateLeaves();
if(FeasibleEdges)NullaryCandidates();
else InstantiateAllEdges();
}
else {
#ifdef NEW_STRATIFIED_INLINING
#else
CreateLeaves();
#endif
}
}
void Cancel(){
// TODO
}
@ -347,15 +381,19 @@ namespace Duality {
}
#endif
virtual void LearnFrom(Counterexample &old_cex){
cex = old_cex;
virtual void LearnFrom(Solver *other_solver){
// get the counterexample as a guide
cex.swap(other_solver->GetCounterexample());
// propose conjectures based on old unwinding
Duality *old_duality = dynamic_cast<Duality *>(other_solver);
if(old_duality)
proposers.push_back(new HistoryProposer(old_duality,this));
}
/** Return the counterexample */
virtual Counterexample GetCounterexample(){
Counterexample res = cex;
cex.tree = 0; // Cex now belongs to caller
return res;
/** Return a reference to the counterexample */
virtual Counterexample &GetCounterexample(){
return cex;
}
// options
@ -366,6 +404,7 @@ namespace Duality {
bool Report; // spew on stdout
bool StratifiedInlining; // Do stratified inlining as preprocessing step
int RecursionBound; // Recursion bound for bounded verification
bool BatchExpand;
bool SetBoolOption(bool &opt, const std::string &value){
if(value == "0") {
@ -404,6 +443,9 @@ namespace Duality {
if(option == "stratified_inlining"){
return SetBoolOption(StratifiedInlining,value);
}
if(option == "batch_expand"){
return SetBoolOption(BatchExpand,value);
}
if(option == "recursion_bound"){
return SetIntOption(RecursionBound,value);
}
@ -515,7 +557,11 @@ namespace Duality {
c.Children.resize(edge->Children.size());
for(unsigned j = 0; j < c.Children.size(); j++)
c.Children[j] = leaf_map[edge->Children[j]];
Extend(c);
Node *new_node;
Extend(c,new_node);
#ifdef EARLY_EXPAND
TryExpandNode(new_node);
#endif
}
for(Unexpanded::iterator it = unexpanded.begin(), en = unexpanded.end(); it != en; ++it)
indset->Add(*it);
@ -767,16 +813,14 @@ namespace Duality {
}
/* For stratified inlining, we need a topological sort of the
nodes. */
hash_map<Node *, int> TopoSort;
int TopoSortCounter;
std::vector<Edge *> SortedEdges;
void DoTopoSortRec(Node *node){
if(TopoSort.find(node) != TopoSort.end())
return;
TopoSort[node] = TopoSortCounter++; // just to break cycles
TopoSort[node] = INT_MAX; // just to break cycles
Edge *edge = node->Outgoing; // note, this is just *one* outgoing edge
if(edge){
std::vector<Node *> &chs = edge->Children;
@ -784,22 +828,81 @@ namespace Duality {
DoTopoSortRec(chs[i]);
}
TopoSort[node] = TopoSortCounter++;
SortedEdges.push_back(edge);
}
void DoTopoSort(){
TopoSort.clear();
SortedEdges.clear();
TopoSortCounter = 0;
for(unsigned i = 0; i < nodes.size(); i++)
DoTopoSortRec(nodes[i]);
}
int StratifiedLeafCount;
#ifdef NEW_STRATIFIED_INLINING
/** Stratified inlining builds an initial layered unwinding before
switching to the LAWI strategy. Currently the number of layers
is one. Only nodes that are the targets of back edges are
consider to be leaves. This assumes we have already computed a
topological sort.
*/
bool DoStratifiedInlining(){
DoTopoSort();
int depth = 1; // TODO: make this an option
std::vector<hash_map<Node *,Node *> > unfolding_levels(depth+1);
for(int level = 1; level <= depth; level++)
for(unsigned i = 0; i < SortedEdges.size(); i++){
Edge *edge = SortedEdges[i];
Node *parent = edge->Parent;
std::vector<Node *> &chs = edge->Children;
std::vector<Node *> my_chs(chs.size());
for(unsigned j = 0; j < chs.size(); j++){
Node *child = chs[j];
int ch_level = TopoSort[child] >= TopoSort[parent] ? level-1 : level;
if(unfolding_levels[ch_level].find(child) == unfolding_levels[ch_level].end()){
if(ch_level == 0)
unfolding_levels[0][child] = CreateLeaf(child);
else
throw InternalError("in levelized unwinding");
}
my_chs[j] = unfolding_levels[ch_level][child];
}
Candidate cand; cand.edge = edge; cand.Children = my_chs;
Node *new_node;
bool ok = Extend(cand,new_node);
MarkExpanded(new_node); // we don't expand here -- just mark it done
if(!ok) return false; // got a counterexample
unfolding_levels[level][parent] = new_node;
}
return true;
}
Node *CreateLeaf(Node *node){
RPFP::Node *nchild = CreateNodeInstance(node);
MakeLeaf(nchild, /* do_not_expand = */ true);
nchild->Annotation.SetEmpty();
return nchild;
}
void MarkExpanded(Node *node){
if(unexpanded.find(node) != unexpanded.end()){
unexpanded.erase(node);
insts_of_node[node->map].push_back(node);
}
}
#else
/** In stratified inlining, we build the unwinding from the bottom
down, trying to satisfy the node bounds. We do this as a pre-pass,
limiting the expansion. If we get a counterexample, we are done,
else we continue as usual expanding the unwinding upward.
*/
int StratifiedLeafCount;
bool DoStratifiedInlining(){
timer_start("StratifiedInlining");
@ -822,6 +925,8 @@ namespace Duality {
return true;
}
#endif
/** Here, we do the downward expansion for stratified inlining */
hash_map<Node *, Node *> LeafMap, StratifiedLeafMap;
@ -908,9 +1013,14 @@ namespace Duality {
}
Candidate cand = candidates.front();
candidates.pop_front();
if(CandidateFeasible(cand))
if(!Extend(cand))
if(CandidateFeasible(cand)){
Node *new_node;
if(!Extend(cand,new_node))
return false;
#ifdef EARLY_EXPAND
TryExpandNode(new_node);
#endif
}
}
}
@ -930,9 +1040,9 @@ namespace Duality {
Node *CreateUnderapproxNode(Node *node){
// cex.tree->ComputeUnderapprox(cex.root,0);
// cex.get_tree()->ComputeUnderapprox(cex.get_root(),0);
RPFP::Node *under_node = CreateNodeInstance(node->map /* ,StratifiedLeafCount-- */);
under_node->Annotation.IntersectWith(cex.root->Underapprox);
under_node->Annotation.IntersectWith(cex.get_root()->Underapprox);
AddThing(under_node->Annotation.Formula);
Edge *e = unwinding->CreateLowerBoundEdge(under_node);
under_node->Annotation.SetFull(); // allow this node to cover others
@ -968,9 +1078,8 @@ namespace Duality {
ExpandNodeFromCoverFail(node);
}
#endif
if(_cex) *_cex = cex;
else delete cex.tree; // delete the cex if not required
cex.tree = 0;
if(_cex) (*_cex).swap(cex); // return the cex if asked
cex.clear(); // throw away the useless cex
node->Bound = save; // put back original bound
timer_stop("ProveConjecture");
return false;
@ -1255,7 +1364,7 @@ namespace Duality {
slvr.pop(1);
delete checker;
#else
RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
gen_cands_rpfp->Push();
Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
if(gen_cands_rpfp->Check(root) != unsat){
@ -1350,16 +1459,20 @@ namespace Duality {
}
}
bool UpdateNodeToNode(Node *node, Node *top){
if(!node->Annotation.SubsetEq(top->Annotation)){
reporter->Update(node,top->Annotation);
indset->Update(node,top->Annotation);
bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){
if(!node->Annotation.SubsetEq(fact)){
reporter->Update(node,fact,eager);
indset->Update(node,fact);
updated_nodes.insert(node->map);
node->Annotation.IntersectWith(top->Annotation);
node->Annotation.IntersectWith(fact);
return true;
}
return false;
}
bool UpdateNodeToNode(Node *node, Node *top){
return Update(node,top->Annotation);
}
/** Update the unwinding solution, using an interpolant for the
derivation tree. */
@ -1401,8 +1514,7 @@ namespace Duality {
// std::cout << "decisions: " << (end_decs - start_decs) << std::endl;
last_decisions = end_decs - start_decs;
if(res){
cex.tree = dt.tree;
cex.root = dt.top;
cex.set(dt.tree,dt.top); // note tree is now owned by cex
if(UseUnderapprox){
UpdateWithCounterexample(node,dt.tree,dt.top);
}
@ -1414,6 +1526,64 @@ namespace Duality {
delete dtp;
return !res;
}
/* For a given nod in the unwinding, get conjectures from the
proposers and check them locally. Update the node with any true
conjectures.
*/
void DoEagerDeduction(Node *node){
for(unsigned i = 0; i < proposers.size(); i++){
const std::vector<RPFP::Transformer> &conjectures = proposers[i]->Propose(node);
for(unsigned j = 0; j < conjectures.size(); j++){
const RPFP::Transformer &conjecture = conjectures[j];
RPFP::Transformer bound(conjecture);
std::vector<expr> conj_vec;
unwinding->CollectConjuncts(bound.Formula,conj_vec);
for(unsigned k = 0; k < conj_vec.size(); k++){
bound.Formula = conj_vec[k];
if(CheckEdgeCaching(node->Outgoing,bound) == unsat)
Update(node,bound, /* eager = */ true);
//else
//std::cout << "conjecture failed\n";
}
}
}
}
check_result CheckEdge(RPFP *checker, Edge *edge){
Node *root = edge->Parent;
checker->Push();
checker->AssertNode(root);
checker->AssertEdge(edge,1,true);
check_result res = checker->Check(root);
checker->Pop(1);
return res;
}
check_result CheckEdgeCaching(Edge *unwinding_edge, const RPFP::Transformer &bound){
// use a dedicated solver for this edge
// TODO: can this mess be hidden somehow?
RPFP_caching *checker = gen_cands_rpfp; // TODO: a good choice?
Edge *edge = unwinding_edge->map; // get the edge in the original RPFP
RPFP_caching::scoped_solver_for_edge ssfe(checker,edge,true /* models */, true /*axioms*/);
Edge *checker_edge = checker->GetEdgeClone(edge);
// copy the annotations and bound to the clone
Node *root = checker_edge->Parent;
root->Bound = bound;
for(unsigned j = 0; j < checker_edge->Children.size(); j++){
Node *oc = unwinding_edge->Children[j];
Node *nc = checker_edge->Children[j];
nc->Annotation = oc->Annotation;
}
return CheckEdge(checker,checker_edge);
}
/* If the counterexample derivation is partial due to
use of underapproximations, complete it. */
@ -1422,10 +1592,7 @@ namespace Duality {
DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand);
bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree
if(!res) throw "Duality internal error in BuildFullCex";
if(cex.tree)
delete cex.tree;
cex.tree = dt.tree;
cex.root = dt.top;
cex.set(dt.tree,dt.top);
}
void UpdateBackEdges(Node *node){
@ -1448,25 +1615,23 @@ namespace Duality {
}
/** Extend the unwinding, keeping it solved. */
bool Extend(Candidate &cand){
bool Extend(Candidate &cand, Node *&node){
timer_start("Extend");
Node *node = CreateNodeInstance(cand.edge->Parent);
node = CreateNodeInstance(cand.edge->Parent);
CreateEdgeInstance(cand.edge,node,cand.Children);
UpdateBackEdges(node);
reporter->Extend(node);
bool res = SatisfyUpperBound(node);
DoEagerDeduction(node); // first be eager...
bool res = SatisfyUpperBound(node); // then be lazy
if(res) indset->CloseDescendants(node);
else {
#ifdef UNDERAPPROX_NODES
ExpandUnderapproxNodes(cex.tree, cex.root);
ExpandUnderapproxNodes(cex.get_tree(), cex.get_root());
#endif
if(UseUnderapprox) BuildFullCex(node);
timer_stop("Extend");
return res;
}
#ifdef EARLY_EXPAND
TryExpandNode(node);
#endif
timer_stop("Extend");
return res;
}
@ -1564,6 +1729,8 @@ namespace Duality {
class DerivationTree {
public:
virtual ~DerivationTree(){}
DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand)
: slvr(rpfp->slvr()),
ctx(rpfp->ctx)
@ -1913,10 +2080,28 @@ namespace Duality {
stack.push_back(stack_entry());
}
struct DoRestart {};
virtual bool Build(){
while (true) {
try {
return BuildMain();
}
catch (const DoRestart &) {
// clear the statck and try again
updated_nodes.clear();
while(stack.size() > 1)
PopLevel();
reporter->Message("restarted");
}
}
}
bool BuildMain(){
stack.back().level = tree->slvr().get_scope_level();
bool was_sat = true;
int update_failures = 0;
while (true)
{
@ -1925,6 +2110,7 @@ namespace Duality {
unsigned slvr_level = tree->slvr().get_scope_level();
if(slvr_level != stack.back().level)
throw "stacks out of sync!";
reporter->Depth(stack.size());
// res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
check_result foo = tree->Check(top);
@ -1940,51 +2126,47 @@ namespace Duality {
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
tree->SolveSingleNode(top,node);
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
try {
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
}
catch(const RPFP::Bad &){
// bad interpolants can get us here
throw DoRestart();
}
#endif
if(RecordUpdate(node))
update_count++;
else
heuristic->Update(node->map); // make it less likely to expand this node in future
}
if(update_count == 0){
if(was_sat)
throw Incompleteness();
if(was_sat){
update_failures++;
if(update_failures > 10)
throw Incompleteness();
}
reporter->Message("backtracked without learning");
}
else update_failures = 0;
}
tree->ComputeProofCore(); // need to compute the proof core before popping solver
bool propagated = false;
while(1) {
std::vector<Node *> &expansions = stack.back().expansions;
bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
PopLevel();
if(stack.size() == 1)break;
if(prev_level_used){
Node *node = stack.back().expansions[0];
#ifndef NO_PROPAGATE
if(!Propagate(node)) break;
#endif
if(!RecordUpdate(node)) break; // shouldn't happen!
RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
propagated = true;
@ -2008,18 +2190,26 @@ namespace Duality {
was_sat = true;
tree->Push();
std::vector<Node *> &expansions = stack.back().expansions;
#ifndef NO_DECISIONS
for(unsigned i = 0; i < expansions.size(); i++){
tree->FixCurrentState(expansions[i]->Outgoing);
}
#endif
#if 0
if(tree->slvr().check() == unsat)
throw "help!";
#endif
stack.push_back(stack_entry());
stack.back().level = tree->slvr().get_scope_level();
if(ExpandSomeNodes(false,1)){
continue;
int expand_max = 1;
if(0&&duality->BatchExpand){
int thing = stack.size() * 0.1;
expand_max = std::max(1,thing);
if(expand_max > 1)
std::cout << "foo!\n";
}
if(ExpandSomeNodes(false,expand_max))
continue;
tree->Pop(1);
while(stack.size() > 1){
tree->Pop(1);
stack.pop_back();
@ -2029,6 +2219,30 @@ namespace Duality {
}
}
void PopLevel(){
std::vector<Node *> &expansions = stack.back().expansions;
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
}
bool NodeTooComplicated(Node *node){
int ops = tree->CountOperators(node->Annotation.Formula);
if(ops > 10) return true;
@ -2040,7 +2254,13 @@ namespace Duality {
// have to destroy the old proof to get a new interpolant
timer_start("SimplifyNode");
tree->PopPush();
tree->InterpolateByCases(top,node);
try {
tree->InterpolateByCases(top,node);
}
catch(const RPFP::Bad&){
timer_stop("SimplifyNode");
throw RPFP::Bad();
}
timer_stop("SimplifyNode");
}
@ -2078,6 +2298,8 @@ namespace Duality {
std::list<Node *> updated_nodes;
virtual void ExpandNode(RPFP::Node *p){
stack.push_back(stack_entry());
stack.back().level = tree->slvr().get_scope_level();
stack.back().expansions.push_back(p);
DerivationTree::ExpandNode(p);
std::vector<Node *> &new_nodes = p->Outgoing->Children;
@ -2435,7 +2657,7 @@ namespace Duality {
}
bool ContainsCex(Node *node, Counterexample &cex){
expr val = cex.tree->Eval(cex.root->Outgoing,node->Annotation.Formula);
expr val = cex.get_tree()->Eval(cex.get_root()->Outgoing,node->Annotation.Formula);
return eq(val,parent->ctx.bool_val(true));
}
@ -2454,15 +2676,15 @@ namespace Duality {
Node *other = insts[i];
if(CouldCover(node,other)){
reporter()->Forcing(node,other);
if(cex.tree && !ContainsCex(other,cex))
if(cex.get_tree() && !ContainsCex(other,cex))
continue;
if(cex.tree) {delete cex.tree; cex.tree = 0;}
cex.clear();
if(parent->ProveConjecture(node,other->Annotation,other,&cex))
if(CloseDescendants(node))
return true;
}
}
if(cex.tree) {delete cex.tree; cex.tree = 0;}
cex.clear();
return false;
}
#else
@ -2561,13 +2783,12 @@ namespace Duality {
Counterexample old_cex;
public:
ReplayHeuristic(RPFP *_rpfp, Counterexample &_old_cex)
: Heuristic(_rpfp), old_cex(_old_cex)
: Heuristic(_rpfp)
{
old_cex.swap(_old_cex); // take ownership from caller
}
~ReplayHeuristic(){
if(old_cex.tree)
delete old_cex.tree;
}
// Maps nodes of derivation tree into old cex
@ -2575,9 +2796,7 @@ namespace Duality {
void Done() {
cex_map.clear();
if(old_cex.tree)
delete old_cex.tree;
old_cex.tree = 0; // only replay once!
old_cex.clear();
}
void ShowNodeAndChildren(Node *n){
@ -2599,7 +2818,7 @@ namespace Duality {
}
virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
if(!high_priority || !old_cex.tree){
if(!high_priority || !old_cex.get_tree()){
Heuristic::ChooseExpand(choices,best,false);
return;
}
@ -2608,7 +2827,7 @@ namespace Duality {
for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
Node *node = (*it);
if(cex_map.empty())
cex_map[node] = old_cex.root; // match the root nodes
cex_map[node] = old_cex.get_root(); // match the root nodes
if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node
Node *parent = node->Incoming[0]->Parent; // assumes we are a tree!
if(cex_map.find(parent) == cex_map.end())
@ -2634,7 +2853,7 @@ namespace Duality {
Node *old_node = cex_map[node];
if(!old_node)
unmatched.insert(node);
else if(old_cex.tree->Empty(old_node))
else if(old_cex.get_tree()->Empty(old_node))
unmatched.insert(node);
else
matched.insert(node);
@ -2708,7 +2927,120 @@ namespace Duality {
}
};
/** This proposer class generates conjectures based on the
unwinding generated by a previous solver. The assumption is
that the provious solver was working on a different
abstraction of the same system. The trick is to adapt the
annotations in the old unwinding to the new predicates. We
start by generating a map from predicates and parameters in
the old problem to the new.
HACK: mapping is done by cheesy name comparison.
*/
class HistoryProposer : public Proposer
{
Duality *old_solver;
Duality *new_solver;
hash_map<Node *, std::vector<RPFP::Transformer> > conjectures;
public:
/** Construct a history solver. */
HistoryProposer(Duality *_old_solver, Duality *_new_solver)
: old_solver(_old_solver), new_solver(_new_solver) {
// tricky: names in the axioms may have changed -- map them
hash_set<func_decl> &old_constants = old_solver->unwinding->ls->get_constants();
hash_set<func_decl> &new_constants = new_solver->rpfp->ls->get_constants();
hash_map<std::string,func_decl> cmap;
for(hash_set<func_decl>::iterator it = new_constants.begin(), en = new_constants.end(); it != en; ++it)
cmap[GetKey(*it)] = *it;
hash_map<func_decl,func_decl> bckg_map;
for(hash_set<func_decl>::iterator it = old_constants.begin(), en = old_constants.end(); it != en; ++it){
func_decl f = new_solver->ctx.translate(*it); // move to new context
if(cmap.find(GetKey(f)) != cmap.end())
bckg_map[f] = cmap[GetKey(f)];
// else
// std::cout << "constant not matched\n";
}
RPFP *old_unwinding = old_solver->unwinding;
hash_map<std::string, std::vector<Node *> > pred_match;
// index all the predicates in the old unwinding
for(unsigned i = 0; i < old_unwinding->nodes.size(); i++){
Node *node = old_unwinding->nodes[i];
std::string key = GetKey(node);
pred_match[key].push_back(node);
}
// match with predicates in the new RPFP
RPFP *rpfp = new_solver->rpfp;
for(unsigned i = 0; i < rpfp->nodes.size(); i++){
Node *node = rpfp->nodes[i];
std::string key = GetKey(node);
std::vector<Node *> &matches = pred_match[key];
for(unsigned j = 0; j < matches.size(); j++)
MatchNodes(node,matches[j],bckg_map);
}
}
virtual std::vector<RPFP::Transformer> &Propose(Node *node){
return conjectures[node->map];
}
virtual ~HistoryProposer(){
};
private:
void MatchNodes(Node *new_node, Node *old_node, hash_map<func_decl,func_decl> &bckg_map){
if(old_node->Annotation.IsFull())
return; // don't conjecture true!
hash_map<std::string, expr> var_match;
std::vector<expr> &new_params = new_node->Annotation.IndParams;
// Index the new parameters by their keys
for(unsigned i = 0; i < new_params.size(); i++)
var_match[GetKey(new_params[i])] = new_params[i];
RPFP::Transformer &old = old_node->Annotation;
std::vector<expr> from_params = old.IndParams;
for(unsigned j = 0; j < from_params.size(); j++)
from_params[j] = new_solver->ctx.translate(from_params[j]); // get in new context
std::vector<expr> to_params = from_params;
for(unsigned j = 0; j < to_params.size(); j++){
std::string key = GetKey(to_params[j]);
if(var_match.find(key) == var_match.end()){
// std::cout << "unmatched parameter!\n";
return;
}
to_params[j] = var_match[key];
}
expr fmla = new_solver->ctx.translate(old.Formula); // get in new context
fmla = new_solver->rpfp->SubstParams(old.IndParams,to_params,fmla); // substitute parameters
hash_map<ast,expr> memo;
fmla = new_solver->rpfp->SubstRec(memo,bckg_map,fmla); // substitute background constants
RPFP::Transformer new_annot = new_node->Annotation;
new_annot.Formula = fmla;
conjectures[new_node].push_back(new_annot);
}
// We match names by removing suffixes beginning with double at sign
std::string GetKey(Node *node){
return GetKey(node->Name);
}
std::string GetKey(const expr &var){
return GetKey(var.decl());
}
std::string GetKey(const func_decl &f){
std::string name = f.name().str();
int idx = name.find("@@");
if(idx >= 0)
name.erase(idx);
return name;
}
};
};
@ -2716,8 +3048,9 @@ namespace Duality {
std::ostream &s;
public:
StreamReporter(RPFP *_rpfp, std::ostream &_s)
: Reporter(_rpfp), s(_s) {event = 0;}
: Reporter(_rpfp), s(_s) {event = 0; depth = -1;}
int event;
int depth;
void ev(){
s << "[" << event++ << "]" ;
}
@ -2728,23 +3061,30 @@ namespace Duality {
s << " " << rps[i]->number;
s << std::endl;
}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){
ev(); s << "update " << node->number << " " << node->Name.name() << ": ";
rpfp->Summarize(update.Formula);
std::cout << std::endl;
if(depth > 0) s << " (depth=" << depth << ")";
if(eager) s << " (eager)";
s << std::endl;
}
virtual void Bound(RPFP::Node *node){
ev(); s << "check " << node->number << std::endl;
}
virtual void Expand(RPFP::Edge *edge){
RPFP::Node *node = edge->Parent;
ev(); s << "expand " << node->map->number << " " << node->Name.name() << std::endl;
ev(); s << "expand " << node->map->number << " " << node->Name.name();
if(depth > 0) s << " (depth=" << depth << ")";
s << std::endl;
}
virtual void Depth(int d){
depth = d;
}
virtual void AddCover(RPFP::Node *covered, std::vector<RPFP::Node *> &covering){
ev(); s << "cover " << covered->Name.name() << ": " << covered->number << " by ";
for(unsigned i = 0; i < covering.size(); i++)
std::cout << covering[i]->number << " ";
std::cout << std::endl;
s << covering[i]->number << " ";
s << std::endl;
}
virtual void RemoveCover(RPFP::Node *covered, RPFP::Node *covering){
ev(); s << "uncover " << covered->Name.name() << ": " << covered->number << " by " << covering->number << std::endl;
@ -2755,7 +3095,7 @@ namespace Duality {
virtual void Conjecture(RPFP::Node *node, const RPFP::Transformer &t){
ev(); s << "conjecture " << node->number << " " << node->Name.name() << ": ";
rpfp->Summarize(t.Formula);
std::cout << std::endl;
s << std::endl;
}
virtual void Dominates(RPFP::Node *node, RPFP::Node *other){
ev(); s << "dominates " << node->Name.name() << ": " << node->number << " > " << other->number << std::endl;

22
src/duality/duality_wrapper.cpp Normal file → Executable file
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -37,16 +37,18 @@ Revision History:
namespace Duality {
solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) {
solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) {
params_ref p;
p.set_bool("proof", true); // this is currently useless
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("mbqi",true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
if(true || extensional)
extensional = mbqi && (true || _extensional);
if(extensional)
p.set_bool("array.extensional",true);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
@ -656,6 +658,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
}
void solver::print(const char *filename) {
std::ofstream f(filename);
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(f, m_solver->get_assertion(n-1));
}
void solver::show_assertion_ids() {
#if 0
unsigned n = m_solver->get_num_assertions();

37
src/duality/duality_wrapper.h
View file

@ -182,6 +182,7 @@ namespace Duality {
void set(char const * param, char const * value) { m_config.set(param,value); }
void set(char const * param, bool value) { m_config.set(param,value); }
void set(char const * param, int value) { m_config.set(param,value); }
config &get_config() {return m_config;}
symbol str_symbol(char const * s);
symbol int_symbol(int n);
@ -243,6 +244,9 @@ namespace Duality {
sort_kind get_sort_kind(const sort &s);
expr translate(const expr &e);
func_decl translate(const func_decl &);
void print_expr(std::ostream &s, const ast &e);
fixedpoint mk_fixedpoint();
@ -818,6 +822,7 @@ namespace Duality {
model the_model;
bool canceled;
proof_gen_mode m_mode;
bool extensional;
public:
solver(context & c, bool extensional = false, bool models = true);
solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
@ -921,6 +926,7 @@ namespace Duality {
unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}
void show();
void print(const char *filename);
void show_assertion_ids();
proof get_proof(){
@ -928,6 +934,7 @@ namespace Duality {
return proof(ctx(),m_solver->get_proof());
}
bool extensional_array_theory() {return extensional;}
};
#if 0
@ -1370,6 +1377,20 @@ namespace Duality {
return to_expr(a.raw());
}
inline expr context::translate(const expr &e) {
::expr *f = to_expr(e.raw());
if(&e.ctx().m() != &m()) // same ast manager -> no translation
throw "ast manager mismatch";
return cook(f);
}
inline func_decl context::translate(const func_decl &e) {
::func_decl *f = to_func_decl(e.raw());
if(&e.ctx().m() != &m()) // same ast manager -> no translation
throw "ast manager mismatch";
return func_decl(*this,f);
}
typedef double clock_t;
clock_t current_time();
inline void output_time(std::ostream &os, clock_t time){os << time;}
@ -1401,14 +1422,6 @@ namespace hash_space {
};
}
// to make Duality::ast hashable in windows
#ifdef WIN32
template <> inline
size_t stdext::hash_value<Duality::ast >(const Duality::ast& s)
{
return s.raw()->get_id();
}
#endif
// to make Duality::ast usable in ordered collections
namespace std {
@ -1445,14 +1458,6 @@ namespace hash_space {
};
}
// to make Duality::func_decl hashable in windows
#ifdef WIN32
template <> inline
size_t stdext::hash_value<Duality::func_decl >(const Duality::func_decl& s)
{
return s.raw()->get_id();
}
#endif
// to make Duality::func_decl usable in ordered collections
namespace std {

2
src/interp/foci2.h
View file

@ -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")))

4
src/interp/iz3base.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -34,9 +34,7 @@ Revision History:
#include "../smt/smt_solver.h"
#ifndef WIN32
using namespace stl_ext;
#endif
iz3base::range &iz3base::ast_range(ast t){

4
src/interp/iz3checker.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -36,9 +36,7 @@ Revision History:
#include <iterator>
#ifndef WIN32
using namespace stl_ext;
#endif
struct iz3checker : iz3base {

2
src/interp/iz3foci.cpp
View file

@ -25,9 +25,7 @@ Revision History:
#include "foci2.h"
#include "iz3foci.h"
#ifndef WIN32
using namespace stl_ext;
#endif
class iz3foci_impl : public iz3secondary {

545
src/interp/iz3hash.h Executable file → Normal file
View file

@ -7,7 +7,16 @@ Module Name:
Abstract:
Wrapper for stl hash tables
Simple implementation of bucket-list hash tables conforming to SGI
hash_map and hash_set interfaces. Just enough members are
implemented to support iz3 and duality.
iz3 and duality need this package because they assume that insert
preserves iterators and references to elements, which is not true
of the hashtable packages in util.
This package lives in namespace hash_space. Specializations of
class "hash" should be made in this namespace.
Author:
@ -17,66 +26,36 @@ 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>
#include <vector>
#include <iterator>
#include "hash.h"
// stupid STL doesn't include hash function for class string
#ifndef WIN32
namespace stl_ext {
template <>
class hash<std::string> {
stl_ext::hash<const char *> H;
public:
size_t operator()(const std::string &s) const {
return H(s.c_str());
}
};
}
#endif
#define stl_ext hash_space
namespace hash_space {
template <typename T> class hash {};
template <>
class hash<int> {
public:
size_t operator()(const int &s) const {
return s;
}
};
template <>
class hash<std::string> {
public:
size_t operator()(const std::string &s) const {
return string_hash(s.c_str(), s.size(), 0);
}
};
template <>
class hash<std::pair<int,int> > {
public:
@ -84,17 +63,7 @@ namespace hash_space {
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:
@ -102,70 +71,402 @@ namespace hash_space {
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
enum { num_primes = 29 };
#ifdef WIN32
static const unsigned long primes[num_primes] =
{
7ul,
53ul,
97ul,
193ul,
389ul,
769ul,
1543ul,
3079ul,
6151ul,
12289ul,
24593ul,
49157ul,
98317ul,
196613ul,
393241ul,
786433ul,
1572869ul,
3145739ul,
6291469ul,
12582917ul,
25165843ul,
50331653ul,
100663319ul,
201326611ul,
402653189ul,
805306457ul,
1610612741ul,
3221225473ul,
4294967291ul
};
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;
}
};
}
inline unsigned long next_prime(unsigned long n) {
const unsigned long* to = primes + (int)num_primes;
for(const unsigned long* p = primes; p < to; p++)
if(*p >= n) return *p;
return primes[num_primes-1];
}
#endif
#ifndef WIN32
#if 0
namespace stl_ext {
template <class T>
class hash<T *> {
template<class Value, class Key, class HashFun, class GetKey, class KeyEqFun>
class hashtable
{
public:
size_t operator()(const T *p) const {
return (size_t) p;
typedef Value &reference;
typedef const Value &const_reference;
struct Entry
{
Entry* next;
Value val;
Entry(const Value &_val) : val(_val) {next = 0;}
};
struct iterator
{
Entry* ent;
hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef Value& reference;
typedef Value* pointer;
iterator(Entry* _ent, hashtable* _tab) : ent(_ent), tab(_tab) { }
iterator() { }
Value &operator*() const { return ent->val; }
Value *operator->() const { return &(operator*()); }
iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
iterator operator++(int) {
iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const iterator& it) const {
return ent == it.ent;
}
bool operator!=(const iterator& it) const {
return ent != it.ent;
}
};
struct const_iterator
{
const Entry* ent;
const hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef const Value& reference;
typedef const Value* pointer;
const_iterator(const Entry* _ent, const hashtable* _tab) : ent(_ent), tab(_tab) { }
const_iterator() { }
const Value &operator*() const { return ent->val; }
const Value *operator->() const { return &(operator*()); }
const_iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
const_iterator operator++(int) {
const_iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const const_iterator& it) const {
return ent == it.ent;
}
bool operator!=(const const_iterator& it) const {
return ent != it.ent;
}
};
private:
typedef std::vector<Entry*> Table;
Table buckets;
size_t entries;
HashFun hash_fun ;
GetKey get_key;
KeyEqFun key_eq_fun;
public:
hashtable(size_t init_size) : buckets(init_size,(Entry *)0) {
entries = 0;
}
hashtable(const hashtable& other) {
dup(other);
}
hashtable& operator= (const hashtable& other) {
if (&other != this)
dup(other);
return *this;
}
~hashtable() {
clear();
}
size_t size() const {
return entries;
}
bool empty() const {
return size() == 0;
}
void swap(hashtable& other) {
buckets.swap(other.buckets);
std::swap(entries, other.entries);
}
iterator begin() {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return iterator(buckets[i], this);
return end();
}
iterator end() {
return iterator(0, this);
}
const_iterator begin() const {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return const_iterator(buckets[i], this);
return end();
}
const_iterator end() const {
return const_iterator(0, this);
}
size_t get_bucket(const Value& val, size_t n) const {
return hash_fun(get_key(val)) % n;
}
size_t get_key_bucket(const Key& key) const {
return hash_fun(key) % buckets.size();
}
size_t get_bucket(const Value& val) const {
return get_bucket(val,buckets.size());
}
Entry *lookup(const Value& val, bool ins = false)
{
resize(entries + 1);
size_t n = get_bucket(val);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), get_key(val)))
return ent;
if(!ins) return 0;
Entry* tmp = new Entry(val);
tmp->next = from;
buckets[n] = tmp;
++entries;
return tmp;
}
Entry *lookup_key(const Key& key) const
{
size_t n = get_key_bucket(key);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), key))
return ent;
return 0;
}
const_iterator find(const Key& key) const {
return const_iterator(lookup_key(key),this);
}
iterator find(const Key& key) {
return iterator(lookup_key(key),this);
}
std::pair<iterator,bool> insert(const Value& val){
size_t old_entries = entries;
Entry *ent = lookup(val,true);
return std::pair<iterator,bool>(iterator(ent,this),entries > old_entries);
}
iterator insert(const iterator &it, const Value& val){
Entry *ent = lookup(val,true);
return iterator(ent,this);
}
size_t erase(const Key& key)
{
Entry** p = &(buckets[get_key_bucket(key)]);
size_t count = 0;
while(*p){
Entry *q = *p;
if (key_eq_fun(get_key(q->val), key)) {
++count;
*p = q->next;
delete q;
}
else
p = &(q->next);
}
entries -= count;
return count;
}
void resize(size_t new_size) {
const size_t old_n = buckets.size();
if (new_size <= old_n) return;
const size_t n = next_prime(new_size);
if (n <= old_n) return;
Table tmp(n, (Entry*)(0));
for (size_t i = 0; i < old_n; ++i) {
Entry* ent = buckets[i];
while (ent) {
size_t new_bucket = get_bucket(ent->val, n);
buckets[i] = ent->next;
ent->next = tmp[new_bucket];
tmp[new_bucket] = ent;
ent = buckets[i];
}
}
buckets.swap(tmp);
}
void clear()
{
for (size_t i = 0; i < buckets.size(); ++i) {
for (Entry* ent = buckets[i]; ent != 0;) {
Entry* next = ent->next;
delete ent;
ent = next;
}
buckets[i] = 0;
}
entries = 0;
}
void dup(const hashtable& other)
{
buckets.resize(other.buckets.size());
for (size_t i = 0; i < other.buckets.size(); ++i) {
Entry** to = &buckets[i];
for (Entry* from = other.buckets[i]; from; from = from->next)
to = &((*to = new Entry(from->val))->next);
}
entries = other.entries;
}
};
template <typename T>
class equal {
public:
bool operator()(const T& x, const T &y) const {
return x == y;
}
};
template <typename T>
class identity {
public:
const T &operator()(const T &x) const {
return x;
}
};
template <typename T, typename U>
class proj1 {
public:
const T &operator()(const std::pair<T,U> &x) const {
return x.first;
}
};
template <typename Element, class HashFun = hash<Element>,
class EqFun = equal<Element> >
class hash_set
: public hashtable<Element,Element,HashFun,identity<Element>,EqFun> {
public:
typedef Element value_type;
hash_set()
: hashtable<Element,Element,HashFun,identity<Element>,EqFun>(7) {}
};
template <typename Key, typename Value, class HashFun = hash<Key>,
class EqFun = equal<Key> >
class hash_map
: public hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun> {
public:
hash_map()
: hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>(7) {}
Value &operator[](const Key& key) {
std::pair<Key,Value> kvp(key,Value());
return lookup(kvp,true)->val.second;
}
};
}
#endif
#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

6
src/interp/iz3interp.cpp
View file

@ -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)
@ -43,9 +43,7 @@ Revision History:
#ifndef WIN32
using namespace stl_ext;
#endif
@ -64,7 +62,7 @@ struct frame_reducer : public iz3mgr {
: iz3mgr(other) {}
void get_proof_assumptions_rec(z3pf proof, hash_set<ast> &memo, std::vector<bool> &used_frames){
if(memo.count(proof))return;
if(memo.find(proof) != memo.end())return;
memo.insert(proof);
pfrule dk = pr(proof);
if(dk == PR_ASSERTED){

27
src/interp/iz3mgr.cpp Normal file → Executable file
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -38,9 +38,7 @@ Revision History:
#include "params.h"
#ifndef WIN32
using namespace stl_ext;
#endif
std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){
@ -249,6 +247,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
void iz3mgr::show(ast t){
if(t.null()){
std::cout << "(null)" << std::endl;
}
params_ref p;
p.set_bool("flat_assoc",false);
std::cout << mk_pp(t.raw(), m(), p) << std::endl;
@ -693,10 +694,13 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
throw "not an inequality";
}
}
Qrhs = make(Times,c,Qrhs);
bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
if(pstrict && qstrict && round_off)
bool pstrict = op(P) == Lt;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false;
}
Qrhs = make(Times,c,Qrhs);
bool strict = pstrict || qstrict;
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
@ -881,3 +885,14 @@ iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
std::vector<ast> bvs; bvs.push_back(var);
return make_quant(quantifier,bvs,e);
}
#if 0
void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast &e, const ast &var, std::vector<ast> &substs){
std::pair<ast,bool> foo(e,false);
std::pair<hash_map<ast,bool>::iterator,bool> bar = memo.insert(foo);
if(bar.second){
if(op(e) ==
}
}
#endif

8
src/interp/iz3mgr.h Normal file → Executable file
View file

@ -126,14 +126,6 @@ namespace hash_space {
};
}
// to make ast_r hashable in windows
#ifdef WIN32
template <> inline
size_t stdext::hash_value<ast_r >(const ast_r& s)
{
return s.raw()->get_id();
}
#endif
// to make ast_r usable in ordered collections
namespace std {

4
src/interp/iz3pp.cpp
View file

@ -36,11 +36,8 @@ Revision History:
#include"expr_abstract.h"
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
// We promise not to use this for hash_map with range destructor
namespace stl_ext {
template <>
@ -51,7 +48,6 @@ namespace stl_ext {
}
};
}
#endif
// TBD: algebraic data-types declarations will not be printed.

2
src/interp/iz3profiling.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)

2
src/interp/iz3proof.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)

465
src/interp/iz3proof_itp.cpp Normal file → Executable file
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -26,9 +26,7 @@ Revision History:
#include "iz3proof_itp.h"
#ifndef WIN32
using namespace stl_ext;
#endif
// #define INVARIANT_CHECKING
@ -369,11 +367,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
default:
{
symb s = sym(itp2);
if(s == sforall || s == sexists)
res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
else
opr o = op(itp2);
if(o == Uninterpreted){
symb s = sym(itp2);
if(s == sforall || s == sexists)
res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
else
res = itp2;
}
else {
res = itp2;
}
}
}
}
@ -405,11 +409,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
default:
{
symb s = sym(itp1);
if(s == sforall || s == sexists)
res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
else
opr o = op(itp1);
if(o == Uninterpreted){
symb s = sym(itp1);
if(s == sforall || s == sexists)
res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
else
res = itp1;
}
else {
res = itp1;
}
}
}
}
@ -464,18 +474,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
ast &res = bar.first->second;
if(bar.second){
symb g = sym(e);
if(g == rotate_sum){
if(var == get_placeholder(arg(e,0))){
res = e;
if(op(e) == Uninterpreted){
symb g = sym(e);
if(g == rotate_sum){
if(var == get_placeholder(arg(e,0))){
res = e;
}
else
res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
return res;
}
if(g == concat){
res = e;
return res;
}
else
res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
return res;
}
if(g == concat){
res = e;
return res;
}
int nargs = num_args(e);
std::vector<ast> args(nargs);
@ -538,8 +550,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
else if(g == symm) res = simplify_symm(args);
else if(g == modpon) res = simplify_modpon(args);
else if(g == sum) res = simplify_sum(args);
#if 0
else if(g == exmid) res = simplify_exmid(args);
else if(g == cong) res = simplify_cong(args);
#if 0
else if(g == modpon) res = simplify_modpon(args);
else if(g == leq2eq) res = simplify_leq2eq(args);
else if(g == eq2leq) res = simplify_eq2leq(args);
@ -579,18 +592,36 @@ class iz3proof_itp_impl : public iz3proof_itp {
return is_ineq(ineq);
}
ast destruct_cond_ineq(const ast &ineq, ast &Aproves, ast &Bproves){
ast res = ineq;
opr o = op(res);
if(o == And){
Aproves = my_and(Aproves,arg(res,0));
res = arg(res,1);
o = op(res);
}
if(o == Implies){
Bproves = my_and(Bproves,arg(res,0));
res = arg(res,1);
}
return res;
}
ast simplify_sum(std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = args[0];
ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
if(!is_normal_ineq(ineq)) throw cannot_simplify();
sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
return my_and(Aproves,my_implies(Bproves,ineq));
}
ast simplify_rotate_sum(const ast &pl, const ast &pf){
ast cond = mk_true();
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = make(Leq,make_int("0"),make_int("0"));
return rotate_sum_rec(pl,pf,cond,ineq);
ineq = rotate_sum_rec(pl,pf,Aproves,Bproves,ineq);
if(is_true(Aproves) && is_true(Bproves))
return ineq;
return my_and(Aproves,my_implies(Bproves,ineq));
}
bool is_rewrite_chain(const ast &chain){
@ -623,7 +654,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
opr o = op(ineq2);
if(o == Implies){
if(o == And){
sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
Aproves = my_and(Aproves,arg(ineq2,0));
}
else if(o == Implies){
sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
Bproves = my_and(Bproves,arg(ineq2,0));
}
@ -658,7 +693,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast dummy1, dummy2;
sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2);
n1 = merge_normal_chains(n1,n2, Aproves, Bproves);
ineq = make_normal(in1,n1);
ineq = is_true(n1) ? in1 : make_normal(in1,n1);
}
bool is_ineq(const ast &ineq){
@ -683,23 +718,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
}
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
if(pf == pl)
return my_implies(Bproves,simplify_ineq(ineq));
ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Aproves, ast &Bproves, ast &ineq){
if(pf == pl){
if(sym(ineq) == normal)
return ineq;
return simplify_ineq(ineq);
}
if(op(pf) == Uninterpreted && sym(pf) == sum){
if(arg(pf,2) == pl){
ast Aproves = mk_true();
sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
ineq = idiv_ineq(ineq,arg(pf,1));
return my_implies(Bproves,ineq);
return ineq;
}
ast Aproves = mk_true();
sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
if(!is_true(Aproves))
throw "help!";
return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
return rotate_sum_rec(pl,arg(pf,0),Aproves,Bproves,ineq);
}
throw cannot_simplify();
}
@ -710,29 +742,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast x = arg(equality,0);
ast y = arg(equality,1);
ast Aproves1 = mk_true(), Bproves1 = mk_true();
ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1));
ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1));
ast pf1 = destruct_cond_ineq(arg(pf,1), Aproves1, Bproves1);
ast pf2 = destruct_cond_ineq(arg(pf,2), Aproves1, Bproves1);
ast xleqy = round_ineq(ineq_from_chain(pf1,Aproves1,Bproves1));
ast yleqx = round_ineq(ineq_from_chain(pf2,Aproves1,Bproves1));
ast ineq1 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1);
sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1);
Bproves1 = my_and(Bproves1,z3_simplify(ineq1));
ast Acond = my_implies(Aproves1,my_and(Bproves1,z3_simplify(ineq1)));
ast Aproves2 = mk_true(), Bproves2 = mk_true();
ast ineq2 = make(Leq,make_int("0"),make_int("0"));
sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2);
sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
Bproves2 = z3_simplify(ineq2);
if(!is_true(Aproves1) || !is_true(Aproves2))
throw "help!";
ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2)));
// if(!is_true(Aproves1) || !is_true(Bproves1))
// std::cout << "foo!\n";;
if(get_term_type(x) == LitA){
ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitA,top_pos,Acond,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
if(get_term_type(y) == LitA){
ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx)));
ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter));
ast rewrite2 = make_rewrite(LitA,top_pos,Acond,make(Equal,iter,y));
ast rewrite1 = make_rewrite(LitB,top_pos,Bcond,make(Equal,x,iter));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
throw cannot_simplify();
@ -741,6 +775,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast round_ineq(const ast &ineq){
if(sym(ineq) == normal)
return make_normal(round_ineq(arg(ineq,0)),arg(ineq,1));
if(!is_ineq(ineq))
throw cannot_simplify();
ast res = simplify_ineq(ineq);
@ -749,6 +785,29 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
ast unmixed_eq2ineq(const ast &lhs, const ast &rhs, opr comp_op, const ast &equa, ast &cond){
ast ineqs= chain_ineqs(comp_op,LitA,equa,lhs,rhs); // chain must be from lhs to rhs
cond = my_and(cond,chain_conditions(LitA,equa));
ast Bconds = z3_simplify(chain_conditions(LitB,equa));
if(is_true(Bconds) && op(ineqs) != And)
return my_implies(cond,ineqs);
if(op(ineqs) != And)
return my_and(Bconds,my_implies(cond,ineqs));
throw "help!";
}
ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){
if(is_true(equa))
return itp;
std::vector<ast> args(3);
args[0] = itp;
args[1] = make_int("1");
ast ineq = make(Leq,make_int(rational(0)),make_int(rational(0)));
args[2] = make_normal(ineq,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
return simplify_sum(args);
}
ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,1)){
ast cond = mk_true();
@ -756,20 +815,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(is_equivrel_chain(equa)){
ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
if(lhst != LitMixed && rhst != LitMixed){
ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs
cond = my_and(cond,chain_conditions(LitA,equa));
ast Bconds = z3_simplify(chain_conditions(LitB,equa));
if(is_true(Bconds) && op(ineqs) != And)
return my_implies(cond,ineqs);
}
if(lhst != LitMixed && rhst != LitMixed)
return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
else {
ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
ast left, left_term, middle, right_term, right;
left = get_left_movers(equa,lhs,middle,left_term);
middle = get_right_movers(middle,rhs,right,right_term);
ast itp = unmixed_eq2ineq(left_term, right_term, op(arg(neg_equality,0)), middle, cond);
// itp = my_implies(cond,itp);
itp = add_mixed_eq2ineq(lhs, left_term, left, itp);
itp = add_mixed_eq2ineq(right_term, rhs, right, itp);
return itp;
}
}
}
throw cannot_simplify();
throw "help!";
}
void reverse_modpon(std::vector<ast> &args){
@ -836,6 +896,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast equa = sep_cond(args[0],cond);
if(is_equivrel_chain(equa))
return my_implies(cond,reverse_chain(equa));
if(is_negation_chain(equa))
return commute_negation_chain(equa);
throw cannot_simplify();
}
@ -876,6 +938,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
return chain;
}
struct subterm_normals_failed {};
void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals,
const ast &pos, hash_set<ast> &memo, ast &Aproves, ast &Bproves){
opr o1 = op(ineq1);
@ -889,14 +953,77 @@ class iz3proof_itp_impl : public iz3proof_itp {
get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves);
}
}
else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){
memo.insert(ineq2);
ast sub_chain = extract_rewrites(chain,pos);
if(is_true(sub_chain))
throw "bad inequality rewriting";
ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain));
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
else if(get_term_type(ineq2) == LitMixed){
if(memo.find(ineq2) == memo.end()){
memo.insert(ineq2);
ast sub_chain = extract_rewrites(chain,pos);
if(is_true(sub_chain))
throw "bad inequality rewriting";
ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain));
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}
}
else if(!(ineq1 == ineq2))
throw subterm_normals_failed();
}
ast rewrites_to_normals(const ast &ineq1, const ast &chain, ast &normals, ast &Aproves, ast &Bproves, ast &Aineqs){
if(is_true(chain))
return ineq1;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast new_ineq1 = rewrites_to_normals(ineq1, rest, normals, Aproves, Bproves, Aineqs);
ast p1 = rewrite_pos(last);
ast term1;
ast coeff = arith_rewrite_coeff(new_ineq1,p1,term1);
ast res = subst_in_pos(new_ineq1,rewrite_pos(last),rewrite_rhs(last));
ast rpos;
pos_diff(p1,rewrite_pos(last),rpos);
ast term2 = subst_in_pos(term1,rpos,rewrite_rhs(last));
if(get_term_type(term1) != LitMixed && get_term_type(term2) != LitMixed){
if(is_rewrite_side(LitA,last))
linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
}
else {
ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
ast new_normal = fix_normal(term1,term2,pf);
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}
return res;
}
ast arith_rewrite_coeff(const ast &ineq, ast &p1, ast &term){
ast coeff = make_int(rational(1));
if(p1 == top_pos){
term = ineq;
return coeff;
}
int argpos = pos_arg(p1);
opr o = op(ineq);
switch(o){
case Leq:
case Lt:
coeff = argpos ? make_int(rational(1)) : make_int(rational(-1));
break;
case Geq:
case Gt:
coeff = argpos ? make_int(rational(-1)) : make_int(rational(1));
break;
case Not:
case Plus:
break;
case Times:
coeff = arg(ineq,0);
break;
default:
p1 = top_pos;
term = ineq;
return coeff;
}
p1 = arg(p1,1);
ast res = arith_rewrite_coeff(arg(ineq,argpos),p1,term);
p1 = pos_add(argpos,p1);
return coeff == make_int(rational(1)) ? res : make(Times,coeff,res);
}
ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){
@ -906,18 +1033,25 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast ineq2 = apply_rewrite_chain(ineq1,tail);
ast nc = mk_true();
hash_set<ast> memo;
get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
ast itp;
ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
ast Aproves_save = Aproves, Bproves_save = Bproves; try {
get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
}
catch (const subterm_normals_failed &){ Aproves = Aproves_save; Bproves = Bproves_save; nc = mk_true();
rewrites_to_normals(ineq1, tail, nc, Aproves, Bproves, itp);
}
if(is_rewrite_side(LitA,head)){
itp = ineq1;
linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form
//itp = ineq1;
ast mc = z3_simplify(chain_side_proves(LitB,pref));
Bproves = my_and(Bproves,mc);
}
else {
itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
ast mc = z3_simplify(chain_side_proves(LitA,pref));
Aproves = my_and(Aproves,mc);
}
if(is_true(nc))
return itp;
return make_normal(itp,nc);
}
@ -951,7 +1085,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast simplify_modpon(const std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = simplify_modpon_fwd(args,Bproves);
ast Q2 = sep_cond(args[2],Bproves);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp;
if(is_normal_ineq(Q2)){ // inequalities are special
ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
@ -964,6 +1098,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast simplify_exmid(const std::vector<ast> &args){
if(is_equivrel(args[0])){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = destruct_cond_ineq(args[1],Aproves,Bproves);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp = contra_chain(Q2,chain);
return my_and(Aproves,my_implies(Bproves,interp));
}
throw "bad exmid";
}
ast simplify_cong(const std::vector<ast> &args){
ast Aproves = mk_true(), Bproves = mk_true();
ast chain = destruct_cond_ineq(args[0],Aproves,Bproves);
rational pos;
if(is_numeral(args[1],pos)){
int ipos = pos.get_unsigned();
chain = chain_pos_add(ipos,chain);
ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves);
ast interp = contra_chain(Q2,chain);
return my_and(Aproves,my_implies(Bproves,interp));
}
throw "bad cong";
}
bool is_equivrel(const ast &p){
opr o = op(p);
return o == Equal || o == Iff;
@ -1248,6 +1407,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(pos == top_pos && op(equality) == Iff && !is_true(arg(equality,0)))
throw "bad rewrite";
#endif
if(!is_equivrel(equality))
throw "bad rewrite";
return make(t == LitA ? rewrite_A : rewrite_B, pos, cond, equality);
}
@ -1450,6 +1611,50 @@ class iz3proof_itp_impl : public iz3proof_itp {
return is_negation_chain(rest);
}
ast commute_negation_chain(const ast &chain){
if(is_true(chain))
return chain;
ast last = chain_last(chain);
ast rest = chain_rest(chain);
if(is_true(rest)){
ast old = rewrite_rhs(last);
if(!(op(old) == Not))
throw "bad negative equality chain";
ast equ = arg(old,0);
if(!is_equivrel(equ))
throw "bad negative equality chain";
last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True));
return chain_cons(rest,last);
}
ast pos = rewrite_pos(last);
if(pos == top_pos)
throw "bad negative equality chain";
int idx = pos_arg(pos);
if(idx != 0)
throw "bad negative equality chain";
pos = arg(pos,1);
if(pos == top_pos){
ast lhs = rewrite_lhs(last);
ast rhs = rewrite_rhs(last);
if(op(lhs) != Equal || op(rhs) != Equal)
throw "bad negative equality chain";
last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last),
make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0))));
}
else {
idx = pos_arg(pos);
if(idx == 0)
idx = 1;
else if(idx == 1)
idx = 0;
else
throw "bad negative equality chain";
pos = pos_add(0,pos_add(idx,arg(pos,1)));
last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last));
}
return chain_cons(commute_negation_chain(rest),last);
}
// split a rewrite chain into head and tail at last top-level rewrite
ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){
ast last = chain_last(chain);
@ -1466,6 +1671,47 @@ class iz3proof_itp_impl : public iz3proof_itp {
return head;
}
// split a rewrite chain into head and tail at last non-mixed term
ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
if(is_true(chain) || get_term_type(rhs) != LitMixed){
mid = rhs;
tail = mk_true();
return chain;
}
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast mm = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
ast res = get_right_movers(rest,mm,tail,mid);
tail = chain_cons(tail,last);
return res;
}
// split a rewrite chain into head and tail at first non-mixed term
ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
if(is_true(chain)){
mid = lhs;
if(get_term_type(lhs) != LitMixed){
tail = mk_true();
return chain;
}
return ast();
}
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast res = get_left_movers(rest,lhs,tail,mid);
if(res.null()){
mid = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last));
if(get_term_type(mid) != LitMixed){
tail = mk_true();
return chain;
}
return ast();
}
tail = chain_cons(tail,last);
return res;
}
struct cannot_split {};
/** Split a chain of rewrites two chains, operating on positions 0 and 1.
@ -1558,7 +1804,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast diff;
if(comp_op == Leq) diff = make(Sub,rhs,mid);
else diff = make(Sub,mid,rhs);
ast foo = z3_simplify(make(Leq,make_int("0"),diff));
ast foo = make(Leq,make_int("0"),z3_simplify(diff));
if(is_true(cond))
cond = foo;
else {
@ -1668,11 +1914,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
LitType lhst = get_term_type(lhs);
LitType rhst = get_term_type(rhs);
if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
if(lhst == LitMixed && (rhst != LitMixed || ast_id(lhs) < ast_id(rhs)))
return make_normal_step(lhs,rhs,proof);
else
if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs)))
return make_normal_step(rhs,lhs,reverse_chain(proof));
throw "help!";
}
ast chain_side_proves(LitType side, const ast &chain){
@ -1692,8 +1940,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast lhs2 = normal_lhs(f2);
int id1 = ast_id(lhs1);
int id2 = ast_id(lhs2);
if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
if(id1 < id2)
return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
if(id2 < id1)
return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
ast rhs1 = normal_rhs(f1);
ast rhs2 = normal_rhs(f2);
LitType t1 = get_term_type(rhs1);
@ -1719,9 +1969,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
Aproves = my_and(Aproves,mcB);
ast rep = apply_rewrite_chain(rhs1,Aproof);
new_proof = concat_rewrite_chain(pf1,Aproof);
new_normal = make_normal_step(rhs1,rep,new_proof);
new_normal = make_normal_step(lhs1,rep,new_proof);
ast A_normal = make_normal_step(rhs1,rep,Aproof);
ast res = cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves));
res = merge_normal_chains_rec(res,cons_normal(A_normal,make(True)),trans,Aproves,Bproves);
return res;
}
else if(t1 == LitA && t2 == LitB)
else if(t1 == LitB && t2 == LitA)
return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
else if(t1 == LitA) {
ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
@ -1743,17 +1997,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
return chain;
ast f = normal_first(chain);
ast r = normal_rest(chain);
r = trans_normal_chain(r,trans);
ast rhs = normal_rhs(f);
hash_map<ast,ast>::iterator it = trans.find(rhs);
ast new_normal;
if(it != trans.end()){
if(it != trans.end() && get_term_type(normal_lhs(f)) == LitMixed){
const ast &f2 = it->second;
ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
}
else
new_normal = f;
return cons_normal(new_normal,trans_normal_chain(r,trans));
if(get_term_type(normal_lhs(f)) == LitMixed)
trans[normal_lhs(f)] = new_normal;
return cons_normal(new_normal,r);
}
ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){
@ -2011,8 +2268,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con){
throw proof_error();
}
if(get_term_type(con) == LitA)
return mk_false();
if(get_term_type(con) == LitB)
return mk_true();
ast itp = make(And,make(contra,no_proof,mk_false()),
make(contra,mk_true(),mk_not(con)));
return itp;
}
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x. Ditto for ~(x=y) */
@ -2247,10 +2510,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
throw proof_error();
}
}
Qrhs = make(Times,c,Qrhs);
#if 0
bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
if(pstrict && qstrict && round_off)
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
#else
bool pstrict = op(P) == Lt;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false;
}
Qrhs = make(Times,c,Qrhs);
bool strict = pstrict || qstrict;
#endif
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
@ -2269,8 +2541,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
itp = mk_true();
break;
default: { // mixed equality
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed)
std::cerr << "WARNING: mixed term in leq2eq\n";
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){
// std::cerr << "WARNING: mixed term in leq2eq\n";
std::vector<ast> lits;
lits.push_back(con);
lits.push_back(make(Not,xleqy));
lits.push_back(make(Not,yleqx));
return make_axiom(lits);
}
std::vector<ast> conjs; conjs.resize(3);
conjs[0] = mk_not(con);
conjs[1] = xleqy;
@ -2383,6 +2661,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
hash_map<ast,ast>::iterator it = localization_map.find(e);
if(it != localization_map.end() && is_bool_type(get_type(e))
&& !pv->ranges_intersect(pv->ast_scope(it->second),rng))
it = localization_map.end(); // prevent quantifiers over booleans
if(it != localization_map.end()){
pf = localization_pf_map[e];
e = it->second;
@ -2405,7 +2688,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
frng = srng; // this term will be localized
}
else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
frng = erng; // this term will be localized
// std::cout << "WARNING: non-local arithmetic\n";
// frng = erng; // this term will be localized
}
else if(o == Select){ // treat the array term like a function symbol
prover::range srng = pv->ast_scope(arg(e,0));
if(!(srng.lo > srng.hi) && pv->ranges_intersect(srng,rng)) // localize to desired range if possible
frng = pv->range_glb(srng,rng);
else
frng = srng; // this term will be localized
}
std::vector<ast> largs(nargs);
std::vector<ast> eqs;
@ -2434,7 +2725,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
return e; // this term occurs in range, so it's O.K.
if(is_array_type(get_type(e)))
throw "help!";
std::cerr << "WARNING: array quantifier\n";
// choose a frame for the constraint that is close to range
int frame = pv->range_near(pv->ast_scope(e),rng);

151
src/interp/iz3translate.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -39,9 +39,7 @@ Revision History:
#include <set>
//using std::vector;
#ifndef WIN32
using namespace stl_ext;
#endif
@ -188,6 +186,15 @@ public:
get_Z3_lits(con, lits);
iproof->make_axiom(lits);
}
#ifdef LOCALIZATION_KLUDGE
else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST
&& get_locality_rec(prem(proof,1)) == INT_MAX){
std::vector<ast> lits;
ast con = conc(proof);
get_Z3_lits(con, lits);
iproof->make_axiom(lits);
}
#endif
else {
unsigned nprems = num_prems(proof);
for(unsigned i = 0; i < nprems; i++){
@ -1271,6 +1278,84 @@ public:
return make(Plus,args);
}
ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
if(op(t) == Plus){
int nargs = num_args(t);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = replace_summands_with_fresh_vars(arg(t,i),map);
return make(Plus,args);
}
if(op(t) == Times)
return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map));
if(map.find(t) == map.end())
map[t] = mk_fresh_constant("@s",get_type(t));
return map[t];
}
ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
ast res = normalize_inequality(ineq);
ast lhs = arg(res,0);
lhs = replace_summands_with_fresh_vars(lhs,map);
res = make(op(res),SortSum(lhs),arg(res,1));
return res;
}
Iproof::node painfully_reconstruct_farkas(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
int nprems = prems.size();
std::vector<ast> pcons(nprems),npcons(nprems);
hash_map<ast,ast> pcon_to_pf, npcon_to_pcon, pain_map;
for(int i = 0; i < nprems; i++){
pcons[i] = conc(prems[i]);
npcons[i] = painfully_normalize_ineq(pcons[i],pain_map);
pcon_to_pf[npcons[i]] = pfs[i];
npcon_to_pcon[npcons[i]] = pcons[i];
}
// ast leq = make(Leq,arg(con,0),arg(con,1));
ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
pcons.push_back(mk_not(con));
npcons.push_back(ncon);
// ast assumps = make(And,pcons);
ast new_proof;
if(is_sat(npcons,new_proof))
throw "Proof error!";
pfrule dk = pr(new_proof);
int nnp = num_prems(new_proof);
std::vector<Iproof::node> my_prems;
std::vector<ast> farkas_coeffs, my_pcons;
if(dk == PR_TH_LEMMA
&& get_theory_lemma_theory(new_proof) == ArithTheory
&& get_theory_lemma_kind(new_proof) == FarkasKind)
get_farkas_coeffs(new_proof,farkas_coeffs);
else if(dk == PR_UNIT_RESOLUTION && nnp == 2){
for(int i = 0; i < nprems; i++)
farkas_coeffs.push_back(make_int(rational(1)));
}
else
throw "cannot reconstruct farkas proof";
for(int i = 0; i < nnp; i++){
ast p = conc(prem(new_proof,i));
p = really_normalize_ineq(p);
if(pcon_to_pf.find(p) != pcon_to_pf.end()){
my_prems.push_back(pcon_to_pf[p]);
my_pcons.push_back(npcon_to_pcon[p]);
}
else if(p == ncon){
my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
my_pcons.push_back(mk_not(con));
}
else
throw "cannot reconstruct farkas proof";
}
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
return res;
}
ast really_normalize_ineq(const ast &ineq){
ast res = normalize_inequality(ineq);
res = make(op(res),SortSum(arg(res,0)),arg(res,1));
@ -1309,7 +1394,7 @@ public:
farkas_coeffs.push_back(make_int(rational(1)));
}
else
throw "cannot reconstruct farkas proof";
return painfully_reconstruct_farkas(prems,pfs,con);
for(int i = 0; i < nnp; i++){
ast p = conc(prem(new_proof,i));
@ -1452,9 +1537,11 @@ public:
lits.push_back(from_ast(con));
// pattern match some idioms
if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) {
res = iproof->make_axiom(lits);
return res;
if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){
if(get_locality_rec(prem(proof,1)) == INT_MAX) {
res = iproof->make_axiom(lits);
return res;
}
}
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
Iproof::node clause = translate_main(prem(proof,0),true);
@ -1465,12 +1552,20 @@ public:
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
std::cout << "foo!\n";
#if 0
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,0),true);
res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,1),true);
res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
#endif
if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
try {
res = CombineEqPropagate(proof);
@ -1495,6 +1590,27 @@ public:
return res;
}
/* This idiom takes ~P and Q=P, yielding ~Q. It uses a "rewrite"
(Q=false) = ~Q. We eliminate the rewrite by using symmetry,
congruence and modus ponens. */
if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_REWRITE && pr(prem(proof,0)) == PR_TRANSITIVITY && pr(prem(prem(proof,0),1)) == PR_IFF_FALSE){
if(op(con) == Not && arg(con,0) == arg(conc(prem(proof,0)),0)){
Iproof::node ante1 = translate_main(prem(prem(proof,0),0),false);
Iproof::node ante2 = translate_main(prem(prem(prem(proof,0),1),0),false);
ast ante1_con = conc(prem(prem(proof,0),0));
ast eq0 = arg(ante1_con,0);
ast eq1 = arg(ante1_con,1);
ast symm_con = make(Iff,eq1,eq0);
Iproof::node ante1s = iproof->make_symmetry(symm_con,ante1_con,ante1);
ast cong_con = make(Iff,make(Not,eq1),make(Not,eq0));
Iproof::node ante1sc = iproof->make_congruence(symm_con,cong_con,ante1s);
res = iproof->make_mp(cong_con,ante2,ante1sc);
return res;
}
}
// translate all the premises
std::vector<Iproof::node> args(nprems);
for(unsigned i = 0; i < nprems; i++)
@ -1627,9 +1743,10 @@ public:
break;
case ArrayTheory: {// nothing fancy for this
ast store_array;
if(!get_store_array(con,store_array))
throw unsupported();
res = iproof->make_axiom(lits,ast_scope(store_array));
if(get_store_array(con,store_array))
res = iproof->make_axiom(lits,ast_scope(store_array));
else
res = iproof->make_axiom(lits); // for array extensionality axiom
break;
}
default:
@ -1653,7 +1770,21 @@ public:
res = args[0];
break;
}
case PR_IFF_FALSE: { // turns ~p into p <-> false, noop for us
if(is_local(con))
res = args[0];
else
throw unsupported();
break;
}
case PR_COMMUTATIVITY: {
ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
ast pf = iproof->make_reflexivity(comm_equiv);
res = make(commute,pf,comm_equiv);
break;
}
default:
pfgoto(proof);
assert(0 && "translate_main: unsupported proof rule");
throw unsupported();
}

67
src/interp/iz3translate_direct.cpp
View file

@ -20,7 +20,7 @@ Revision History:
--*/
#ifdef WIN32
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
@ -42,11 +42,7 @@ Revision History:
#include <set>
//using std::vector;
#ifndef WIN32
using namespace stl_ext;
#endif
#ifndef WIN32
/* This can introduce an address dependency if the range type of hash_map has
a destructor. Since the code in this file is not used and only here for
@ -62,9 +58,6 @@ namespace stl_ext {
};
}
#endif
static int lemma_count = 0;
#if 0
static int nll_lemma_count = 0;
@ -96,38 +89,12 @@ namespace hash_space {
};
}
#ifdef WIN32
template <> inline
size_t stdext::hash_value<Z3_resolvent >(const Z3_resolvent& p)
{
std::hash<Z3_resolvent> h;
return h(p);
}
namespace std {
template <>
class less<Z3_resolvent > {
public:
bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const {
size_t ixproof = (size_t) x.proof.raw();
size_t iyproof = (size_t) y.proof.raw();
if(ixproof < iyproof) return true;
if(ixproof > iyproof) return false;
return x.pivot < y.pivot;
}
};
}
#else
bool operator==(const Z3_resolvent &x, const Z3_resolvent &y) {
return x.proof == y.proof && x.pivot == y.pivot;
}
#endif
typedef std::vector<Z3_resolvent *> ResolventAppSet;
@ -151,36 +118,6 @@ namespace hash_space {
};
}
#ifdef WIN32
template <> inline
size_t stdext::hash_value<non_local_lits >(const non_local_lits& p)
{
std::hash<non_local_lits> h;
return h(p);
}
namespace std {
template <>
class less<non_local_lits > {
public:
bool operator()(const non_local_lits &x, const non_local_lits &y) const {
ResolventAppSet::const_iterator itx = x.proofs.begin();
ResolventAppSet::const_iterator ity = y.proofs.begin();
while(true){
if(ity == y.proofs.end()) return false;
if(itx == x.proofs.end()) return true;
size_t xi = (size_t) *itx;
size_t yi = (size_t) *ity;
if(xi < yi) return true;
if(xi > yi) return false;
++itx; ++ity;
}
}
};
}
#else
bool operator==(const non_local_lits &x, const non_local_lits &y) {
ResolventAppSet::const_iterator itx = x.proofs.begin();
@ -194,8 +131,6 @@ bool operator==(const non_local_lits &x, const non_local_lits &y) {
}
#endif
/* This translator goes directly from Z3 proofs to interpolatable
proofs without an intermediate representation as an iz3proof. */

2
src/muz/base/fixedpoint_params.pyg
View file

@ -74,6 +74,8 @@ def_module_params('fixedpoint',
('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
('profile', BOOL, False, 'DUALITY: profile run time'),
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
))

4
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -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) {

72
src/muz/duality/duality_dl_interface.cpp Normal file → Executable file
View file

@ -64,20 +64,22 @@ namespace Duality {
std::vector<expr> clauses;
std::vector<std::vector<RPFP::label_struct> > clause_labels;
hash_map<RPFP::Edge *,int> map; // edges to clauses
Solver *old_rs;
Solver::Counterexample cex;
duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) {
ls = 0;
rpfp = 0;
status = StatusNull;
old_rs = 0;
}
~duality_data(){
if(old_rs)
dealloc(old_rs);
if(rpfp)
dealloc(rpfp);
if(ls)
dealloc(ls);
if(cex.tree)
delete cex.tree;
}
};
@ -132,15 +134,18 @@ lbool dl_interface::query(::expr * query) {
m_ctx.ensure_opened();
// if there is old data, get the cex and dispose (later)
Solver::Counterexample old_cex;
duality_data *old_data = _d;
if(old_data)
old_cex = old_data->cex;
Solver *old_rs = 0;
if(old_data){
old_rs = old_data->old_rs;
old_rs->GetCounterexample().swap(old_data->cex);
}
scoped_proof generate_proofs_please(m_ctx.get_manager());
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ctx.set("mbqi",m_ctx.get_params().mbqi());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
_d->rpfp = alloc(RPFP,_d->ls);
@ -195,8 +200,9 @@ lbool dl_interface::query(::expr * query) {
Solver *rs = Solver::Create("duality", _d->rpfp);
rs->LearnFrom(old_cex); // new solver gets hints from old cex
if(old_rs)
rs->LearnFrom(old_rs); // new solver gets hints from old solver
// set its options
IF_VERBOSE(1, rs->SetOption("report","1"););
rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0");
@ -204,6 +210,7 @@ lbool dl_interface::query(::expr * query) {
rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0");
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
unsigned rb = m_ctx.get_params().recursion_bound();
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
@ -229,15 +236,14 @@ lbool dl_interface::query(::expr * query) {
// save the result and counterexample if there is one
_d->status = ans ? StatusModel : StatusRefutation;
_d->cex = rs->GetCounterexample();
_d->cex.swap(rs->GetCounterexample()); // take ownership of cex
_d->old_rs = rs; // save this for later hints
if(old_data){
old_data->cex.tree = 0; // we own it now
dealloc(old_data);
dealloc(old_data); // this deallocates the old solver if there is one
}
dealloc(rs);
// dealloc(rs); this is now owned by data
// true means the RPFP problem is SAT, so the query is UNSAT
return ans ? l_false : l_true;
@ -265,18 +271,16 @@ void dl_interface::reset_statistics() {
static hash_set<func_decl> *local_func_decls;
static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) {
static void print_proof(dl_interface *d, std::ostream& out, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
RPFP::Node &node = *cex.root;
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
// first, prove the children (that are actually used)
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i])){
Solver::Counterexample foo = cex;
foo.root = edge.Children[i];
print_proof(d,out,foo);
if(!tree->Empty(edge.Children[i])){
print_proof(d,out,tree,edge.Children[i]);
}
}
@ -285,7 +289,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << "(step s!" << node.number;
out << " (" << node.Name.name();
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
out << " " << tree->Eval(&edge,edge.F.IndParams[i]);
out << ")\n";
// print the rule number
@ -307,8 +311,8 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
out << " (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = cex.tree->Localize(&edge,skolem);
out << " (= " << skolem << " " << tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
@ -316,7 +320,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << " (labels";
std::vector<symbol> labels;
cex.tree->GetLabels(&edge,labels);
tree->GetLabels(&edge,labels);
for(unsigned j = 0; j < labels.size(); j++){
out << " " << labels[j];
}
@ -328,7 +332,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << " (ref ";
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i]))
if(!tree->Empty(edge.Children[i]))
out << " s!" << edge.Children[i]->number;
else
out << " true";
@ -353,11 +357,11 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
// negation of the query is the last clause -- prove it
hash_set<func_decl> locals;
local_func_decls = &locals;
print_proof(this,out,_d->cex);
print_proof(this,out,_d->cex.get_tree(),_d->cex.get_root());
out << ")\n";
out << "(model \n\"";
::model mod(m_ctx.get_manager());
model orig_model = _d->cex.tree->dualModel;
model orig_model = _d->cex.get_tree()->dualModel;
for(unsigned i = 0; i < orig_model.num_consts(); i++){
func_decl cnst = orig_model.get_const_decl(i);
if(locals.find(cnst) == locals.end()){
@ -428,10 +432,10 @@ model_ref dl_interface::get_model() {
return md;
}
static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
static proof_ref extract_proof(dl_interface *d, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
ast_manager &mgr = ctx.m();
RPFP::Node &node = *cex.root;
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
RPFP::Edge *orig_edge = edge.map;
@ -453,21 +457,19 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
expr val = cex.tree->Eval(&edge,skolem);
expr val = tree->Eval(&edge,skolem);
expr_ref thing(ctx.uncook(val),mgr);
substs[0].push_back(thing);
expr local_skolem = cex.tree->Localize(&edge,skolem);
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
svector<std::pair<unsigned, unsigned> > pos;
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!cex.tree->Empty(edge.Children[i])){
if(!tree->Empty(edge.Children[i])){
pos.push_back(std::pair<unsigned,unsigned>(i+1,0));
Solver::Counterexample foo = cex;
foo.root = edge.Children[i];
proof_ref prem = extract_proof(d,foo);
proof_ref prem = extract_proof(d,tree,edge.Children[i]);
prems.push_back(prem);
substs.push_back(expr_ref_vector(mgr));
}
@ -476,7 +478,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
func_decl f = node.Name;
std::vector<expr> args;
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
args.push_back(cex.tree->Eval(&edge,edge.F.IndParams[i]));
args.push_back(tree->Eval(&edge,edge.F.IndParams[i]));
expr conc = f(args);
@ -493,7 +495,7 @@ proof_ref dl_interface::get_proof() {
if(_d->status == StatusRefutation){
hash_set<func_decl> locals;
local_func_decls = &locals;
return extract_proof(this,_d->cex);
return extract_proof(this,_d->cex.get_tree(),_d->cex.get_root());
}
else
return proof_ref(m_ctx.get_manager());

8
src/parsers/smt2/smt2parser.cpp
View file

@ -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());

2
src/shell/main.cpp
View file

@ -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";

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

@ -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 {

12
src/smt/smt_quantifier.cpp
View file

@ -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

7
src/smt/smt_setup.cpp
View file

@ -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));

111
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -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;
}
};

236
src/smt/theory_horn_ineq.cpp
View file

@ -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;
}
}

328
src/smt/theory_horn_ineq.h
View file

@ -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_ */

1166
src/smt/theory_horn_ineq_def.h
View file

File diff suppressed because it is too large Load diff

60
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -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););

4
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -1368,12 +1368,12 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
not_f_sgn = m_bv_util.mk_bv_not(f_sgn);
not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv);
res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv);
res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs);
sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);

16
src/tactic/fpa/qffpa_tactic.cpp
View file

@ -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();
}

92
src/tactic/sls/sls_compilation_settings.h
View file

@ -22,20 +22,10 @@ Notes:
#ifndef _SLS_COMPILATION_SETTINGS_H_
#define _SLS_COMPILATION_SETTINGS_H_
// which unsatisfied assertion is selected? only works with _FOCUS_ > 0
// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
#define _BFS_ 0
// how many terms are considered for variable selection?
// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom
// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT)
#define _FOCUS_ 1
// probability of choosing the same assertion again in the next step
#define _PERC_STICKY_ 0
// do we use dirty unit propagation to get rid of nested top level assertions?
#define _DIRTY_UP_ 0
// shall we use additive weighting scheme?
#define _PAWS_ 5
#define _PAWS_INIT_ 40
@ -45,7 +35,7 @@ Notes:
#define _RESTARTS_ 1
// limit of moves/plateaus/seconds until first restart occurs
#define _RESTART_LIMIT_ 100
// 0 = initialize with all zero, 1 initialize with random value
//// 0 = initialize with all zero, 1 initialize with random value
#define _RESTART_INIT_ 0
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
#define _RESTART_SCHEME_ 1
@ -58,13 +48,6 @@ Notes:
// should score of conjunctions be calculated by average rather than max?
#define _SCORE_AND_AVG_ 0
// should score of discunctions be calculated by multiplication of the inverse score rather than min?
#define _SCORE_OR_MUL_ 0
// do we use some kind of variable neighbourhood-search?
// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained
#define _VNS_ 0
// shall we check 2-bit flips in plateaus using Monte Carlo?
#define _VNS_MC_ 0
@ -74,33 +57,13 @@ Notes:
// shall we check another assertion if no improving step was found in the first one?
#define _VNS_REPICK_ 0
// what is the probability of doing so (percentage)?
#define _VNS_PERC_ 100
// do a decreasing move with percentage ...
#define _INSIST_PERC_ 0
// do we reduce the score of unsatisfied literals?
// 0 = no
// 1 = yes, by multiplying it with some factor
// 2 = yes, by squaring it
// 3 = yes, by setting it to zero
// 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!)
// 0 = no, 1 = yes, by multiplying it with some factor
#define _WEIGHT_DIST_ 1
// the factor used for _WEIGHT_DIST_ = 1
#define _WEIGHT_DIST_FACTOR_ 0.5
// shall we toggle the weight after each restart?
#define _WEIGHT_TOGGLE_ 0
// do we use intensification steps in local minima? if so, how many?
#define _INTENSIFICATION_ 0
#define _INTENSIFICATION_TRIES_ 0
// what is the percentage of random moves in plateaus (instead of full randomization)?
#define _PERC_PLATEAU_MOVES_ 0
// shall we repick assertion when randomizing in a plateau or use the current one?
// 0 = use old one, 1 = repick according to usual scheme, 2 = repick randomly and force different one
#define _REPICK_ 1
@ -111,16 +74,6 @@ Notes:
// how much diversification is used in the UCT-scheme?
#define _UCT_CONSTANT_ 20.0
// is uct clause selection probabilistic similar to variable selection in sparrow?
// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score
#define _PROBABILISTIC_UCT_ 0
// additive constants for probabilistic uct > 0
#define _UCT_EPS_ 0.0001
// shall we reset _UCT_ touched values after restart?
#define _UCT_RESET_ 0
// how shall we initialize the _UCT_ total touched counter?
// 0 = initialize with one, 1 = initialize with number of assertions
#define _UCT_INIT_ 0
@ -132,32 +85,8 @@ Notes:
// shall we use addition/subtraction?
#define _USE_ADDSUB_ 1
// shall we try multilication and division by 2?
#define _USE_MUL2DIV2_ 0
// shall we try multiplication by 3?
#define _USE_MUL3_ 0
// shall we try unary minus (= inverting and incrementing)
#define _USE_UNARY_MINUS_ 0
// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0
#define _UNIFORM_RANDOM_ 0
// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
#define _REAL_RS_ 0
#define _REAL_PBFS_ 0
// how many bits do we neglect in each iteration?
#define _SKIP_BITS_ 0
// when randomizing local, what is the probability for changing a single bit?
// 0 = use standard scheme and pick a new value at random (= 50), otherwise the value (as int) gives the percentage
#define _PERC_CHANGE_ 0
// do we use random steps for noise?
// 0 = no, 1 = randomize local, 2 = make random move
#define _TYPE_RSTEP_ 0
// with what probability _PERM_STEP_/1000 will the random step happen?
#define _PERM_RSTEP_ 0
@ -168,20 +97,7 @@ Notes:
// shall we use caching for top_score?
#define _CACHE_TOP_SCORE_ 1
#if ((_BFS_ > 0) + (_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1)
InvalidConfiguration;
#endif
#if (_PROBABILISTIC_UCT_ && !_UCT_)
InvalidConfiguration;
#endif
#if (_PERM_RSTEP_ && !_TYPE_RSTEP_)
InvalidConfiguration;
#endif
#if (_PERC_CHANGE_ == 50)
InvalidConfiguration;
#endif
#if (_PERC_STICKY_ && !_FOCUS_)
#if ((_UCT_ > 0) + _REAL_RS_ > 1)
InvalidConfiguration;
#endif

1003
src/tactic/sls/sls_engine.cpp
View file

File diff suppressed because it is too large Load diff

76
src/tactic/sls/sls_engine.h
View file

@ -22,6 +22,7 @@ Notes:
#include"stopwatch.h"
#include"lbool.h"
#include"model_converter.h"
#include"goal.h"
#include"sls_compilation_settings.h"
#include"sls_tracker.h"
@ -35,17 +36,13 @@ public:
stopwatch m_stopwatch;
unsigned m_full_evals;
unsigned m_incr_evals;
unsigned m_moves, m_flips, m_incs, m_decs, m_invs, m_umins, m_mul2s, m_mul3s, m_div2s;
unsigned m_moves, m_flips, m_incs, m_decs, m_invs;
stats() :
m_restarts(0),
m_full_evals(0),
m_incr_evals(0),
m_moves(0),
m_umins(0),
m_mul2s(0),
m_mul3s(0),
m_div2s(0),
m_flips(0),
m_incs(0),
m_decs(0),
@ -71,6 +68,7 @@ protected:
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
ptr_vector<expr> m_assertions;
unsigned m_restart_limit;
unsigned m_max_restarts;
@ -78,7 +76,7 @@ protected:
ptr_vector<mpz> m_old_values;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
public:
sls_engine(ast_manager & m, params_ref const & p);
@ -92,78 +90,46 @@ public:
void updt_params(params_ref const & _p);
void assert_expr(expr * e) { m_assertions.push_back(e); }
stats const & get_stats(void) { return m_stats; }
void reset_statistics(void) { m_stats.reset(); }
bool full_eval(goal_ref const & g, model & mdl);
bool full_eval(model & mdl);
void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result);
void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result);
void mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result);
void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented);
void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented);
void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);
void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);
double find_best_move(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_lsb(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_mc(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value);
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i);
double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i);
lbool search(goal_ref const & g);
lbool search(void);
lbool operator()();
void operator()(goal_ref const & g, model_converter_ref & mc);
protected:
void checkpoint();
lbool search_old(goal_ref const & g);
double get_restart_armin(unsigned cnt_restarts);
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
bool what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value);
double top_score();
double rescore();
double serious_score(func_decl * fd, const mpz & new_value);
double incremental_score(func_decl * fd, const mpz & new_value);
bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double incremental_score_prune(func_decl * fd, const mpz & new_value);
double find_best_move(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double top_score(goal_ref const & g);
double rescore(goal_ref const & g);
double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
#if _EARLY_PRUNE_
double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value);
#endif
double find_best_move_vns(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
void mk_random_move(goal_ref const & g);
bool handle_plateau(goal_ref const & g);
bool handle_plateau(goal_ref const & g, double old_score);
inline unsigned check_restart(unsigned curr_value);
};
#endif
#endif

91
src/tactic/sls/sls_evaluator.h
View file

@ -559,8 +559,7 @@ public:
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
#if _REAL_RS_ || _REAL_PBFS_
//if (!m_tracker.has_uplinks(cur))
#if _REAL_RS_
if (m_tracker.is_top_expr(cur))
{
if (m_mpz_manager.eq(new_value,m_one))
@ -573,7 +572,6 @@ public:
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
@ -582,7 +580,6 @@ public:
#else
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
@ -633,7 +630,6 @@ public:
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
@ -642,7 +638,6 @@ public:
#else
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
@ -684,7 +679,7 @@ public:
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
#if _REAL_RS_ || _PAWS_
run_serious_update(max_depth);
#else
run_update(max_depth);
@ -728,7 +723,6 @@ public:
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
@ -736,10 +730,8 @@ public:
m_tracker.set_score(cur, new_score);
if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur)))
//if ((new_score >= prune_score) && (m_tracker.has_pos_occ(cur)))
pot_benefits = 1;
if ((new_score <= prune_score) && (m_tracker.has_neg_occ(cur)))
//if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur)))
pot_benefits = 1;
if (m_tracker.has_uplinks(cur)) {
@ -772,7 +764,6 @@ public:
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
@ -874,7 +865,6 @@ public:
expr * cur = cur_depth_exprs[i];
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
prune_score = m_tracker.get_score_prune(cur);
@ -914,7 +904,6 @@ public:
expr * cur = cur_depth_exprs[i];
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
@ -960,60 +949,19 @@ public:
}
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
// Randomize _all_ candidates:
//// bool did_something = false;
//for (unsigned i = 0; i < unsat_constants.size(); i++) {
// func_decl * fd = unsat_constants[i];
// mpz temp = m_tracker.get_random(fd->get_range());
// // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) {
// // did_something = true;
// // }
// update(fd, temp);
// m_mpz_manager.del(temp);
//}
// Randomize _one_ candidate:
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
#if _PERC_CHANGE_
sort * srt = fd->get_range();
mpz temp;
if (m_manager.is_bool(srt))
m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
else
{
mpz temp2, mask;
unsigned bv_sz = m_bv_util.get_bv_size(srt);
m_mpz_manager.set(temp, m_tracker.get_value(fd));
for (unsigned bit = 0; bit < bv_sz; bit++)
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
{
m_mpz_manager.set(mask, m_powers(bit));
m_mpz_manager.bitwise_xor(temp, mask, temp2);
m_mpz_manager.set(temp, temp2);
}
m_mpz_manager.del(mask);
m_mpz_manager.del(temp2);
}
#else
mpz temp = m_tracker.get_random(fd->get_range());
#endif
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
#if _REAL_RS_ || _PAWS_
serious_update(fd, temp);
#else
update(fd, temp);
#endif
m_mpz_manager.del(temp);
TRACE("sls", /*tout << "Randomization candidates: ";
for (unsigned i = 0; i < unsat_constants.size(); i++)
tout << unsat_constants[i]->get_name() << ", ";
tout << std::endl;*/
tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
tout << "Locally randomized model: " << std::endl;
m_tracker.show_model(tout); );
@ -1023,36 +971,9 @@ public:
randomize_local(m_tracker.get_constants(e));
}
void randomize_local(goal_ref const & g, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(g, flip));
void randomize_local(ptr_vector<expr> const & as) {
randomize_local(m_tracker.get_unsat_constants(as));
}
void randomize_local_n(goal_ref const & g, ptr_vector<func_decl> & unsat_constants) {
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
sort * srt = fd->get_range();
unsigned bv_sz = m_manager.is_bool(srt) ? 1 : m_bv_util.get_bv_size(srt);
mpz max_val = m_tracker.get_random(srt);
update(fd, max_val);
double max_score = m_tracker.get_top_sum() / g->size();
mpz temp_val;
double temp_score;
for (unsigned i = 1; i < 2; i++)
//for (unsigned i = 1; i < bv_sz; i++)
{
m_mpz_manager.set(temp_val, m_tracker.get_random(srt));
update(fd, temp_val);
temp_score = m_tracker.get_top_sum() / g->size();
if (temp_score > max_score)
{
m_mpz_manager.set(max_val, temp_val);
max_score = temp_score;
}
}
update(fd, max_val);
m_mpz_manager.del(temp_val);
m_mpz_manager.del(max_val);
}
};
#endif

800
src/tactic/sls/sls_tracker.h
View file

File diff suppressed because it is too large Load diff

2
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -28,8 +28,6 @@ Notes:
#include"bv_size_reduction_tactic.h"
#include"aig_tactic.h"
#include"sat_tactic.h"
//#include"nnf_tactic.h"
//#include"sls_tactic.h"
#define MEMLIMIT 300

38
src/util/rational.h
View file

@ -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_ */