mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Merge pull request #1606 from NikolajBjorner/opt

Browse source 
This integrates several features and improvements to the SAT and finite domain solver.

- The SAT solver by default handle cardinality and PB constraints using a custom plugin that operates directly on cardinality and PB constraints.
- A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal.
- A "cube" interface is exposed over the solver API. 
- Model conversion is first class over the textual API, such that subgoals created from running a solver can be passed in text files and a model for the original formula can be recreated from the result.
- This has also led to changes in how models are tracked over tactic subgoals. The API for extracting models from apply_result have been replaced.
- An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated.
- The SAT solver includes new inprocessing technques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.

- A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of formulas as opposed to a conjunction of formulas. The vector of formulas correspond to the set of "assert" instructions in the SMT-LIB input.
This commit is contained in:
Nikolaj Bjorner 2018-05-23 08:47:08 -07:00 • committed by GitHub
commit 75eba45926
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
378 changed files with 29494 additions and 6481 deletions
Download patch file Download diff file Expand all files Collapse all files

4
CMakeLists.txt
View file

@ -33,8 +33,8 @@ endif()
# Project version
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 7)
set(Z3_VERSION_PATCH 1)
set(Z3_VERSION_MINOR 8)
set(Z3_VERSION_PATCH 0)
set(Z3_VERSION_TWEAK 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified

6
contrib/cmake/src/test/lp/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
add_executable(lp_tst lp_main.cpp lp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat> $<TARGET_OBJECTS:lp> )
target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS})
z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})

6
examples/c++/example.cpp
View file

@ -470,7 +470,7 @@ void unsat_core_example2() {
// The solver s already contains p1 => F
// To disable F, we add (not p1) as an additional assumption
qs.push_back(!p1);
std::cout << s.check((unsigned)qs.size(), &qs[0]) << "\n";
std::cout << s.check(static_cast<unsigned>(qs.size()), &qs[0]) << "\n";
expr_vector core2 = s.unsat_core();
std::cout << core2 << "\n";
std::cout << "size: " << core2.size() << "\n";
@ -707,7 +707,7 @@ void tactic_example7() {
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << "model for subgoal:\n" << m << "\n";
std::cout << "model for original goal:\n" << r.convert_model(m) << "\n";
std::cout << "model for original goal:\n" << subgoal.convert_model(m) << "\n";
}
void tactic_example8() {
@ -1149,7 +1149,7 @@ static void parse_example() {
func_decl_vector decls(c);
sort B = c.bool_sort();
decls.push_back(c.function("a", 0, 0, B));
expr a = c.parse_string("(assert a)", sorts, decls);
expr_vector a = c.parse_string("(assert a)", sorts, decls);
std::cout << a << "\n";
// expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");

30
examples/c/test_capi.c
View file

@ -378,7 +378,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
{
Z3_sort t;
Z3_symbol f_name, t_name;
Z3_ast q;
Z3_ast_vector q;
t = Z3_get_range(ctx, f);
@ -394,13 +394,14 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
/* Inside the parser, type t will be referenced using the symbol 'T'. */
t_name = Z3_mk_string_symbol(ctx, "T");
q = Z3_parse_smtlib2_string(ctx,
"(assert (forall ((x T) (y T)) (= (f x y) (f y x))))",
1, &t_name, &t,
1, &f_name, &f);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
Z3_solver_assert(ctx, s, q);
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q));
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) {
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i));
}
}
/**
@ -1642,7 +1643,7 @@ void parser_example2()
Z3_ast x, y;
Z3_symbol names[2];
Z3_func_decl decls[2];
Z3_ast f;
Z3_ast_vector f;
printf("\nparser_example2\n");
LOG_MSG("parser_example2");
@ -1665,8 +1666,11 @@ void parser_example2()
0, 0, 0,
/* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */
2, names, decls);
printf("formula: %s\n", Z3_ast_to_string(ctx, f));
Z3_solver_assert(ctx, s, f);
printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f));
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f));
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) {
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i));
}
check(ctx, s, Z3_L_TRUE);
del_solver(ctx, s);
@ -1685,7 +1689,7 @@ void parser_example3()
Z3_symbol g_name;
Z3_sort g_domain[2];
Z3_func_decl g;
Z3_ast thm;
Z3_ast_vector thm;
printf("\nparser_example3\n");
LOG_MSG("parser_example3");
@ -1710,8 +1714,8 @@ void parser_example3()
"(assert (forall ((x Int) (y Int)) (=> (= x y) (= (g x 0) (g 0 y)))))",
0, 0, 0,
1, &g_name, &g);
printf("formula: %s\n", Z3_ast_to_string(ctx, thm));
prove(ctx, s, thm, Z3_TRUE);
printf("formula: %s\n", Z3_ast_vector_to_string(ctx, thm));
prove(ctx, s, Z3_ast_vector_get(ctx, thm, 0), Z3_TRUE);
del_solver(ctx, s);
Z3_del_context(ctx);
@ -2576,13 +2580,15 @@ void reference_counter_example() {
*/
void smt2parser_example() {
Z3_context ctx;
Z3_ast fs;
Z3_ast_vector fs;
printf("\nsmt2parser_example\n");
LOG_MSG("smt2parser_example");
ctx = mk_context();
fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0);
printf("formulas: %s\n", Z3_ast_to_string(ctx, fs));
Z3_ast_vector_inc_ref(ctx, fs);
printf("formulas: %s\n", Z3_ast_vector_to_string(ctx, fs));
Z3_ast_vector_dec_ref(ctx, fs);
Z3_del_context(ctx);
}

19
examples/dotnet/Program.cs
View file

@ -175,7 +175,7 @@ namespace test_mapi
string bench = string.Format("(assert (forall ((x {0}) (y {1})) (= ({2} x y) ({3} y x))))",
t.Name, t.Name, f.Name, f.Name);
return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f });
return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f })[0];
}
/// <summary>
@ -322,7 +322,6 @@ namespace test_mapi
Status q = s.Check();
Console.WriteLine("Solver says: " + q);
Console.WriteLine("Model: \n" + s.Model);
Console.WriteLine("Converted Model: \n" + ar.ConvertModel(0, s.Model));
if (q != Status.SATISFIABLE)
throw new TestFailedException();
}
@ -612,7 +611,6 @@ namespace test_mapi
Expr f_x = ctx.MkApp(f, x);
Expr f_y = ctx.MkApp(f, y);
Expr g_y = ctx.MkApp(g, y);
Pattern[] pats = new Pattern[] { ctx.MkPattern(new Expr[] { f_x, g_y }) };
Expr[] no_pats = new Expr[] { f_y };
Expr[] bound = new Expr[2] { x, y };
Expr body = ctx.MkAnd(ctx.MkEq(f_x, f_y), ctx.MkEq(f_y, g_y));
@ -629,7 +627,6 @@ namespace test_mapi
Expr f_x = ctx.MkApp(f, x);
Expr f_y = ctx.MkApp(f, y);
Expr g_y = ctx.MkApp(g, y);
Pattern[] pats = new Pattern[] { ctx.MkPattern(new Expr[] { f_x, g_y }) };
Expr[] no_pats = new Expr[] { f_y };
Symbol[] names = new Symbol[] { ctx.MkSymbol("x"), ctx.MkSymbol("y") };
Sort[] sorts = new Sort[] { ctx.IntSort, ctx.IntSort };
@ -730,7 +727,6 @@ namespace test_mapi
{
Console.WriteLine("BasicTests");
Symbol qi = ctx.MkSymbol(1);
Symbol fname = ctx.MkSymbol("f");
Symbol x = ctx.MkSymbol("x");
Symbol y = ctx.MkSymbol("y");
@ -977,7 +973,8 @@ namespace test_mapi
using (Context ctx = new Context(new Dictionary<string, string>() { { "MODEL", "true" } }))
{
Expr a = ctx.ParseSMTLIB2File(filename);
BoolExpr[] fmls = ctx.ParseSMTLIB2File(filename);
BoolExpr a = ctx.MkAnd(fmls);
Console.WriteLine("SMT2 file read time: " + (System.DateTime.Now - before).TotalSeconds + " sec");
@ -1319,7 +1316,7 @@ namespace test_mapi
new Sort[] { int_type, int_type } // types of projection operators
);
FuncDecl first = tuple.FieldDecls[0]; // declarations are for projections
FuncDecl second = tuple.FieldDecls[1];
// FuncDecl second = tuple.FieldDecls[1];
Expr x = ctx.MkConst("x", int_type);
Expr y = ctx.MkConst("y", int_type);
Expr n1 = tuple.MkDecl[x, y];
@ -1383,7 +1380,9 @@ namespace test_mapi
{
Console.WriteLine("ParserExample1");
var fml = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
var fmls = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
var fml = ctx.MkAnd(fmls);
Console.WriteLine("formula {0}", fml);
Model m = Check(ctx, fml, Status.SATISFIABLE);
@ -1399,7 +1398,7 @@ namespace test_mapi
FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort());
FuncDecl b = ctx.MkConstDecl(declNames[1], ctx.MkIntSort());
FuncDecl[] decls = new FuncDecl[] { a, b };
BoolExpr f = ctx.ParseSMTLIB2String("(assert (> a b))", null, null, declNames, decls);
BoolExpr f = ctx.ParseSMTLIB2String("(assert (> a b))", null, null, declNames, decls)[0];
Console.WriteLine("formula: {0}", f);
Check(ctx, f, Status.SATISFIABLE);
}
@ -1420,7 +1419,7 @@ namespace test_mapi
BoolExpr thm = ctx.ParseSMTLIB2String("(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
null, null,
new Symbol[] { ctx.MkSymbol("gg") },
new FuncDecl[] { g });
new FuncDecl[] { g })[0];
Console.WriteLine("formula: {0}", thm);
Prove(ctx, thm, false, ca);

14
examples/java/JavaExample.java
View file

@ -167,12 +167,12 @@ class JavaExample
"function must be binary, and argument types must be equal to return type");
}
String bench = "(benchmark comm :formula (forall (x " + t.getName()
String bench = "(assert (forall (x " + t.getName()
+ ") (y " + t.getName() + ") (= (" + f.getName() + " x y) ("
+ f.getName() + " y x))))";
return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
new Sort[] { t }, new Symbol[] { f.getName() },
new FuncDecl[] { f });
new FuncDecl[] { f })[0];
}
// / "Hello world" example: create a Z3 logical context, and delete it.
@ -344,8 +344,6 @@ class JavaExample
Status q = s.check();
System.out.println("Solver says: " + q);
System.out.println("Model: \n" + s.getModel());
System.out.println("Converted Model: \n"
+ ar.convertModel(0, s.getModel()));
if (q != Status.SATISFIABLE)
throw new TestFailedException();
}
@ -1041,7 +1039,7 @@ class JavaExample
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
Expr a = ctx.parseSMTLIB2File(filename, null, null, null, null);
BoolExpr a = ctx.mkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null));
long t_diff = ((new Date()).getTime() - before.getTime()) / 1000;
@ -1445,7 +1443,7 @@ class JavaExample
BoolExpr f = ctx.parseSMTLIB2String(
"(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
null, null, null, null);
null, null, null, null)[0];
System.out.println("formula " + f);
@SuppressWarnings("unused")
@ -1465,7 +1463,7 @@ class JavaExample
FuncDecl[] decls = new FuncDecl[] { a, b };
BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
declNames, decls);
declNames, decls)[0];
System.out.println("formula: " + f);
check(ctx, f, Status.SATISFIABLE);
}
@ -1486,7 +1484,7 @@ class JavaExample
BoolExpr thm = ctx.parseSMTLIB2String(
"(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
null, null, new Symbol[] { ctx.mkSymbol("gg") },
new FuncDecl[] { g });
new FuncDecl[] { g })[0];
System.out.println("formula: " + thm);
prove(ctx, thm, false, ca);
}

2
examples/python/all_interval_series.py
View file

@ -8,6 +8,8 @@ from __future__ import print_function
from z3 import *
import time
set_option("sat.gc.burst", False) # disable GC at every search. It is wasteful for these small queries.
def diff_at_j_is_i(xs, j, i):
assert(0 <= j and j + 1 < len(xs))
assert(1 <= i and i < len(xs))

5
examples/tptp/tptp5.cpp
View file

@ -2203,9 +2203,8 @@ static void check_error(z3::context& ctx) {
static void display_tptp(std::ostream& out) {
// run SMT2 parser, pretty print TFA format.
z3::context ctx;
Z3_ast _fml = Z3_parse_smtlib2_file(ctx, g_input_file, 0, 0, 0, 0, 0, 0);
check_error(ctx);
z3::expr fml(ctx, _fml);
z3::expr_vector fmls = ctx.parse_file(g_input_file);
z3::expr fml = z3::mk_and(fmls);
pp_tptp pp(ctx);
pp.collect_decls(fml);

7
scripts/mk_project.py
View file

@ -9,12 +9,12 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 7, 1, 0)
set_version(4, 8, 0, 0)
add_lib('util', [])
add_lib('lp', ['util'], 'util/lp')
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
add_lib('nlsat', ['polynomial', 'sat'])
add_lib('lp', ['util','nlsat'], 'util/lp')
add_lib('hilbert', ['util'], 'math/hilbert')
add_lib('simplex', ['util'], 'math/simplex')
add_lib('automata', ['util'], 'math/automata')
@ -69,10 +69,9 @@ def init_project_def():
add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf')
add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf', 'spacer'], 'muz/fp')
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')

1
scripts/mk_util.py
View file

@ -2809,6 +2809,7 @@ def get_header_files_for_components(component_src_dirs):
def mk_install_tactic_cpp(cnames, path):
component_src_dirs = []
for cname in cnames:
print("Component %s" % cname)
c = get_component(cname)
component_src_dirs.append(c.src_dir)
h_files_full_path = get_header_files_for_components(component_src_dirs)

3
scripts/vsts-mac.sh
View file

@ -15,5 +15,4 @@ make c_example
git clone https://github.com/z3prover/z3test.git z3test
ls
python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2
python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2

9
src/CMakeLists.txt
View file

@ -36,10 +36,10 @@ endforeach()
# raised if you try to declare a component is dependent on another component
# that has not yet been declared.
add_subdirectory(util)
add_subdirectory(util/lp)
add_subdirectory(math/polynomial)
add_subdirectory(sat)
add_subdirectory(nlsat)
add_subdirectory(util/lp)
add_subdirectory(math/hilbert)
add_subdirectory(math/simplex)
add_subdirectory(math/automata)
@ -56,12 +56,12 @@ add_subdirectory(parsers/util)
add_subdirectory(math/grobner)
add_subdirectory(math/euclid)
add_subdirectory(tactic/core)
add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
add_subdirectory(math/subpaving/tactic)
add_subdirectory(tactic/aig)
add_subdirectory(solver)
add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
add_subdirectory(ackermannization)
add_subdirectory(interp)
add_subdirectory(cmd_context)
@ -92,7 +92,6 @@ add_subdirectory(muz/ddnf)
add_subdirectory(muz/duality)
add_subdirectory(muz/spacer)
add_subdirectory(muz/fp)
add_subdirectory(tactic/nlsat_smt)
add_subdirectory(tactic/ufbv)
add_subdirectory(sat/sat_solver)
add_subdirectory(tactic/smtlogics)

14
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -29,12 +29,7 @@ public:
~ackermannize_bv_tactic() override { }
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
mc = nullptr;
void operator()(goal_ref const & g, goal_ref_buffer & result) override {
tactic_report report("ackermannize", *g);
fail_if_unsat_core_generation("ackermannize", g);
fail_if_proof_generation("ackermannize", g);
@ -52,17 +47,14 @@ public:
TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;);
result.reset();
result.push_back(g.get());
mc = nullptr;
pc = nullptr;
core = nullptr;
return;
}
result.push_back(resg.get());
// report model
if (g->models_enabled()) {
mc = mk_ackermannize_bv_model_converter(m, lackr.get_info());
resg->add(mk_ackermannize_bv_model_converter(m, lackr.get_info()));
}
resg->inc_depth();
TRACE("ackermannize", resg->display(tout << "out\n"););
SASSERT(resg->is_well_sorted());

12
src/ackermannization/ackr_model_converter.cpp
View file

@ -39,8 +39,9 @@ public:
~ackr_model_converter() override { }
void operator()(model_ref & md, unsigned goal_idx) override {
SASSERT(goal_idx == 0);
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void operator()(model_ref & md) override {
SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
model_ref& old_model = fixed_model ? abstr_model : md;
SASSERT(old_model.get());
@ -49,8 +50,6 @@ public:
md = new_model;
}
void operator()(model_ref & md) override { operator()(md, 0); }
model_converter * translate(ast_translation & translator) override {
ackr_info_ref retv_info = info->translate(translator);
if (fixed_model) {
@ -62,6 +61,10 @@ public:
}
}
void display(std::ostream & out) override {
out << "(ackr-model-converter)\n";
}
protected:
ast_manager & m;
const ackr_info_ref info;
@ -144,6 +147,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
else {
TRACE("ackr_model", tout << "entry already present\n";);
}
}
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) {

12
src/ackermannization/lackr_model_converter_lazy.cpp
View file

@ -30,8 +30,7 @@ public:
~lackr_model_converter_lazy() override { }
void operator()(model_ref & md, unsigned goal_idx) override {
SASSERT(goal_idx == 0);
void operator()(model_ref & md) override {
SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
SASSERT(model_constructor.get());
model * new_model = alloc(model, m);
@ -39,15 +38,18 @@ public:
model_constructor->make_model(md);
}
void operator()(model_ref & md) override {
operator()(md, 0);
}
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
//void display(std::ostream & out);
model_converter * translate(ast_translation & translator) override {
NOT_IMPLEMENTED_YET();
}
void display(std::ostream & out) override {
out << "(lackr-model-converter)\n";
}
protected:
ast_manager& m;
const lackr_model_constructor_ref model_constructor;

2
src/api/api_context.h
View file

@ -114,7 +114,7 @@ namespace api {
~context();
ast_manager & m() const { return *(m_manager.get()); }
context_params & params() { return m_params; }
context_params & params() { m_params.updt_params(); return m_params; }
scoped_ptr<cmd_context>& cmd() { return m_cmd; }
bool produce_proofs() const { return m().proofs_enabled(); }
bool produce_models() const { return m_params.m_model; }

29
src/api/api_goal.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "api/api_context.h"
#include "api/api_goal.h"
#include "ast/ast_translation.h"
#include "api/api_model.h"
extern "C" {
@ -151,6 +152,20 @@ extern "C" {
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) {
Z3_TRY;
LOG_Z3_goal_convert_model(c, g, m);
RESET_ERROR_CODE();
model_ref new_m;
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
mk_c(c)->save_object(m_ref);
if (m) m_ref->m_model = to_model_ref(m)->copy();
if (to_goal_ref(g)->mc())
(*to_goal_ref(g)->mc())(m_ref->m_model);
RETURN_Z3(of_model(m_ref));
Z3_CATCH_RETURN(0);
}
Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) {
Z3_TRY;
LOG_Z3_goal_translate(c, g, target);
@ -178,4 +193,18 @@ extern "C" {
Z3_CATCH_RETURN("");
}
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g) {
Z3_TRY;
LOG_Z3_goal_to_dimacs_string(c, g);
RESET_ERROR_CODE();
std::ostringstream buffer;
to_goal_ref(g)->display_dimacs(buffer);
// Hack for removing the trailing '\n'
std::string result = buffer.str();
SASSERT(result.size() > 0);
result.resize(result.size()-1);
return mk_c(c)->mk_external_string(result);
Z3_CATCH_RETURN("");
}
};

51
src/api/api_interp.cpp
View file

@ -506,10 +506,11 @@ extern "C" {
static std::string read_msg;
static std::vector<Z3_ast> read_theory;
static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector<Z3_ast> &assertions){
static Z3_ast_vector iZ3_parse(Z3_context ctx, const char *filename, const char ** error){
return nullptr;
#if 0
read_error.clear();
try {
std::string foo(filename);
Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, nullptr, nullptr, 0, nullptr, nullptr);
Z3_app app = Z3_to_app(ctx, assrts);
int nconjs = Z3_get_app_num_args(ctx, app);
@ -521,47 +522,42 @@ extern "C" {
read_error << "SMTLIB parse error: " << Z3_get_parser_error(ctx);
read_msg = read_error.str();
*error = read_msg.c_str();
return false;
return nullptr;
}
Z3_set_error_handler(ctx, nullptr);
return true;
return nullptr;
#endif
}
int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast *cnsts[], unsigned *parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast *theory[]){
int Z3_read_interpolation_problem(Z3_context ctx, Z3_ast_vector cnsts, unsigned* _num, unsigned* parents[], const char *filename, Z3_string_ptr error, Z3_ast_vector theory){
hash_map<std::string, std::string> file_params;
get_file_params(filename, file_params);
unsigned num_theory = 0;
if (file_params.find("THEORY") != file_params.end())
if (file_params.find("THEORY") != file_params.end()) {
num_theory = atoi(file_params["THEORY"].c_str());
}
svector<Z3_ast> assertions;
if (!iZ3_parse(ctx, filename, error, assertions))
Z3_ast_vector assertions = iZ3_parse(ctx, filename, error);
if (assertions == 0)
return false;
if (num_theory > assertions.size())
num_theory = assertions.size();
unsigned num = assertions.size() - num_theory;
if (num_theory > Z3_ast_vector_size(ctx, assertions))
num_theory = Z3_ast_vector_size(ctx, assertions);
unsigned num = Z3_ast_vector_size(ctx, assertions) - num_theory;
read_cnsts.resize(num);
read_parents.resize(num);
read_theory.resize(num_theory);
for (unsigned j = 0; j < num_theory; j++)
read_theory[j] = assertions[j];
for (unsigned j = 0; theory && j < num_theory; j++)
Z3_ast_vector_push(ctx, theory, Z3_ast_vector_get(ctx, assertions, j));
for (unsigned j = 0; j < num; j++)
read_cnsts[j] = assertions[j + num_theory];
if (ret_num_theory)
*ret_num_theory = num_theory;
if (theory)
*theory = &read_theory[0];
Z3_ast_vector_push(ctx, cnsts, Z3_ast_vector_get(ctx, assertions, j + num_theory));
if (!parents){
*_num = num;
*cnsts = &read_cnsts[0];
Z3_ast_vector_dec_ref(ctx, assertions);
return true;
}
@ -571,7 +567,7 @@ extern "C" {
hash_map<Z3_ast, int> pred_map;
for (unsigned j = 0; j < num; j++){
Z3_ast lhs = nullptr, rhs = read_cnsts[j];
Z3_ast lhs = nullptr, rhs = Z3_ast_vector_get(ctx, cnsts, j);
if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, rhs))) == Z3_OP_IMPLIES){
Z3_app app1 = Z3_to_app(ctx, rhs);
@ -612,7 +608,7 @@ extern "C" {
read_error << "formula " << j + 1 << ": should be (implies {children} fmla parent)";
goto fail;
}
read_cnsts[j] = lhs;
Z3_ast_vector_set(ctx, cnsts, j, lhs);
Z3_ast name = rhs;
if (pred_map.find(name) != pred_map.end()){
read_error << "formula " << j + 1 << ": duplicate symbol";
@ -631,11 +627,12 @@ extern "C" {
}
*_num = num;
*cnsts = &read_cnsts[0];
*parents = &read_parents[0];
Z3_ast_vector_dec_ref(ctx, assertions);
return true;
fail:
Z3_ast_vector_dec_ref(ctx, assertions);
read_msg = read_error.str();
*error = read_msg.c_str();
return false;

29
src/api/api_model.cpp
View file

@ -421,34 +421,7 @@ extern "C" {
expr * r = to_func_entry(e)->m_func_entry->get_arg(i);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(nullptr);
}
// ----------------------------
//
// DEPRECATED API
//
// ----------------------------
void Z3_API Z3_del_model(Z3_context c, Z3_model m) {
Z3_model_dec_ref(c, m);
}
unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m) {
return Z3_model_get_num_consts(c, m);
}
Z3_func_decl Z3_API Z3_get_model_constant(Z3_context c, Z3_model m, unsigned i) {
return Z3_model_get_const_decl(c, m, i);
}
unsigned Z3_API Z3_get_model_num_funcs(Z3_context c, Z3_model m) {
return Z3_model_get_num_funcs(c, m);
}
Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i) {
return Z3_model_get_func_decl(c, m, i);
}
}
unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) {
RESET_ERROR_CODE();

14
src/api/api_opt.cpp
View file

@ -17,8 +17,8 @@ Revision History:
--*/
#include<iostream>
#include "util/cancel_eh.h"
#include "util/file_path.h"
#include "util/scoped_timer.h"
#include "util/file_path.h"
#include "parsers/smt2/smt2parser.h"
#include "opt/opt_context.h"
#include "opt/opt_cmds.h"
@ -31,6 +31,7 @@ Revision History:
#include "api/api_model.h"
#include "api/api_ast_vector.h"
extern "C" {
struct Z3_optimize_ref : public api::object {
@ -143,6 +144,12 @@ extern "C" {
mk_c(c)->handle_exception(ex);
}
r = l_undef;
if (ex.msg() == std::string("canceled") && mk_c(c)->m().canceled()) {
to_optimize_ptr(o)->set_reason_unknown(ex.msg());
}
else {
mk_c(c)->handle_exception(ex);
}
}
// to_optimize_ref(d).cleanup();
}
@ -298,6 +305,11 @@ extern "C" {
parse_wcnf(*to_optimize_ptr(opt), s, h);
return;
}
if (ext && std::string("lp") == ext) {
unsigned_vector h;
parse_lp(*to_optimize_ptr(opt), s, h);
return;
}
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
std::stringstream errstrm;

25
src/api/api_parsers.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "api/api_ast_vector.h"
#include "cmd_context/cmd_context.h"
#include "smt/smt_solver.h"
#include "parsers/smt2/smt2parser.h"
@ -41,7 +42,7 @@ extern "C" {
// ---------------
// Support for SMTLIB2
Z3_ast parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
@ -51,6 +52,8 @@ extern "C" {
Z3_TRY;
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx->set_ignore_check(true);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
for (unsigned i = 0; i < num_decls; ++i) {
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
}
@ -69,7 +72,7 @@ extern "C" {
ctx = nullptr;
mk_c(c)->m_parser_error_buffer = errstrm.str();
SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast(mk_c(c)->m().mk_true());
return of_ast_vector(v);
}
}
catch (z3_exception& e) {
@ -77,16 +80,18 @@ extern "C" {
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast(mk_c(c)->m().mk_true());
return of_ast_vector(v);
}
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
unsigned size = static_cast<unsigned>(end - it);
return of_ast(mk_c(c)->mk_and(size, it));
for (; it != end; ++it) {
v->m_ast_vector.push_back(*it);
}
return of_ast_vector(v);
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str,
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
@ -97,12 +102,12 @@ extern "C" {
LOG_Z3_parse_smtlib2_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
std::string s(str);
std::istringstream is(s);
Z3_ast r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name,
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
@ -113,10 +118,10 @@ extern "C" {
LOG_Z3_parse_smtlib2_string(c, file_name, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
std::ifstream is(file_name);
if (!is) {
SET_ERROR_CODE(Z3_PARSER_ERROR);
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
return nullptr;
}
Z3_ast r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}

83
src/api/api_solver.cpp
View file

@ -31,16 +31,21 @@ Revision History:
#include "api/api_stats.h"
#include "api/api_ast_vector.h"
#include "solver/tactic2solver.h"
#include "solver/smt_logics.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "util/file_path.h"
#include "tactic/portfolio/smt_strategic_solver.h"
#include "smt/smt_solver.h"
#include "smt/smt_implied_equalities.h"
#include "solver/smt_logics.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
#include "sat/dimacs.h"
#include "sat/sat_solver.h"
#include "sat/tactic/goal2sat.h"
extern "C" {
static void init_solver_core(Z3_context c, Z3_solver _s) {
@ -128,6 +133,15 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) {
Z3_TRY;
LOG_Z3_solver_import_model_converter(c, src, dst);
model_converter_ref mc = to_solver_ref(src)->get_model_converter();
to_solver_ref(dst)->set_model_converter(mc.get());
Z3_CATCH;
}
void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
ctx->set_ignore_check(true);
@ -146,7 +160,7 @@ extern "C" {
for (; it != end; ++it) {
to_solver_ref(s)->assert_expr(*it);
}
// to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
}
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) {
@ -168,10 +182,10 @@ extern "C" {
}
else if (ext && std::string("dimacs") == ext) {
ast_manager& m = to_solver_ref(s)->get_manager();
sat::solver solver(to_solver_ref(s)->get_params(), m.limit(), nullptr);
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
parse_dimacs(is, solver);
sat2goal s2g;
model_converter_ref mc;
ref<sat2goal::mc> mc;
atom2bool_var a2b(m);
goal g(m);
s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
@ -322,6 +336,7 @@ extern "C" {
to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p));
Z3_CATCH;
}
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) {
Z3_TRY;
@ -338,6 +353,22 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_units(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
expr_ref_vector fmls = to_solver_ref(s)->get_units(mk_c(c)->m());
for (expr* f : fmls) {
v->m_ast_vector.push_back(f);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
for (unsigned i = 0; i < num_assumptions; i++) {
if (!is_expr(to_ast(assumptions[i]))) {
@ -554,4 +585,48 @@ extern "C" {
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) {
Z3_TRY;
LOG_Z3_solver_cube(c, s, vs, cutoff);
ast_manager& m = mk_c(c)->m();
expr_ref_vector result(m), vars(m);
for (ast* a : to_ast_vector_ref(vs)) {
if (!is_expr(a)) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
}
else {
vars.push_back(to_expr(a));
}
}
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
result.append(to_solver_ref(s)->cube(vars, cutoff));
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
return 0;
}
}
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
for (expr* e : result) {
v->m_ast_vector.push_back(e);
}
to_ast_vector_ref(vs).reset();
for (expr* a : vars) {
to_ast_vector_ref(vs).push_back(a);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
};

43
src/api/api_tactic.cpp
View file

@ -25,25 +25,25 @@ Revision History:
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c), m_core(m) {
Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c) {
}
extern "C" {
#define RETURN_TACTIC(_t_) { \
#define RETURN_TACTIC(_t_) { \
Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref, *mk_c(c)); \
_ref_->m_tactic = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_tactic _result_ = of_tactic(_ref_); \
RETURN_Z3(_result_); \
_ref_->m_tactic = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_tactic _result_ = of_tactic(_ref_); \
RETURN_Z3(_result_); \
}
#define RETURN_PROBE(_t_) { \
#define RETURN_PROBE(_t_) { \
Z3_probe_ref * _ref_ = alloc(Z3_probe_ref, *mk_c(c)); \
_ref_->m_probe = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_probe _result_ = of_probe(_ref_); \
RETURN_Z3(_result_); \
_ref_->m_probe = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_probe _result_ = of_probe(_ref_); \
RETURN_Z3(_result_); \
}
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) {
@ -418,7 +418,9 @@ extern "C" {
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
try {
exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_mc, ref->m_pc, ref->m_core);
exec(*to_tactic_ref(t), new_goal, ref->m_subgoals);
ref->m_pc = new_goal->pc();
ref->m_mc = new_goal->mc();
return of_apply_result(ref);
}
catch (z3_exception & ex) {
@ -513,22 +515,5 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m) {
Z3_TRY;
LOG_Z3_apply_result_convert_model(c, r, i, m);
RESET_ERROR_CODE();
if (i > to_apply_result(r)->m_subgoals.size()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(nullptr);
}
model_ref new_m = to_model_ref(m)->copy();
if (to_apply_result(r)->m_mc)
to_apply_result(r)->m_mc->operator()(new_m, i);
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
m_ref->m_model = new_m;
mk_c(c)->save_object(m_ref);
RETURN_Z3(of_model(m_ref));
Z3_CATCH_RETURN(nullptr);
}
};

1
src/api/api_tactic.h
View file

@ -50,7 +50,6 @@ struct Z3_apply_result_ref : public api::object {
goal_ref_buffer m_subgoals;
model_converter_ref m_mc;
proof_converter_ref m_pc;
expr_dependency_ref m_core;
Z3_apply_result_ref(api::context& c, ast_manager & m);
~Z3_apply_result_ref() override {}
};

179
src/api/c++/z3++.h
View file

@ -329,11 +329,11 @@ namespace z3 {
/**
\brief parsing
*/
expr parse_string(char const* s);
expr parse_file(char const* file);
expr_vector parse_string(char const* s);
expr_vector parse_file(char const* file);
expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
/**
\brief Interpolation support
@ -440,6 +440,7 @@ namespace z3 {
void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
friend std::ostream & operator<<(std::ostream & out, params const & p);
};
@ -844,7 +845,6 @@ namespace z3 {
*/
friend expr operator!(expr const & a);
/**
\brief Return an expression representing <tt>a and b</tt>.
@ -901,6 +901,16 @@ namespace z3 {
friend expr ite(expr const & c, expr const & t, expr const & e);
bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
friend expr distinct(expr_vector const& args);
friend expr concat(expr const& a, expr const& b);
friend expr concat(expr_vector const& args);
@ -1915,7 +1925,7 @@ namespace z3 {
bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
friend std::ostream & operator<<(std::ostream & out, stats const & s);
};
inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
@ -2033,6 +2043,97 @@ namespace z3 {
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
expr_vector cube(expr_vector& vars, unsigned cutoff) {
Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
check_error();
return expr_vector(ctx(), r);
}
class cube_iterator {
solver& m_solver;
unsigned& m_cutoff;
expr_vector& m_vars;
expr_vector m_cube;
bool m_end;
bool m_empty;
void inc() {
assert(!m_end && !m_empty);
m_cube = m_solver.cube(m_vars, m_cutoff);
m_cutoff = 0xFFFFFFFF;
if (m_cube.size() == 1 && m_cube[0].is_false()) {
m_cube = z3::expr_vector(m_solver.ctx());
m_end = true;
}
else if (m_cube.empty()) {
m_empty = true;
}
}
public:
cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
m_solver(s),
m_cutoff(cutoff),
m_vars(vars),
m_cube(s.ctx()),
m_end(end),
m_empty(false) {
if (!m_end) {
inc();
}
}
cube_iterator& operator++() {
assert(!m_end);
if (m_empty) {
m_end = true;
}
else {
inc();
}
return *this;
}
cube_iterator operator++(int) { assert(false); return *this; }
expr_vector const * operator->() const { return &(operator*()); }
expr_vector const& operator*() const { return m_cube; }
bool operator==(cube_iterator const& other) {
return other.m_end == m_end;
};
bool operator!=(cube_iterator const& other) {
return other.m_end != m_end;
};
};
class cube_generator {
solver& m_solver;
unsigned m_cutoff;
expr_vector m_default_vars;
expr_vector& m_vars;
public:
cube_generator(solver& s):
m_solver(s),
m_cutoff(0xFFFFFFFF),
m_default_vars(s.ctx()),
m_vars(m_default_vars)
{}
cube_generator(solver& s, expr_vector& vars):
m_solver(s),
m_cutoff(0xFFFFFFFF),
m_default_vars(s.ctx()),
m_vars(vars)
{}
cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
void set_cutoff(unsigned c) { m_cutoff = c; }
};
cube_generator cubes() { return cube_generator(*this); }
cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
};
inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
@ -2056,7 +2157,6 @@ namespace z3 {
return *this;
}
void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
// fails for some compilers:
// void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
@ -2067,6 +2167,17 @@ namespace z3 {
unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
model convert_model(model const & m) const {
check_context(*this, m);
Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
check_error();
return model(ctx(), new_m);
}
model get_model() const {
Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
check_error();
return model(ctx(), new_m);
}
expr as_expr() const {
unsigned n = size();
if (n == 0)
@ -2080,6 +2191,7 @@ namespace z3 {
return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
}
}
std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); }
friend std::ostream & operator<<(std::ostream & out, goal const & g);
};
inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
@ -2104,25 +2216,6 @@ namespace z3 {
}
unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
model convert_model(model const & m, unsigned i = 0) const {
check_context(*this, m);
Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
check_error();
return model(ctx(), new_m);
}
expr as_expr() const {
unsigned n = size();
if (n == 0)
return ctx().bool_val(true);
else if (n == 1)
return operator[](0).as_expr();
else {
array<Z3_ast> args(n);
for (unsigned i = 0; i < n; i++)
args[i] = operator[](i).as_expr();
return expr(ctx(), Z3_mk_or(ctx(), n, args.ptr()));
}
}
friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
};
inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
@ -2880,18 +2973,19 @@ namespace z3 {
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
}
inline expr context::parse_string(char const* s) {
Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
check_parser_error();
return expr(*this, r);
inline expr_vector context::parse_string(char const* s) {
Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
check_error();
return expr_vector(*this, r);
}
inline expr context::parse_file(char const* s) {
Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
check_parser_error();
return expr(*this, r);
inline expr_vector context::parse_file(char const* s) {
Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
check_error();
return expr_vector(*this, r);
}
inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
array<Z3_symbol> sort_names(sorts.size());
array<Z3_symbol> decl_names(decls.size());
array<Z3_sort> sorts1(sorts);
@ -2902,12 +2996,13 @@ namespace z3 {
for (unsigned i = 0; i < decls.size(); ++i) {
decl_names[i] = decls[i].name();
}
Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
check_parser_error();
return expr(*this, r);
Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
check_error();
return expr_vector(*this, r);
}
inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
array<Z3_symbol> sort_names(sorts.size());
array<Z3_symbol> decl_names(decls.size());
array<Z3_sort> sorts1(sorts);
@ -2918,9 +3013,9 @@ namespace z3 {
for (unsigned i = 0; i < decls.size(); ++i) {
decl_names[i] = decls[i].name();
}
Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
check_parser_error();
return expr(*this, r);
Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
check_error();
return expr_vector(*this, r);
}

13
src/api/dotnet/ApplyResult.cs
View file

@ -55,19 +55,6 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Convert a model for the subgoal <paramref name="i"/> into a model for the original
/// goal <c>g</c>, that the ApplyResult was obtained from.
/// </summary>
/// <returns>A model for <c>g</c></returns>
public Model ConvertModel(uint i, Model m)
{
Contract.Requires(m != null);
Contract.Ensures(Contract.Result<Model>() != null);
return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject));
}
/// <summary>
/// A string representation of the ApplyResult.
/// </summary>

10
src/api/dotnet/Context.cs
View file

@ -3325,7 +3325,7 @@ namespace Microsoft.Z3
/// Parse the given string using the SMT-LIB2 parser.
/// </summary>
/// <returns>A conjunction of assertions in the scope (up to push/pop) at the end of the string.</returns>
public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
@ -3335,16 +3335,17 @@ namespace Microsoft.Z3
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
return assertions.ToBoolExprArray();
}
/// <summary>
/// Parse the given file using the SMT-LIB2 parser.
/// </summary>
/// <seealso cref="ParseSMTLIB2String"/>
public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
@ -3354,9 +3355,10 @@ namespace Microsoft.Z3
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
return assertions.ToBoolExprArray();
}
#endregion

24
src/api/dotnet/Goal.cs
View file

@ -174,6 +174,21 @@ namespace Microsoft.Z3
get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
}
/// <summary>
/// Convert a model for the goal into a model of the
/// original goal from which this goal was derived.
/// </summary>
/// <returns>A model for <c>g</c></returns>
public Model ConvertModel(Model m)
{
Contract.Ensures(Contract.Result<Model>() != null);
if (m != null)
return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject));
else
return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, IntPtr.Zero));
}
/// <summary>
/// Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
/// </summary>
@ -208,6 +223,15 @@ namespace Microsoft.Z3
return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
}
/// <summary>
/// Goal to DIMACS formatted string conversion.
/// </summary>
/// <returns>A string representation of the Goal.</returns>
public string ToDimacs()
{
return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject);
}
/// <summary>
/// Goal to BoolExpr conversion.
/// </summary>

17
src/api/dotnet/InterpolationContext.cs
View file

@ -133,19 +133,16 @@ namespace Microsoft.Z3
/// well documented.</remarks>
public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
{
uint num = 0, num_theory = 0;
IntPtr[] n_cnsts;
IntPtr[] n_theory;
uint num = 0;
IntPtr n_err_str;
int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
ASTVector _cnsts = new ASTVector(this);
ASTVector _theory = new ASTVector(this);
int r = Native.Z3_read_interpolation_problem(nCtx, _cnsts.NativeObject, ref num, out parents, filename, out n_err_str, _theory.NativeObject);
error = Marshal.PtrToStringAnsi(n_err_str);
cnsts = new Expr[num];
cnsts = _cnsts.ToExprArray();
parents = new uint[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
cnsts[i] = Expr.Create(this, n_cnsts[i]);
for (int i = 0; i < num_theory; i++)
theory[i] = Expr.Create(this, n_theory[i]);
theory = _theory.ToExprArray();
return r;
}

4
src/api/dotnet/Params.cs
View file

@ -91,7 +91,7 @@ namespace Microsoft.Z3
public Params Add(string name, bool value)
{
Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
return this;
return this;
}
/// <summary>
@ -100,7 +100,7 @@ namespace Microsoft.Z3
public Params Add(string name, uint value)
{
Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
return this;
return this;
}
/// <summary>

68
src/api/dotnet/Solver.cs
View file

@ -57,7 +57,7 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
@ -266,6 +266,20 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Currently inferred units.
/// </summary>
public BoolExpr[] Units
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
return assertions.ToBoolExprArray();
}
}
/// <summary>
/// Checks whether the assertions in the solver are consistent or not.
/// </summary>
@ -331,10 +345,10 @@ namespace Microsoft.Z3
}
/// <summary>
/// The model of the last <c>Check</c>.
/// The model of the last <c>Check(params Expr[] assumptions)</c>.
/// </summary>
/// <remarks>
/// The result is <c>null</c> if <c>Check</c> was not invoked before,
/// The result is <c>null</c> if <c>Check(params Expr[] assumptions)</c> was not invoked before,
/// if its results was not <c>SATISFIABLE</c>, or if model production is not enabled.
/// </remarks>
public Model Model
@ -350,10 +364,10 @@ namespace Microsoft.Z3
}
/// <summary>
/// The proof of the last <c>Check</c>.
/// The proof of the last <c>Check(params Expr[] assumptions)</c>.
/// </summary>
/// <remarks>
/// The result is <c>null</c> if <c>Check</c> was not invoked before,
/// The result is <c>null</c> if <c>Check(params Expr[] assumptions)</c> was not invoked before,
/// if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled.
/// </remarks>
public Expr Proof
@ -400,6 +414,42 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Backtrack level that can be adjusted by conquer process
/// </summary>
public uint BacktrackLevel { get; set; }
/// <summary>
/// Variables available and returned by the cuber.
/// </summary>
public BoolExpr[] CubeVariables { get; set; }
/// <summary>
/// Return a set of cubes.
/// </summary>
public IEnumerable<BoolExpr[]> Cube()
{
ASTVector cv = new ASTVector(Context);
if (CubeVariables != null)
foreach (var b in CubeVariables) cv.Push(b);
while (true) {
var lvl = BacktrackLevel;
BacktrackLevel = uint.MaxValue;
ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
var v = r.ToBoolExprArray();
CubeVariables = cv.ToBoolExprArray();
if (v.Length == 1 && v[0].IsFalse) {
break;
}
yield return v;
if (v.Length == 0) {
break;
}
}
}
/// <summary>
/// Create a clone of the current solver with respect to <c>ctx</c>.
/// </summary>
@ -410,6 +460,13 @@ namespace Microsoft.Z3
return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/// <summary>
/// Import model converter from other solver.
/// </summary>
public void ImportModelConverter(Solver src)
{
Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
}
/// <summary>
/// Solver statistics.
@ -437,6 +494,7 @@ namespace Microsoft.Z3
: base(ctx, obj)
{
Contract.Requires(ctx != null);
this.BacktrackLevel = uint.MaxValue;
}
internal class DecRefQueue : IDecRefQueue

13
src/api/java/ApplyResult.java
View file

@ -46,19 +46,6 @@ public class ApplyResult extends Z3Object {
return res;
}
/**
* Convert a model for the subgoal {@code i} into a model for the
* original goal {@code g}, that the ApplyResult was obtained from.
*
* @return A model for {@code g}
* @throws Z3Exception
**/
public Model convertModel(int i, Model m)
{
return new Model(getContext(),
Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
}
/**
* A string representation of the ApplyResult.
**/

13
src/api/java/Context.java
View file

@ -2549,8 +2549,9 @@ public class Context implements AutoCloseable {
* set of assertions returned are the ones in the
* last scope level.
**/
public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
{
int csn = Symbol.arrayLength(sortNames);
int cs = Sort.arrayLength(sorts);
@ -2559,17 +2560,18 @@ public class Context implements AutoCloseable {
if (csn != cs || cdn != cd) {
throw new Z3Exception("Argument size mismatch");
}
return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts), AST.arrayLength(decls),
Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
return v.ToBoolExprArray();
}
/**
* Parse the given file using the SMT-LIB2 parser.
* @see #parseSMTLIB2String
**/
public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
{
@ -2579,11 +2581,12 @@ public class Context implements AutoCloseable {
int cd = AST.arrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
fileName, AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
AST.arrayLength(decls), Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
return v.ToBoolExprArray();
}
/**

15
src/api/java/Goal.java
View file

@ -240,6 +240,21 @@ public class Goal extends Z3Object {
(unsatCores), (proofs)));
}
/**
* Convert a model for the goal into a model of the
* original goal from which this goal was derived.
*
* @return A model for {@code g}
* @throws Z3Exception
**/
public Model convertModel(Model m)
{
return new Model(getContext(),
Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
}
@Override
void incRef() {
Native.goalIncRef(getContext().nCtx(), getNativeObject());

42
src/api/java/InterpolationContext.java
View file

@ -176,31 +176,25 @@ public class InterpolationContext extends Context
/// Remarks: For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.
public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
public ReadInterpolationProblemResult ReadInterpolationProblem(String filename)
{
ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
Native.IntPtr n_num = new Native.IntPtr();
Native.IntPtr n_num_theory = new Native.IntPtr();
Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
Native.StringPtr n_err_str = new Native.StringPtr();
res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
int num = n_num.value;
int num_theory = n_num_theory.value;
res.error = n_err_str.value;
res.cnsts = new Expr[num];
res.parents = new int[num];
theory = new Expr[num_theory];
for (int i = 0; i < num; i++)
{
res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
res.parents[i] = n_parents.value[i];
}
for (int i = 0; i < num_theory; i++)
res.theory[i] = Expr.create(this, n_theory.value[i]);
return res;
ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
ASTVector _cnsts = new ASTVector(this);
ASTVector _theory = new ASTVector(this);
Native.StringPtr n_err_str = new Native.StringPtr();
Native.IntPtr n_num = new Native.IntPtr();
res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts.getNativeObject(), n_num,
n_parents, filename, n_err_str, _theory.getNativeObject());
res.error = n_err_str.value;
res.theory = _theory.ToExprArray();
res.cnsts = _cnsts.ToExprArray();
int num = n_num.value;
res.parents = new int[num];
for (int i = 0; i < num; i++) {
res.parents[i] = n_parents.value[i];
}
return res;
}
///

33
src/api/java/Solver.java
View file

@ -121,22 +121,6 @@ public class Solver extends Z3Object {
}
}
/**
* Load solver assertions from a file.
*/
public void fromFile(String file)
{
Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
}
/**
* Load solver assertions from a string.
*/
public void fromString(String str)
{
Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
}
/**
* Assert multiple constraints into the solver, and track them (in the
@ -188,6 +172,23 @@ public class Solver extends Z3Object {
constraint.getNativeObject(), p.getNativeObject());
}
/// <summary>
/// Load solver assertions from a file.
/// </summary>
public void fromFile(String file)
{
Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
}
/// <summary>
/// Load solver assertions from a string.
/// </summary>
public void fromString(String str)
{
Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
}
/**
* The number of assertions in the solver.
*

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

@ -1415,6 +1415,17 @@ def is_or(a):
"""
return is_app_of(a, Z3_OP_OR)
def is_implies(a):
"""Return `True` if `a` is a Z3 implication expression.
>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False
"""
return is_app_of(a, Z3_OP_IMPLIES)
def is_not(a):
"""Return `True` if `a` is a Z3 not expression.
@ -5032,6 +5043,35 @@ class Goal(Z3PPObject):
"""
self.assert_exprs(*args)
def convert_model(self, model):
"""Retrieve model from a satisfiable goal
>>> a, b = Ints('a b')
>>> g = Goal()
>>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
>>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
>>> r = t(g)
>>> r[0]
[Or(b == 0, b == 1), Not(0 <= b)]
>>> r[1]
[Or(b == 0, b == 1), Not(1 <= b)]
>>> # Remark: the subgoal r[0] is unsatisfiable
>>> # Creating a solver for solving the second subgoal
>>> s = Solver()
>>> s.add(r[1])
>>> s.check()
sat
>>> s.model()
[b = 0]
>>> # Model s.model() does not assign a value to `a`
>>> # It is a model for subgoal `r[1]`, but not for goal `g`
>>> # The method convert_model creates a model for `g` from a model for `r[1]`.
>>> r[1].convert_model(s.model())
[b = 0, a = 1]
"""
if __debug__:
_z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx)
def __repr__(self):
return obj_to_string(self)
@ -5039,6 +5079,10 @@ class Goal(Z3PPObject):
"""Return a textual representation of the s-expression representing the goal."""
return Z3_goal_to_string(self.ctx.ref(), self.goal)
def dimacs(self):
"""Return a textual representation of the goal in DIMACS format."""
return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal)
def translate(self, target):
"""Copy goal `self` to context `target`.
@ -6095,6 +6139,7 @@ class Solver(Z3PPObject):
def __init__(self, solver=None, ctx=None):
assert solver is None or ctx is not None
self.ctx = _get_ctx(ctx)
self.backtrack_level = 4000000000
self.solver = None
if solver is None:
self.solver = Z3_mk_solver(self.ctx.ref())
@ -6401,10 +6446,37 @@ class Solver(Z3PPObject):
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def cube(self, vars = None):
"""Get set of cubes"""
self.cube_vs = AstVector(None, self.ctx)
if vars is not None:
for v in vars:
self.cube_vs.push(v)
while True:
lvl = self.backtrack_level
self.backtrack_level = 4000000000
r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
if (len(r) == 1 and is_false(r[0])):
return
yield r
if (len(r) == 0):
return
def cube_vars(self):
return self.cube_vs
def proof(self):
"""Return a proof for the last `check()`. Proof construction must be enabled."""
return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
def from_file(self, filename):
"""Parse assertions from a file"""
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
def from_string(self, s):
"""Parse assertions from a string"""
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
def assertions(self):
"""Return an AST vector containing all added constraints.
@ -6419,6 +6491,11 @@ class Solver(Z3PPObject):
"""
return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
def units(self):
"""Return an AST vector containing all currently inferred units.
"""
return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
def statistics(self):
"""Return statistics for the last `check()`.
@ -7187,36 +7264,6 @@ class ApplyResult(Z3PPObject):
"""Return a textual representation of the s-expression representing the set of subgoals in `self`."""
return Z3_apply_result_to_string(self.ctx.ref(), self.result)
def convert_model(self, model, idx=0):
"""Convert a model for a subgoal into a model for the original goal.
>>> a, b = Ints('a b')
>>> g = Goal()
>>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
>>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
>>> r = t(g)
>>> r[0]
[Or(b == 0, b == 1), Not(0 <= b)]
>>> r[1]
[Or(b == 0, b == 1), Not(1 <= b)]
>>> # Remark: the subgoal r[0] is unsatisfiable
>>> # Creating a solver for solving the second subgoal
>>> s = Solver()
>>> s.add(r[1])
>>> s.check()
sat
>>> s.model()
[b = 0]
>>> # Model s.model() does not assign a value to `a`
>>> # It is a model for subgoal `r[1]`, but not for goal `g`
>>> # The method convert_model creates a model for `g` from a model for `r[1]`.
>>> r.convert_model(s.model(), 1)
[b = 0, a = 1]
"""
if __debug__:
_z3_assert(idx < len(self), "index out of bounds")
_z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
return ModelRef(Z3_apply_result_convert_model(self.ctx.ref(), self.result, idx, model.model), self.ctx)
def as_expr(self):
"""Return a Z3 expression consisting of all subgoals.
@ -8193,19 +8240,19 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
the symbol table used for the SMT 2.0 parser.
>>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
And(x > 0, x < 10)
[x > 0, x < 10]
>>> x, y = Ints('x y')
>>> f = Function('f', IntSort(), IntSort())
>>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
x + f(y) > 0
[x + f(y) > 0]
>>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
a > 0
[a > 0]
"""
ctx = _get_ctx(ctx)
ssz, snames, ssorts = _dict2sarray(sorts, ctx)
dsz, dnames, ddecls = _dict2darray(decls, ctx)
try:
return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
except Z3Exception as e:
_handle_parse_error(e, ctx)
@ -8217,8 +8264,8 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
ctx = _get_ctx(ctx)
ssz, snames, ssorts = _dict2sarray(sorts, ctx)
dsz, dnames, ddecls = _dict2darray(decls, ctx)
try:
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
try:
return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
except Z3Exception as e:
_handle_parse_error(e, ctx)

82
src/api/z3_api.h
View file

@ -5175,9 +5175,9 @@ extern "C" {
It returns a formula comprising of the conjunction of assertions in the scope
(up to push/pop) at the end of the string.
def_API('Z3_parse_smtlib2_string', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
def_API('Z3_parse_smtlib2_string', AST_VECTOR, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
*/
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c,
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c,
Z3_string str,
unsigned num_sorts,
Z3_symbol const sort_names[],
@ -5189,9 +5189,9 @@ extern "C" {
/**
\brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file.
def_API('Z3_parse_smtlib2_file', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
def_API('Z3_parse_smtlib2_file', AST_VECTOR, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))
*/
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c,
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c,
Z3_string file_name,
unsigned num_sorts,
Z3_symbol const sort_names[],
@ -5450,6 +5450,15 @@ extern "C" {
*/
Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
/**
\brief Convert a model of the formulas of a goal to a model of an original goal.
The model may be null, in which case the returned model is valid if the goal was
established satisfiable.
def_API('Z3_goal_convert_model', MODEL, (_in(CONTEXT), _in(GOAL), _in(MODEL)))
*/
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);
/**
\brief Convert a goal into a string.
@ -5457,6 +5466,13 @@ extern "C" {
*/
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
/**
\brief Convert a goal into a DIMACS formatted string.
def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL)))
*/
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g);
/*@}*/
/** @name Tactics and Probes */
@ -5809,14 +5825,6 @@ extern "C" {
*/
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
/**
\brief Convert a model for the subgoal \c Z3_apply_result_get_subgoal(c, r, i) into a model for the original goal \c g.
Where \c g is the goal used to create \c r using \c Z3_tactic_apply(c, t, g).
def_API('Z3_apply_result_convert_model', MODEL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT), _in(MODEL)))
*/
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m);
/*@}*/
/** @name Solvers*/
@ -5916,6 +5924,13 @@ extern "C" {
*/
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
/**
\brief Ad-hoc method for importing model convertion from solver.
def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER)))
*/
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);
/**
\brief Return a string describing all solver available parameters.
@ -6016,13 +6031,6 @@ extern "C" {
*/
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
/**
\brief Return the set of asserted formulas on the solver.
def_API('Z3_solver_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
/**
\brief load solver assertions from a file.
@ -6037,6 +6045,20 @@ extern "C" {
*/
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
/**
\brief Return the set of asserted formulas on the solver.
def_API('Z3_solver_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
/**
\brief Return the set of units modulo model conversion.
def_API('Z3_solver_get_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
/**
\brief Check whether the assertions in a given solver are consistent or not.
@ -6104,6 +6126,28 @@ extern "C" {
Z3_ast_vector assumptions,
Z3_ast_vector variables,
Z3_ast_vector consequences);
/**
\brief extract a next cube for a solver. The last cube is the constant \c true or \c false.
The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled
using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.
The third argument is a vector of variables that may be used for cubing.
The contents of the vector is only used in the first call. The initial list of variables
is used in subsequent calls until it returns the unsatisfiable cube.
The vector is modified to contain a set of Autarky variables that occor in clauses that
are affected by the (last literal in the) cube. These variables could be used by a different
cuber (on a different solver object) for further recursive cubing.
The last argument is a backtracking level. It instructs the cube process to backtrack below
the indicated level for the next cube.
def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT)))
*/
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
/**
\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions

11
src/api/z3_interp.h
View file

@ -207,18 +207,17 @@ extern "C" {
where each value is represented using the common symbols between
the formulas in the subtree and the remainder of the formulas.
def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST)))
def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _in(AST_VECTOR), _out(UINT), _out_managed_array(2, UINT), _in(STRING), _out(STRING), _in(AST_VECTOR)))
*/
int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
unsigned *num,
Z3_ast *cnsts[],
unsigned *parents[],
Z3_ast_vector cnsts,
unsigned* num,
unsigned* parents[],
Z3_string filename,
Z3_string_ptr error,
unsigned *num_theory,
Z3_ast *theory[]);
Z3_ast_vector theory);

9
src/ast/ast.cpp
View file

@ -1348,6 +1348,10 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
copy_families_plugins(src);
}
void ast_manager::update_fresh_id(ast_manager const& m) {
m_fresh_id = std::max(m_fresh_id, m.m_fresh_id);
}
void ast_manager::init() {
m_int_real_coercions = true;
m_debug_ref_count = false;
@ -1506,7 +1510,7 @@ void ast_manager::compress_ids() {
else
n->m_id = m_expr_id_gen.mk();
asts.push_back(n);
}
}
m_ast_table.finalize();
for (ast* a : asts)
m_ast_table.insert(a);
@ -2221,9 +2225,10 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const
}
else {
string_buffer<64> buffer;
buffer << prefix;
if (prefix == symbol::null)
buffer << "sk";
else
buffer << prefix;
buffer << "!";
if (suffix != symbol::null)
buffer << suffix << "!";

5
src/ast/ast.h
View file

@ -628,6 +628,9 @@ public:
sort * const * get_domain() const { return m_domain; }
sort * get_range() const { return m_range; }
unsigned get_size() const { return get_obj_size(m_arity); }
sort * const * begin() const { return get_domain(); }
sort * const * end() const { return get_domain() + get_arity(); }
};
// -----------------------------------
@ -1451,6 +1454,8 @@ public:
void show_id_gen();
void update_fresh_id(ast_manager const& other);
protected:
reslimit m_limit;
small_object_allocator m_alloc;

14
src/ast/ast_pp_util.cpp
View file

@ -36,7 +36,6 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
}
void ast_pp_util::display_decls(std::ostream& out) {
smt2_pp_environment_dbg env(m);
ast_smt_pp pp(m);
coll.order_deps();
unsigned n = coll.get_num_sorts();
@ -47,10 +46,10 @@ void ast_pp_util::display_decls(std::ostream& out) {
for (unsigned i = 0; i < n; ++i) {
func_decl* f = coll.get_func_decls()[i];
if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
ast_smt2_pp(out, f, env);
out << "\n";
ast_smt2_pp(out, f, m_env) << "\n";
}
}
SASSERT(coll.get_num_preds() == 0);
}
void ast_pp_util::remove_decl(func_decl* f) {
@ -60,18 +59,17 @@ void ast_pp_util::remove_decl(func_decl* f) {
void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
if (neat) {
smt2_pp_environment_dbg env(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
for (expr* f : fmls) {
out << "(assert ";
ast_smt2_pp(out, fmls[i], env);
ast_smt2_pp(out, f, m_env);
out << ")\n";
}
}
else {
ast_smt_pp ll_smt2_pp(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
for (expr* f : fmls) {
out << "(assert ";
ll_smt2_pp.display_expr_smt2(out, fmls[i]);
ll_smt2_pp.display_expr_smt2(out, f);
out << ")\n";
}
}

6
src/ast/ast_pp_util.h
View file

@ -20,16 +20,18 @@ Revision History:
#define AST_PP_UTIL_H_
#include "ast/decl_collector.h"
#include "ast/ast_smt2_pp.h"
#include "util/obj_hashtable.h"
class ast_pp_util {
ast_manager& m;
obj_hashtable<func_decl> m_removed;
smt2_pp_environment_dbg m_env;
public:
decl_collector coll;
ast_pp_util(ast_manager& m): m(m), coll(m, false) {}
ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m, false) {}
void collect(expr* e);
@ -42,6 +44,8 @@ class ast_pp_util {
void display_decls(std::ostream& out);
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);
smt2_pp_environment& env() { return m_env; }
};
#endif /* AST_PP_UTIL_H_ */

2
src/ast/ast_printer.cpp
View file

@ -34,7 +34,7 @@ public:
out << f->get_name();
}
void pp(sort * s, format_ns::format_ref & r) const override { mk_smt2_format(s, env(), params_ref(), r); }
void pp(func_decl * f, format_ns::format_ref & r) const override { mk_smt2_format(f, env(), params_ref(), r); }
void pp(func_decl * f, format_ns::format_ref & r) const override { mk_smt2_format(f, env(), params_ref(), r, "declare-fun"); }
void pp(expr * n, format_ns::format_ref & r) const override {
sbuffer<symbol> buf;
mk_smt2_format(n, env(), params_ref(), 0, nullptr, r, buf);

111
src/ast/ast_smt2_pp.cpp
View file

@ -31,7 +31,7 @@ using namespace format_ns;
#define MAX_INDENT 16
#define SMALL_INDENT 2
format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) const {
format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bool is_skolem) const {
ast_manager & m = get_manager();
if (is_smt2_quoted_symbol(s)) {
std::string str = mk_smt2_quoted_symbol(s);
@ -69,7 +69,7 @@ format * smt2_pp_environment::pp_fdecl_name(func_decl * f, unsigned & len) const
}
else {
symbol s = f->get_name();
return pp_fdecl_name(s, len);
return pp_fdecl_name(s, len, f->is_skolem());
}
}
@ -116,8 +116,10 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) {
(f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
if (f->get_parameter(i).is_int())
fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int()));
else if (f->get_parameter(i).is_rational())
fs.push_back(mk_string(get_manager(), f->get_parameter(i).get_rational().to_string().c_str()));
else if (f->get_parameter(i).is_rational()) {
std::string str = f->get_parameter(i).get_rational().to_string();
fs.push_back(mk_string(get_manager(), str.c_str()));
}
else
fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast())));
}
@ -614,9 +616,9 @@ class smt2_printer {
return f;
ptr_buffer<format> buf;
buf.push_back(f);
for (unsigned i = 0; i < names.size(); i++) {
buf.push_back(pp_simple_attribute(is_pos ? ":lblpos " : ":lblneg ", names[i]));
}
for (symbol const& n : names)
buf.push_back(pp_simple_attribute(is_pos ? ":lblpos " : ":lblneg ", n));
return mk_seq1(m(), buf.begin(), buf.end(), f2f(), "!");
}
@ -891,8 +893,21 @@ class smt2_printer {
}
}
void register_var_names(unsigned n) {
unsigned idx = 1;
for (unsigned i = 0; i < n; i++) {
symbol name = next_name("x", idx);
SASSERT(!m_var_names_set.contains(name));
m_var_names.push_back(name);
m_var_names_set.insert(name);
}
}
void unregister_var_names(quantifier * q) {
unsigned num_decls = q->get_num_decls();
unregister_var_names(q->get_num_decls());
}
void unregister_var_names(unsigned num_decls) {
for (unsigned i = 0; i < num_decls; i++) {
symbol s = m_var_names.back();
m_var_names.pop_back();
@ -900,13 +915,12 @@ class smt2_printer {
}
}
format * pp_var_decls(quantifier * q) {
format * pp_var_args(unsigned num_decls, sort* const* srts) {
ptr_buffer<format> buf;
unsigned num_decls = q->get_num_decls();
SASSERT(num_decls <= m_var_names.size());
symbol * it = m_var_names.end() - num_decls;
for (unsigned i = 0; i < num_decls; i++, it++) {
format * fs[1] = { m_env.pp_sort(q->get_decl_sort(i)) };
format * fs[1] = { m_env.pp_sort(srts[i]) };
std::string var_name;
if (is_smt2_quoted_symbol (*it)) {
var_name = mk_smt2_quoted_symbol (*it);
@ -919,6 +933,10 @@ class smt2_printer {
return mk_seq5(m(), buf.begin(), buf.end(), f2f());
}
format * pp_var_decls(quantifier * q) {
return pp_var_args(q->get_num_decls(), q->get_decl_sorts());
}
void process_quantifier(quantifier * q, frame & fr) {
if (fr.m_idx == 0) {
begin_scope();
@ -1009,10 +1027,8 @@ class smt2_printer {
void reset_expr2alias_stack() {
SASSERT(!m_expr2alias_stack.empty());
ptr_vector<expr2alias>::iterator it = m_expr2alias_stack.begin();
ptr_vector<expr2alias>::iterator end = m_expr2alias_stack.end();
for (; it != end; ++it)
(*it)->reset();
for (expr2alias * e : m_expr2alias_stack)
e->reset();
m_expr2alias = m_expr2alias_stack[0];
}
@ -1113,7 +1129,7 @@ public:
r = m_env.pp_sort(s);
}
void operator()(func_decl * f, format_ref & r) {
void operator()(func_decl * f, format_ref & r, char const* cmd) {
unsigned arity = f->get_arity();
unsigned len;
format * fname = m_env.pp_fdecl_name(f, len);
@ -1125,9 +1141,26 @@ public:
}
args[1] = mk_seq5<format**, f2f>(m(), buf.begin(), buf.end(), f2f());
args[2] = m_env.pp_sort(f->get_range());
r = mk_seq1<format**, f2f>(m(), args, args+3, f2f(), "declare-fun");
r = mk_seq1<format**, f2f>(m(), args, args+3, f2f(), cmd);
}
void operator()(func_decl * f, expr * e, format_ref & r, char const* cmd) {
unsigned len;
format * fname = m_env.pp_fdecl_name(f, len);
register_var_names(f->get_arity());
format * args[4];
args[0] = fname;
args[1] = pp_var_args(f->get_arity(), f->get_domain());
args[2] = m_env.pp_sort(f->get_range());
process(e, r);
args[3] = r;
r = mk_seq1<format**, f2f>(m(), args, args+4, f2f(), cmd);
unregister_var_names(f->get_arity());
}
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
@ -1142,9 +1175,14 @@ void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, f
pr(s, r);
}
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ref & r, char const* cmd) {
smt2_printer pr(env, p);
pr(f, r);
pr(f, r, cmd);
}
void mk_smt2_format(func_decl * f, expr * e, smt2_pp_environment & env, params_ref const & p, format_ref & r, char const* cmd) {
smt2_printer pr(env, p);
pr(f, e, r, cmd);
}
void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p,
@ -1185,17 +1223,29 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
mk_smt2_format(f, env, p, r);
mk_smt2_format(f, env, p, r, cmd);
if (indent > 0)
r = mk_indent(m, indent, r.get());
pp(out, r.get(), m, p);
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
mk_smt2_format(f, e, env, p, r, cmd);
if (indent > 0)
r = mk_indent(m, indent, r.get());
pp(out, r.get(), m, p);
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p, unsigned indent,
unsigned num_vars, char const * var_prefix) {
ast_manager & m = env.get_manager();
@ -1208,6 +1258,15 @@ std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, sm
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p) {
unsigned len;
ast_manager & m = env.get_manager();
format_ref r(fm(m));
r = env.pp_fdecl_name(s, len, is_skolem);
pp(out, r.get(), m, p);
return out;
}
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
m_ast(t),
m_manager(m),
@ -1226,6 +1285,8 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num
m_var_prefix(var_prefix) {
}
std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
smt2_pp_environment_dbg env(p.m_manager);
if (p.m_ast == nullptr) {
@ -1273,14 +1334,14 @@ std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) {
}
std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e) {
for (unsigned i = 0; i < e.size(); ++i)
out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
for (func_decl* f : e)
out << mk_ismt2_pp(f, e.get_manager()) << "\n";
return out;
}
std::ostream& operator<<(std::ostream& out, sort_ref_vector const& e) {
for (unsigned i = 0; i < e.size(); ++i)
out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
for (sort* s : e)
out << mk_ismt2_pp(s, e.get_manager()) << "\n";
return out;
}

10
src/ast/ast_smt2_pp.h
View file

@ -31,10 +31,12 @@ Revision History:
#include "ast/dl_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/ast_smt_pp.h"
#include "util/smt2_util.h"
class smt2_pp_environment {
protected:
mutable smt_renaming m_renaming;
format_ns::format * mk_neg(format_ns::format * f) const;
format_ns::format * mk_float(rational const & val) const;
bool is_indexed_fdecl(func_decl * f) const;
@ -61,7 +63,7 @@ public:
virtual format_ns::format * pp_string_literal(app * t);
virtual format_ns::format * pp_sort(sort * s);
virtual format_ns::format * pp_fdecl_ref(func_decl * f);
format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;
format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len, bool is_skolem) const;
format_ns::format * pp_fdecl_name(func_decl * f, unsigned & len) const;
};
@ -95,12 +97,14 @@ void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
unsigned num_vars, char const * var_prefix,
format_ns::format_ref & r, sbuffer<symbol> & var_names);
void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r, char const* cmd);
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0,
unsigned num_vars = 0, char const * var_prefix = nullptr);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun");
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
/**
\brief Internal wrapper (for debugging purposes only)

64
src/ast/ast_smt_pp.cpp
View file

@ -45,14 +45,6 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
std::ostringstream buffer;
char const * data = s.is_numerical() ? "" : s.bare_str();
if (data[0] && !data[1]) {
switch (data[0]) {
case '/': data = "op_div"; break;
case '%': data = "op_mod"; break;
default: break;
}
}
if (k == 0 && *data) {
if (s.is_numerical()) {
return s;
@ -70,14 +62,17 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
return symbol(buffer.str().c_str());
}
if (is_smt2_quoted_symbol(s)) {
if (!s.bare_str()) {
buffer << "null";
}
else if (is_smt2_quoted_symbol(s)) {
buffer << mk_smt2_quoted_symbol(s);
}
else {
buffer << s;
}
if (k > 0) {
buffer << k;
buffer << "!" << k;
}
return symbol(buffer.str().c_str());
@ -124,15 +119,30 @@ bool smt_renaming::all_is_legal(char const* s) {
smt_renaming::smt_renaming() {
for (unsigned i = 0; i < ARRAYSIZE(m_predef_names); ++i) {
symbol s(m_predef_names[i]);
m_translate.insert(s, s);
m_translate.insert(s, sym_b(s, false));
m_rev_translate.insert(s, s);
}
}
symbol smt_renaming::get_symbol(symbol s0) {
// Ensure that symbols that are used both with skolems and non-skolems are named apart.
symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) {
sym_b sb;
symbol s;
if (m_translate.find(s0, s)) {
if (m_translate.find(s0, sb)) {
if (is_skolem == sb.is_skolem)
return sb.name;
if (sb.name_aux != symbol::null) {
return sb.name_aux;
}
int k = 0;
symbol s1;
do {
s = fix_symbol(s0, k++);
}
while (s == s0 || (m_rev_translate.find(s, s1) && s1 != s0));
m_rev_translate.insert(s, s0);
sb.name_aux = s;
m_translate.insert(s, sb);
return s;
}
@ -141,7 +151,7 @@ symbol smt_renaming::get_symbol(symbol s0) {
s = fix_symbol(s0, k++);
}
while (m_rev_translate.contains(s));
m_translate.insert(s0, s);
m_translate.insert(s0, sym_b(s, is_skolem));
m_rev_translate.insert(s, s0);
return s;
}
@ -202,7 +212,7 @@ class smt_printer {
}
void pp_decl(func_decl* d) {
symbol sym = m_renaming.get_symbol(d->get_name());
symbol sym = m_renaming.get_symbol(d->get_name(), d->is_skolem());
if (d->get_family_id() == m_dt_fid) {
datatype_util util(m_manager);
if (util.is_recognizer(d)) {
@ -313,7 +323,7 @@ class smt_printer {
if (num_sorts > 0) {
m_out << "(";
}
m_out << m_renaming.get_symbol(s->get_name());
m_out << m_renaming.get_symbol(s->get_name(), false);
if (num_sorts > 0) {
for (unsigned i = 0; i < num_sorts; ++i) {
m_out << " ";
@ -324,7 +334,7 @@ class smt_printer {
return;
}
else {
sym = m_renaming.get_symbol(s->get_name());
sym = m_renaming.get_symbol(s->get_name(), false);
}
visit_params(true, sym, s->get_num_parameters(), s->get_parameters());
}
@ -395,17 +405,17 @@ class smt_printer {
else if (m_manager.is_label(n, pos, names) && names.size() >= 1) {
m_out << "(! ";
pp_marked_expr(n->get_arg(0));
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0]) << ")";
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
}
else if (m_manager.is_label_lit(n, names) && names.size() >= 1) {
m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0]) << ")";
m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")";
}
else if (num_args == 0) {
if (decl->private_parameters()) {
m_out << m_renaming.get_symbol(decl->get_name());
m_out << m_renaming.get_symbol(decl->get_name(), decl->is_skolem());
}
else {
symbol sym = m_renaming.get_symbol(decl->get_name());
symbol sym = m_renaming.get_symbol(decl->get_name(), decl->is_skolem());
visit_params(false, sym, decl->get_num_parameters(), decl->get_parameters());
}
}
@ -498,7 +508,7 @@ class smt_printer {
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
sort* s = q->get_decl_sort(i);
m_out << "(";
print_bound(m_renaming.get_symbol(q->get_decl_name(i)));
print_bound(m_renaming.get_symbol(q->get_decl_name(i), false));
m_out << " ";
visit_sort(s, true);
m_out << ") ";
@ -563,7 +573,7 @@ class smt_printer {
unsigned num_decls = q->get_num_decls();
if (idx < num_decls) {
unsigned offs = num_decls-idx-1;
symbol name = m_renaming.get_symbol(q->get_decl_name(offs));
symbol name = m_renaming.get_symbol(q->get_decl_name(offs), false);
print_bound(name);
return;
}
@ -805,15 +815,15 @@ public:
m_out << ")";
}
m_out << "(";
m_out << m_renaming.get_symbol(d->name());
m_out << m_renaming.get_symbol(d->name(), false);
m_out << " ";
bool first_constr = true;
for (datatype::constructor* f : *d) {
if (!first_constr) m_out << " "; else first_constr = false;
m_out << "(";
m_out << m_renaming.get_symbol(f->name());
m_out << m_renaming.get_symbol(f->name(), false);
for (datatype::accessor* a : *f) {
m_out << " (" << m_renaming.get_symbol(a->name()) << " ";
m_out << " (" << m_renaming.get_symbol(a->name(), false) << " ";
visit_sort(a->range());
m_out << ")";
}

8
src/ast/ast_smt_pp.h
View file

@ -24,8 +24,10 @@ Revision History:
#include "util/map.h"
class smt_renaming {
struct sym_b { symbol name; bool is_skolem; symbol name_aux; sym_b(symbol n, bool s): name(n), is_skolem(s) {} sym_b():name(),is_skolem(false) {}};
typedef map<symbol, symbol, symbol_hash_proc, symbol_eq_proc> symbol2symbol;
symbol2symbol m_translate;
typedef map<symbol, sym_b, symbol_hash_proc, symbol_eq_proc> symbol2sym_b;
symbol2sym_b m_translate;
symbol2symbol m_rev_translate;
symbol fix_symbol(symbol s, int k);
@ -35,8 +37,8 @@ class smt_renaming {
bool all_is_legal(char const* s);
public:
smt_renaming();
symbol get_symbol(symbol s0);
symbol operator()(symbol const & s) { return get_symbol(s); }
symbol get_symbol(symbol s0, bool is_skolem = false);
symbol operator()(symbol const & s, bool is_skolem = false) { return get_symbol(s, is_skolem); }
};
class ast_smt_pp {

48
src/ast/ast_translation.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/format.h"
#include "ast/ast_translation.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
ast_translation::~ast_translation() {
reset_cache();
@ -47,9 +48,10 @@ void ast_translation::reset_cache() {
void ast_translation::cache(ast * s, ast * t) {
SASSERT(!m_cache.contains(s));
if (s->get_ref_count() > 1) {
m_cache.insert(s, t);
m_from_manager.inc_ref(s);
m_to_manager.inc_ref(t);
m_cache.insert(s, t);
++m_insert_count;
}
}
@ -75,10 +77,16 @@ void ast_translation::push_frame(ast * n) {
}
bool ast_translation::visit(ast * n) {
ast * r;
if (n->get_ref_count() > 1 && m_cache.find(n, r)) {
m_result_stack.push_back(r);
return true;
if (n->get_ref_count() > 1) {
ast * r;
if (m_cache.find(n, r)) {
m_result_stack.push_back(r);
++m_hit_count;
return true;
}
else {
++m_miss_count;
}
}
push_frame(n);
return false;
@ -160,7 +168,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
new_fi.set_chainable(fi->is_chainable());
new_fi.set_pairwise(fi->is_pairwise());
new_fi.set_injective(fi->is_injective());
new_fi.set_skolem(fi->is_skolem());
/// TBD new_fi.set_skolem(fi->is_skolem());
new_fi.set_idempotent(fi->is_idempotent());
new_f = m_to_manager.mk_func_decl(f->get_name(),
@ -187,20 +195,32 @@ ast * ast_translation::process(ast const * _n) {
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
++m_num_process;
if (m_num_process > (1 << 14)) {
reset_cache();
m_num_process = 0;
}
if (!visit(const_cast<ast*>(_n))) {
while (!m_frame_stack.empty()) {
loop:
++m_loop_count;
frame & fr = m_frame_stack.back();
ast * n = fr.m_n;
ast * r;
TRACE("ast_translation", tout << mk_ll_pp(n, m_from_manager, false) << "\n";);
if (fr.m_idx == 0 && n->get_ref_count() > 1 && m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
continue;
if (fr.m_idx == 0 && n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
m_hit_count++;
continue;
}
else {
m_miss_count++;
}
}
switch (n->get_kind()) {
case AST_VAR: {
@ -227,7 +247,7 @@ ast * ast_translation::process(ast const * _n) {
while (fr.m_idx <= num) {
expr * arg = to_app(n)->get_arg(fr.m_idx - 1);
fr.m_idx++;
if (!visit(arg))
if (!visit(arg))
goto loop;
}
func_decl * new_f = to_func_decl(m_result_stack[fr.m_rpos]);

38
src/ast/ast_translation.h
View file

@ -37,6 +37,11 @@ class ast_translation {
ptr_vector<ast> m_extra_children_stack; // for sort and func_decl, since they have nested AST in their parameters
ptr_vector<ast> m_result_stack;
obj_map<ast, ast*> m_cache;
unsigned m_loop_count;
unsigned m_hit_count;
unsigned m_miss_count;
unsigned m_insert_count;
unsigned m_num_process;
void cache(ast * s, ast * t);
void collect_decl_extra_children(decl * d);
@ -50,25 +55,53 @@ class ast_translation {
public:
ast_translation(ast_manager & from, ast_manager & to, bool copy_plugins = true) : m_from_manager(from), m_to_manager(to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
m_loop_count = 0;
m_hit_count = 0;
m_miss_count = 0;
m_insert_count = 0;
m_num_process = 0;
if (&from != &to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
m_to_manager.update_fresh_id(m_from_manager);
}
}
~ast_translation();
template<typename T>
T * operator()(T const * n) {
return translate(n);
}
template<typename T>
T * translate(T const * n) {
if (&from() == &to()) return const_cast<T*>(n);
SASSERT(!n || from().contains(const_cast<T*>(n)));
ast * r = process(n);
SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
return static_cast<T*>(r);
}
ast_manager & from() const { return m_from_manager; }
ast_manager & to() const { return m_to_manager; }
template<typename T>
ref_vector<T, ast_manager> operator()(ref_vector<T, ast_manager> const& src) {
ref_vector<T, ast_manager> dst(to());
for (expr* v : src) dst.push_back(translate(v));
return dst;
}
void reset_cache();
void cleanup();
unsigned loop_count() const { return m_loop_count; }
unsigned hit_count() const { return m_hit_count; }
unsigned miss_count() const { return m_miss_count; }
unsigned insert_count() const { return m_insert_count; }
unsigned long long get_num_collision() const { return m_cache.get_num_collision(); }
};
// Translation with non-persistent cache.
@ -80,6 +113,7 @@ inline expr * translate(expr const * e, ast_manager & from, ast_manager & to) {
return ast_translation(from, to)(e);
}
class expr_dependency_translation {
ast_translation & m_translation;
ptr_vector<expr> m_buffer;

2
src/ast/bv_decl_plugin.cpp
View file

@ -717,7 +717,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT));
op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
if (logic == symbol::null || logic == symbol("ALL")) {
if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD") {
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));

28
src/ast/decl_collector.cpp
View file

@ -21,14 +21,13 @@ Revision History:
#include "ast/ast_pp.h"
void decl_collector::visit_sort(sort * n) {
SASSERT(!m_visited.is_marked(n));
family_id fid = n->get_family_id();
if (m().is_uninterp(n))
m_sorts.push_back(n);
if (fid == m_dt_fid) {
else if (fid == m_dt_fid) {
m_sorts.push_back(n);
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
for (func_decl * cnstr : *m_dt_util.get_datatype_constructors(n)) {
m_todo.push_back(cnstr);
ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
unsigned num_cas = cnstr_acc.size();
@ -48,12 +47,15 @@ bool decl_collector::is_bool(sort * s) {
}
void decl_collector::visit_func(func_decl * n) {
family_id fid = n->get_family_id();
if (fid == null_family_id) {
if (m_sep_preds && is_bool(n->get_range()))
m_preds.push_back(n);
else
m_decls.push_back(n);
if (!m_visited.is_marked(n)) {
family_id fid = n->get_family_id();
if (fid == null_family_id) {
if (m_sep_preds && is_bool(n->get_range()))
m_preds.push_back(n);
else
m_decls.push_back(n);
}
m_visited.mark(n, true);
}
}
@ -72,7 +74,6 @@ void decl_collector::visit(ast* n) {
n = m_todo.back();
m_todo.pop_back();
if (!m_visited.is_marked(n)) {
m_visited.mark(n, true);
switch(n->get_kind()) {
case AST_APP: {
app * a = to_app(n);
@ -99,8 +100,8 @@ void decl_collector::visit(ast* n) {
break;
case AST_FUNC_DECL: {
func_decl * d = to_func_decl(n);
for (unsigned i = 0; i < d->get_arity(); ++i) {
m_todo.push_back(d->get_domain(i));
for (sort* srt : *d) {
m_todo.push_back(srt);
}
m_todo.push_back(d->get_range());
visit_func(d);
@ -111,6 +112,7 @@ void decl_collector::visit(ast* n) {
default:
UNREACHABLE();
}
m_visited.mark(n, true);
}
}
}

4
src/ast/decl_collector.h
View file

@ -38,7 +38,6 @@ class decl_collector {
void visit_sort(sort* n);
bool is_bool(sort* s);
void visit_func(func_decl* n);
typedef obj_hashtable<sort> sort_set;
sort_set* collect_deps(sort* s);
@ -48,9 +47,10 @@ class decl_collector {
public:
// if preds == true, then predicates are stored in a separate collection.
decl_collector(ast_manager & m, bool preds=true);
decl_collector(ast_manager & m, bool preds = true);
ast_manager & m() { return m_manager; }
void visit_func(func_decl* n);
void visit(ast * n);
void visit(unsigned n, expr* const* es);
void visit(expr_ref_vector const& es);

8
src/ast/expr2var.cpp
View file

@ -58,11 +58,9 @@ void expr2var::display(std::ostream & out) const {
}
void expr2var::mk_inv(expr_ref_vector & var2expr) const {
obj_map<expr, var>::iterator it = m_mapping.begin();
obj_map<expr, var>::iterator end = m_mapping.end();
for (; it != end; ++it) {
expr * t = it->m_key;
var x = it->m_value;
for (auto & kv : m_mapping) {
expr * t = kv.m_key;
var x = kv.m_value;
if (x >= var2expr.size())
var2expr.resize(x+1, nullptr);
var2expr.set(x, t);

2
src/ast/pattern/pattern_inference.cpp
View file

@ -710,7 +710,7 @@ bool pattern_inference_cfg::reduce_quantifier(
result = new_q;
IF_IVERBOSE(10,
IF_VERBOSE(10,
verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n";
for (unsigned i = 0; i < new_patterns.size(); i++)
verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n";

18
src/ast/pb_decl_plugin.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "ast/pb_decl_plugin.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
pb_decl_plugin::pb_decl_plugin():
m_at_most_sym("at-most"),
@ -54,7 +55,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
func_decl_info info(m_family_id, k, 1, parameters);
return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
}
}
case OP_PB_GE:
case OP_PB_LE:
case OP_PB_EQ: {
@ -128,9 +129,15 @@ app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const *
normalize(num_args, coeffs, k);
m_params.reset();
m_params.push_back(parameter(floor(m_k)));
bool all_ones = true;
for (unsigned i = 0; i < num_args; ++i) {
all_ones &= m_coeffs[i].is_one();
m_params.push_back(parameter(m_coeffs[i]));
}
if (all_ones && k.is_unsigned()) {
m_params[0] = parameter(floor(m_k).get_unsigned());
return m.mk_app(m_fid, OP_AT_MOST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
return m.mk_app(m_fid, OP_PB_LE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
@ -138,9 +145,15 @@ app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const *
normalize(num_args, coeffs, k);
m_params.reset();
m_params.push_back(parameter(ceil(m_k)));
bool all_ones = true;
for (unsigned i = 0; i < num_args; ++i) {
all_ones &= m_coeffs[i].is_one();
m_params.push_back(parameter(m_coeffs[i]));
}
if (all_ones && k.is_unsigned()) {
m_params[0] = parameter(ceil(m_k).get_unsigned());
return m.mk_app(m_fid, OP_AT_LEAST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
return m.mk_app(m_fid, OP_PB_GE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
@ -149,6 +162,9 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const *
if (!m_k.is_int()) {
return m.mk_false();
}
if (num_args == 0) {
return m_k.is_zero() ? m.mk_true() : m.mk_false();
}
m_params.reset();
m_params.push_back(parameter(m_k));
for (unsigned i = 0; i < num_args; ++i) {

1
src/ast/pb_decl_plugin.h
View file

@ -123,7 +123,6 @@ public:
app* mk_fresh_bool();
private:
rational to_rational(parameter const& p) const;
};

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

@ -800,9 +800,54 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = m_util.mk_numeral(div(v1, v2), is_int);
return BR_DONE;
}
expr_ref quot(m());
if (divides(arg1, arg2, quot)) {
result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
return BR_REWRITE2;
}
return BR_FAILED;
}
bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
if (d == n) {
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
return true;
}
if (m_util.is_mul(n)) {
expr_ref_vector muls(m());
muls.push_back(n);
expr* n1, *n2;
rational r1, r2;
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_mul(muls[i].get(), n1, n2)) {
muls[i] = n1;
muls.push_back(n2);
--i;
}
}
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
else {
for (unsigned i = 0; i < muls.size(); ++i) {
if (d == muls[i].get()) {
muls[i] = muls.back();
muls.pop_back();
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
}
return false;
}
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(m().get_sort(arg1));
numeral v1, v2;

1
src/ast/rewriter/arith_rewriter.h
View file

@ -95,6 +95,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
expr_ref neg_monomial(expr * e) const;
expr * mk_sin_value(rational const & k);
app * mk_sqrt(rational const & k);
bool divides(expr* d, expr* n, expr_ref& quot);
public:
arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):

34
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -92,6 +92,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
func_decl_ref_vector m_keys;
expr_ref_vector m_values;
unsigned_vector m_keyval_lim;
func_decl_ref_vector m_newbits;
unsigned_vector m_newbits_lim;
bool m_blast_mul;
bool m_blast_add;
@ -118,7 +120,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_out(m),
m_bindings(m),
m_keys(m),
m_values(m) {
m_values(m),
m_newbits(m) {
updt_params(p);
}
@ -160,6 +163,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
void push() {
m_keyval_lim.push_back(m_keys.size());
m_newbits_lim.push_back(m_newbits.size());
}
unsigned get_num_scopes() const {
@ -178,9 +182,27 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_keys.resize(lim);
m_values.resize(lim);
m_keyval_lim.resize(new_sz);
lim = m_newbits_lim[new_sz];
m_newbits.shrink(lim);
m_newbits_lim.shrink(new_sz);
}
}
unsigned m_keypos;
void start_rewrite() {
m_keypos = m_keys.size();
}
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
const2bits.insert(m_keys[i].get(), m_values[i].get());
}
for (func_decl* f : m_newbits) newbits.push_back(f);
}
template<typename V>
app * mk_mkbv(V const & bits) {
return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@ -201,6 +223,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_out.reset();
for (unsigned i = 0; i < bv_size; i++) {
m_out.push_back(m().mk_fresh_const(nullptr, b));
m_newbits.push_back(to_app(m_out.back())->get_decl());
}
r = mk_mkbv(m_out);
m_const2bits.insert(f, r);
@ -635,6 +658,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
}
void push() { m_cfg.push(); }
void pop(unsigned s) { m_cfg.pop(s); }
void start_rewrite() { m_cfg.start_rewrite(); }
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) { m_cfg.end_rewrite(const2bits, newbits); }
unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
};
@ -683,3 +708,10 @@ unsigned bit_blaster_rewriter::get_num_scopes() const {
return m_imp->get_num_scopes();
}
void bit_blaster_rewriter::start_rewrite() {
m_imp->start_rewrite();
}
void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
m_imp->end_rewrite(const2bits, newbits);
}

6
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
View file

@ -33,11 +33,15 @@ public:
ast_manager & m() const;
unsigned get_num_steps() const;
void cleanup();
obj_map<func_decl, expr*> const& const2bits() const;
void start_rewrite();
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits);
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);
unsigned get_num_scopes() const;
private:
obj_map<func_decl, expr*> const& const2bits() const;
};
#endif

612
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -25,6 +25,10 @@ Notes:
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "util/lbool.h"
#include "util/uint_set.h"
#include "util/gparams.h"
const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
struct pb2bv_rewriter::imp {
@ -35,6 +39,8 @@ struct pb2bv_rewriter::imp {
func_decl_ref_vector m_fresh; // all fresh variables
unsigned_vector m_fresh_lim;
unsigned m_num_translated;
unsigned m_compile_bv;
unsigned m_compile_card;
struct card2bv_rewriter {
typedef expr* literal;
@ -49,6 +55,9 @@ struct pb2bv_rewriter::imp {
expr_ref_vector m_args;
rational m_k;
vector<rational> m_coeffs;
bool m_keep_cardinality_constraints;
symbol m_pb_solver;
unsigned m_min_arity;
template<lbool is_le>
expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@ -68,7 +77,28 @@ struct pb2bv_rewriter::imp {
fmls.push_back(bv.mk_ule(bound, result));
}
return result;
}
typedef std::pair<rational, expr_ref> ca;
struct compare_coeffs {
bool operator()(ca const& x, ca const& y) const {
return x.first > y.first;
}
};
void sort_args() {
vector<ca> cas;
for (unsigned i = 0; i < m_args.size(); ++i) {
cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m)));
}
std::sort(cas.begin(), cas.end(), compare_coeffs());
m_coeffs.reset();
m_args.reset();
for (ca const& ca : cas) {
m_coeffs.push_back(ca.first);
m_args.push_back(ca.second);
}
}
//
@ -84,21 +114,25 @@ struct pb2bv_rewriter::imp {
// is_le = l_false - >=
//
template<lbool is_le>
expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
expr_ref mk_le_ge(rational const & k) {
//sort_args();
unsigned sz = m_args.size();
expr * const* args = m_args.c_ptr();
TRACE("pb",
for (unsigned i = 0; i < sz; ++i) {
tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
}
switch (is_le) {
case l_true: tout << "<= "; break;
case l_true: tout << "<= "; break;
case l_undef: tout << "= "; break;
case l_false: tout << ">= "; break;
}
tout << m_k << "\n";);
tout << k << "\n";);
if (k.is_zero()) {
if (is_le != l_false) {
return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
return expr_ref(m.mk_not(::mk_or(m_args)), m);
}
else {
return expr_ref(m.mk_true(), m);
@ -107,6 +141,35 @@ struct pb2bv_rewriter::imp {
if (k.is_neg()) {
return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
}
if (m_pb_solver == "totalizer") {
expr_ref result(m);
switch (is_le) {
case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break;
case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break;
case l_undef: break;
}
}
if (m_pb_solver == "sorting") {
expr_ref result(m);
switch (is_le) {
case l_true: if (mk_le(sz, args, k, result)) return result; else break;
case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
}
}
if (m_pb_solver == "segmented") {
expr_ref result(m);
switch (is_le) {
case l_true: return mk_seg_le(k);
case l_false: return mk_seg_ge(k);
case l_undef: break;
}
}
// fall back to divide and conquer encoding.
SASSERT(k.is_pos());
expr_ref zero(m), bound(m);
expr_ref_vector es(m), fmls(m);
@ -138,12 +201,12 @@ struct pb2bv_rewriter::imp {
}
switch (is_le) {
case l_true:
return mk_and(fmls);
return ::mk_and(fmls);
case l_false:
if (!es.empty()) {
fmls.push_back(bv.mk_ule(bound, es.back()));
}
return mk_or(fmls);
return ::mk_or(fmls);
case l_undef:
if (es.empty()) {
fmls.push_back(m.mk_bool_val(k.is_zero()));
@ -151,35 +214,415 @@ struct pb2bv_rewriter::imp {
else {
fmls.push_back(m.mk_eq(bound, es.back()));
}
return mk_and(fmls);
return ::mk_and(fmls);
default:
UNREACHABLE();
return expr_ref(m.mk_true(), m);
}
}
/**
\brief Totalizer encoding. Based on a version by Miguel.
*/
bool mk_le_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
SASSERT(sz == m_coeffs.size());
if (!_k.is_unsigned() || sz == 0) return false;
unsigned k = _k.get_unsigned();
expr_ref_vector args1(m);
rational bound;
flip(sz, args, args1, _k, bound);
if (bound.get_unsigned() < k) {
return mk_ge_tot(sz, args1.c_ptr(), bound, result);
}
if (k > 20) {
return false;
}
result = m.mk_not(bounded_addition(sz, args, k + 1));
TRACE("pb", tout << result << "\n";);
return true;
}
bool mk_ge_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
SASSERT(sz == m_coeffs.size());
if (!_k.is_unsigned() || sz == 0) return false;
unsigned k = _k.get_unsigned();
expr_ref_vector args1(m);
rational bound;
flip(sz, args, args1, _k, bound);
if (bound.get_unsigned() < k) {
return mk_le_tot(sz, args1.c_ptr(), bound, result);
}
if (k > 20) {
return false;
}
result = bounded_addition(sz, args, k);
TRACE("pb", tout << result << "\n";);
return true;
}
void flip(unsigned sz, expr* const* args, expr_ref_vector& args1, rational const& k, rational& bound) {
bound = -k;
for (unsigned i = 0; i < sz; ++i) {
args1.push_back(mk_not(args[i]));
bound += m_coeffs[i];
}
}
expr_ref bounded_addition(unsigned sz, expr * const * args, unsigned k) {
SASSERT(sz > 0);
expr_ref result(m);
vector<expr_ref_vector> es;
vector<unsigned_vector> coeffs;
for (unsigned i = 0; i < m_coeffs.size(); ++i) {
unsigned_vector v;
expr_ref_vector e(m);
unsigned c = m_coeffs[i].get_unsigned();
v.push_back(c >= k ? k : c);
e.push_back(args[i]);
es.push_back(e);
coeffs.push_back(v);
}
while (es.size() > 1) {
for (unsigned i = 0; i + 1 < es.size(); i += 2) {
expr_ref_vector o(m);
unsigned_vector oc;
tot_adder(es[i], coeffs[i], es[i + 1], coeffs[i + 1], k, o, oc);
es[i / 2].set(o);
coeffs[i / 2] = oc;
}
if ((es.size() % 2) == 1) {
es[es.size() / 2].set(es.back());
coeffs[es.size() / 2] = coeffs.back();
}
es.shrink((1 + es.size())/2);
coeffs.shrink((1 + coeffs.size())/2);
}
SASSERT(coeffs.size() == 1);
SASSERT(coeffs[0].back() <= k);
if (coeffs[0].back() == k) {
result = es[0].back();
}
else {
result = m.mk_false();
}
return result;
}
void tot_adder(expr_ref_vector const& l, unsigned_vector const& lc,
expr_ref_vector const& r, unsigned_vector const& rc,
unsigned k,
expr_ref_vector& o, unsigned_vector & oc) {
SASSERT(l.size() == lc.size());
SASSERT(r.size() == rc.size());
uint_set sums;
vector<expr_ref_vector> trail;
u_map<unsigned> sum2def;
for (unsigned i = 0; i <= l.size(); ++i) {
for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
sums.insert(sum);
}
}
for (unsigned u : sums) {
oc.push_back(u);
}
std::sort(oc.begin(), oc.end());
DEBUG_CODE(
for (unsigned i = 0; i + 1 < oc.size(); ++i) {
SASSERT(oc[i] < oc[i+1]);
});
for (unsigned i = 0; i < oc.size(); ++i) {
sum2def.insert(oc[i], i);
trail.push_back(expr_ref_vector(m));
}
for (unsigned i = 0; i <= l.size(); ++i) {
for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
if (i != 0 && j != 0 && (lc[i - 1] >= k || rc[j - 1] >= k)) continue;
unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
expr_ref_vector ands(m);
if (i != 0) {
ands.push_back(l[i - 1]);
}
if (j != 0) {
ands.push_back(r[j - 1]);
}
trail[sum2def.find(sum)].push_back(::mk_and(ands));
}
}
for (unsigned i = 0; i < oc.size(); ++i) {
o.push_back(::mk_or(trail[sum2def.find(oc[i])]));
}
}
/**
\brief MiniSat+ based encoding of PB constraints.
The procedure is described in "Translating Pseudo-Boolean Constraints into SAT "
         Niklas Een, Niklas Sörensson, JSAT 2006.
*/
vector<rational> m_min_base;
rational m_min_cost;
vector<rational> m_base;
void create_basis(vector<rational> const& seq, rational carry_in, rational cost) {
if (cost >= m_min_cost) {
return;
}
rational delta_cost(0);
for (unsigned i = 0; i < seq.size(); ++i) {
delta_cost += seq[i];
}
if (cost + delta_cost < m_min_cost) {
m_min_cost = cost + delta_cost;
m_min_base = m_base;
m_min_base.push_back(delta_cost + rational::one());
}
for (unsigned i = 0; i < sizeof(g_primes)/sizeof(*g_primes); ++i) {
vector<rational> seq1;
rational p(g_primes[i]);
rational rest = carry_in;
// create seq1
for (unsigned j = 0; j < seq.size(); ++j) {
rest += seq[j] % p;
if (seq[j] >= p) {
seq1.push_back(div(seq[j], p));
}
}
m_base.push_back(p);
create_basis(seq1, div(rest, p), cost + rest);
m_base.pop_back();
}
}
bool create_basis() {
m_base.reset();
m_min_cost = rational(INT_MAX);
m_min_base.reset();
rational cost(0);
create_basis(m_coeffs, rational::zero(), cost);
m_base = m_min_base;
TRACE("pb",
tout << "Base: ";
for (unsigned i = 0; i < m_base.size(); ++i) {
tout << m_base[i] << " ";
}
tout << "\n";);
return
!m_base.empty() &&
m_base.back().is_unsigned() &&
m_base.back().get_unsigned() <= 20*m_base.size();
}
/**
\brief Check if 'out mod n >= lim'.
*/
expr_ref mod_ge(ptr_vector<expr> const& out, unsigned n, unsigned lim) {
TRACE("pb", for (unsigned i = 0; i < out.size(); ++i) tout << mk_pp(out[i], m) << " "; tout << "\n";
tout << "n:" << n << " lim: " << lim << "\n";);
if (lim == n) {
return expr_ref(m.mk_false(), m);
}
if (lim == 0) {
return expr_ref(m.mk_true(), m);
}
SASSERT(0 < lim && lim < n);
expr_ref_vector ors(m);
for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
expr_ref tmp(m);
tmp = out[j + lim - 1];
if (j + n - 1 < out.size()) {
tmp = m.mk_and(tmp, m.mk_not(out[j + n - 1]));
}
ors.push_back(tmp);
}
return ::mk_or(ors);
}
// x0 + 5x1 + 3x2 >= k
// x0 x1 x1 -> s0 s1 s2
// s2 x1 x2 -> s3 s4 s5
// k = 7: s5 or (s4 & not s2 & s0)
// k = 6: s4
// k = 5: s4 or (s3 & not s2 & s1)
// k = 4: s4 or (s3 & not s2 & s0)
// k = 3: s3
//
bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
if (!create_basis()) return false;
if (!bound.is_unsigned()) return false;
vector<rational> coeffs(m_coeffs);
result = m.mk_true();
expr_ref_vector carry(m), new_carry(m);
m_base.push_back(bound + rational::one());
for (rational b_i : m_base) {
unsigned B = b_i.get_unsigned();
unsigned d_i = (bound % b_i).get_unsigned();
bound = div(bound, b_i);
for (unsigned j = 0; j < coeffs.size(); ++j) {
rational c = coeffs[j] % b_i;
SASSERT(c.is_unsigned());
for (unsigned k = 0; k < c.get_unsigned(); ++k) {
carry.push_back(args[j]);
}
coeffs[j] = div(coeffs[j], b_i);
}
TRACE("pb", tout << "Carry: " << carry << "\n";
for (auto c : coeffs) tout << c << " ";
tout << "\n";
);
ptr_vector<expr> out;
m_sort.sorting(carry.size(), carry.c_ptr(), out);
expr_ref gt = mod_ge(out, B, d_i + 1);
expr_ref ge = mod_ge(out, B, d_i);
result = mk_and(ge, result);
result = mk_or(gt, result);
TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";);
new_carry.reset();
for (unsigned j = B - 1; j < out.size(); j += B) {
new_carry.push_back(out[j]);
}
carry.reset();
carry.append(new_carry);
}
TRACE("pb", tout << "bound: " << bound << " Carry: " << carry << " result: " << result << "\n";);
return true;
}
/**
\brief Segment based encoding.
The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient.
The segments are sorted, such that the segment with highest coefficient is first.
Then for each segment create circuits based on sorting networks the arguments of the segment.
*/
expr_ref mk_seg_ge(rational const& k) {
rational bound(-k);
for (unsigned i = 0; i < m_args.size(); ++i) {
m_args[i] = mk_not(m_args[i].get());
bound += m_coeffs[i];
}
return mk_seg_le(bound);
}
expr_ref mk_seg_le(rational const& k) {
sort_args();
unsigned sz = m_args.size();
expr* const* args = m_args.c_ptr();
// Create sorted entries.
vector<ptr_vector<expr>> outs;
vector<rational> coeffs;
for (unsigned i = 0, seg_size = 0; i < sz; i += seg_size) {
seg_size = segment_size(i);
ptr_vector<expr> out;
m_sort.sorting(seg_size, args + i, out);
out.push_back(m.mk_false());
outs.push_back(out);
coeffs.push_back(m_coeffs[i]);
}
return mk_seg_le_rec(outs, coeffs, 0, k);
}
expr_ref mk_seg_le_rec(vector<ptr_vector<expr>> const& outs, vector<rational> const& coeffs, unsigned i, rational const& k) {
rational const& c = coeffs[i];
ptr_vector<expr> const& out = outs[i];
if (k.is_neg()) {
return expr_ref(m.mk_false(), m);
}
if (i == outs.size()) {
return expr_ref(m.mk_true(), m);
}
if (i + 1 == outs.size() && k >= rational(out.size()-1)*c) {
return expr_ref(m.mk_true(), m);
}
expr_ref_vector fmls(m);
fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k)));
rational k1;
for (unsigned j = 0; j + 1 < out.size(); ++j) {
k1 = k - rational(j+1)*c;
if (k1.is_neg()) {
fmls.push_back(m.mk_not(out[j]));
break;
}
fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1)));
}
return ::mk_and(fmls);
}
// The number of arguments with the same coefficient.
unsigned segment_size(unsigned start) const {
unsigned i = start;
while (i < m_args.size() && m_coeffs[i] == m_coeffs[start]) ++i;
return i - start;
}
expr_ref mk_and(expr_ref& a, expr_ref& b) {
if (m.is_true(a)) return b;
if (m.is_true(b)) return a;
if (m.is_false(a)) return a;
if (m.is_false(b)) return b;
return expr_ref(m.mk_and(a, b), m);
}
expr_ref mk_or(expr_ref& a, expr_ref& b) {
if (m.is_true(a)) return a;
if (m.is_true(b)) return b;
if (m.is_false(a)) return b;
if (m.is_false(b)) return a;
return expr_ref(m.mk_or(a, b), m);
}
bool mk_le(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
expr_ref_vector args1(m);
rational bound(-k);
for (unsigned i = 0; i < sz; ++i) {
args1.push_back(mk_not(args[i]));
bound += m_coeffs[i];
}
return mk_ge(sz, args1.c_ptr(), bound, result);
}
bool mk_eq(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
expr_ref r1(m), r2(m);
if (mk_ge(sz, args, k, r1) && mk_le(sz, args, k, r2)) {
result = m.mk_and(r1, r2);
return true;
}
else {
return false;
}
}
expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
++m_imp.m_compile_bv;
decl_kind kind = f->get_decl_kind();
rational k = pb.get_k(f);
m_coeffs.reset();
m_args.reset();
for (unsigned i = 0; i < sz; ++i) {
m_coeffs.push_back(pb.get_coeff(f, i));
m_args.push_back(args[i]);
}
CTRACE("pb", k.is_neg(), tout << expr_ref(m.mk_app(f, sz, args), m) << "\n";);
SASSERT(!k.is_neg());
switch (kind) {
case OP_PB_GE:
case OP_AT_LEAST_K: {
expr_ref_vector nargs(m);
nargs.append(sz, args);
dualize(f, nargs, k);
dualize(f, m_args, k);
SASSERT(!k.is_neg());
return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
return mk_le_ge<l_true>(k);
}
case OP_PB_LE:
case OP_AT_MOST_K:
return mk_le_ge<l_true>(sz, args, k);
return mk_le_ge<l_true>(k);
case OP_PB_EQ:
return mk_le_ge<l_undef>(sz, args, k);
return mk_le_ge<l_undef>(k);
default:
UNREACHABLE();
return expr_ref(m.mk_true(), m);
@ -230,7 +673,7 @@ struct pb2bv_rewriter::imp {
public:
card2bv_rewriter(imp& i, ast_manager& m):
card2bv_rewriter(imp& i, ast_manager& m):
m_sort(*this),
m(m),
m_imp(i),
@ -238,29 +681,34 @@ struct pb2bv_rewriter::imp {
pb(m),
bv(m),
m_trail(m),
m_args(m)
m_args(m),
m_keep_cardinality_constraints(false),
m_pb_solver(symbol("solver")),
m_min_arity(9)
{}
void set_pb_solver(symbol const& s) { m_pb_solver = s; }
bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
if (f->get_family_id() == pb.get_family_id()) {
mk_pb(full, f, sz, args, result);
if (f->get_family_id() == pb.get_family_id() && mk_pb(full, f, sz, args, result)) {
// skip
}
else if (au.is_le(f) && is_pb(args[0], args[1])) {
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_lt(f) && is_pb(args[0], args[1])) {
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_ge(f) && is_pb(args[1], args[0])) {
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_gt(f) && is_pb(args[1], args[0])) {
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (m.is_eq(f) && is_pb(args[0], args[1])) {
result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_undef>(m_k);
}
else {
return false;
@ -278,6 +726,11 @@ struct pb2bv_rewriter::imp {
}
}
bool mk_app(expr* e, expr_ref& r) {
app* a;
return (is_app(e) && (a = to_app(e), mk_app(false, a->get_decl(), a->get_num_args(), a->get_args(), r)));
}
bool is_pb(expr* x, expr* y) {
m_args.reset();
m_coeffs.reset();
@ -349,29 +802,62 @@ struct pb2bv_rewriter::imp {
return false;
}
void mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
SASSERT(f->get_family_id() == pb.get_family_id());
if (is_or(f)) {
result = m.mk_or(sz, args);
}
else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
++m_imp.m_compile_card;
}
else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
++m_imp.m_compile_card;
}
else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args);
++m_imp.m_compile_card;
}
else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
++m_imp.m_compile_card;
}
else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
++m_imp.m_compile_card;
}
else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
return false;
}
else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
return false;
}
else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
return false;
}
else {
result = mk_bv(f, sz, args);
}
return true;
}
bool has_small_coefficients(func_decl* f) {
unsigned sz = f->get_arity();
unsigned sum = 0;
for (unsigned i = 0; i < sz; ++i) {
rational c = pb.get_coeff(f, i);
if (!c.is_unsigned()) return false;
unsigned sum1 = sum + c.get_unsigned();
if (sum1 < sum) return false;
sum = sum1;
}
return true;
}
// definitions used for sorting network
@ -387,15 +873,22 @@ struct pb2bv_rewriter::imp {
m_trail.push_back(l);
return l;
}
literal fresh() {
expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m);
literal fresh(char const* n) {
expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m);
m_imp.m_fresh.push_back(to_app(fr)->get_decl());
return trail(fr);
}
void mk_clause(unsigned n, literal const* lits) {
m_imp.m_lemmas.push_back(mk_or(m, n, lits));
m_imp.m_lemmas.push_back(::mk_or(m, n, lits));
}
void keep_cardinality_constraints(bool f) {
m_keep_cardinality_constraints = f;
}
void set_at_most1(sorting_network_encoding enc) { m_sort.cfg().m_encoding = enc; }
};
struct card2bv_rewriter_cfg : public default_rewriter_cfg {
@ -407,6 +900,10 @@ struct pb2bv_rewriter::imp {
return m_r.mk_app_core(f, num, args, result);
}
card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
void set_pb_solver(symbol const& s) { m_r.set_pb_solver(s); }
void set_at_most1(sorting_network_encoding enc) { m_r.set_at_most1(enc); }
};
class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
@ -415,22 +912,77 @@ struct pb2bv_rewriter::imp {
card_pb_rewriter(imp& i, ast_manager & m):
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
m_cfg(i, m) {}
void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); }
void set_at_most1(sorting_network_encoding e) { m_cfg.set_at_most1(e); }
void rewrite(expr* e, expr_ref& r, proof_ref& p) {
expr_ref ee(e, m());
if (m_cfg.m_r.mk_app(e, r)) {
ee = r;
// mp proof?
}
(*this)(ee, r, p);
}
};
card_pb_rewriter m_rw;
bool keep_cardinality() const {
params_ref const& p = m_params;
return
p.get_bool("keep_cardinality_constraints", false) ||
p.get_bool("sat.cardinality.solver", false) ||
p.get_bool("cardinality.solver", false) ||
gparams::get_module("sat").get_bool("cardinality.solver", false);
}
symbol pb_solver() const {
params_ref const& p = m_params;
symbol s = p.get_sym("sat.pb.solver", symbol());
if (s != symbol()) return s;
s = p.get_sym("pb.solver", symbol());
if (s != symbol()) return s;
return gparams::get_module("sat").get_sym("pb.solver", symbol("solver"));
}
sorting_network_encoding atmost1_encoding() const {
symbol enc = m_params.get_sym("atmost1_encoding", symbol());
if (enc == symbol()) {
enc = gparams::get_module("sat").get_sym("atmost1_encoding", symbol());
}
if (enc == symbol("grouped")) return sorting_network_encoding::grouped_at_most_1;
if (enc == symbol("bimander")) return sorting_network_encoding::bimander_at_most_1;
if (enc == symbol("ordered")) return sorting_network_encoding::ordered_at_most_1;
return grouped_at_most_1;
}
imp(ast_manager& m, params_ref const& p):
m(m), m_params(p), m_lemmas(m),
m_fresh(m),
m_num_translated(0),
m_rw(*this, m) {
updt_params(p);
m_compile_bv = 0;
m_compile_card = 0;
}
void updt_params(params_ref const & p) {
m_params.append(p);
m_rw.keep_cardinality_constraints(keep_cardinality());
m_rw.set_pb_solver(pb_solver());
m_rw.set_at_most1(atmost1_encoding());
}
void collect_param_descrs(param_descrs& r) const {
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver");
}
void updt_params(params_ref const & p) {}
unsigned get_num_steps() const { return m_rw.get_num_steps(); }
void cleanup() { m_rw.cleanup(); }
void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
m_rw(e, result, result_proof);
// m_rw(e, result, result_proof);
m_rw.rewrite(e, result, result_proof);
}
void push() {
m_fresh_lim.push_back(m_fresh.size());
@ -453,6 +1005,8 @@ struct pb2bv_rewriter::imp {
}
void collect_statistics(statistics & st) const {
st.update("pb-compile-bv", m_compile_bv);
st.update("pb-compile-card", m_compile_card);
st.update("pb-aux-variables", m_fresh.size());
st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses);
}
@ -463,6 +1017,8 @@ struct pb2bv_rewriter::imp {
pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
void pb2bv_rewriter::collect_param_descrs(param_descrs& r) const { m_imp->collect_param_descrs(r); }
ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }

1
src/ast/rewriter/pb2bv_rewriter.h
View file

@ -31,6 +31,7 @@ public:
~pb2bv_rewriter();
void updt_params(params_ref const & p);
void collect_param_descrs(param_descrs& r) const;
ast_manager & m() const;
unsigned get_num_steps() const;
void cleanup();

66
src/ast/rewriter/pb_rewriter.cpp
View file

@ -115,14 +115,15 @@ expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
else {
tmp = a.mk_add(es.size(), es.c_ptr());
}
rational k = util.get_k(fml);
if (util.is_le(fml)) {
result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
result = a.mk_le(tmp, a.mk_numeral(k, false));
}
else if (util.is_ge(fml)) {
result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
result = a.mk_ge(tmp, a.mk_numeral(k, false));
}
else {
result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
result = m().mk_eq(tmp, a.mk_numeral(k, false));
}
}
else {
@ -233,6 +234,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
}
bool is_eq = f->get_decl_kind() == OP_PB_EQ;
br_status st = BR_DONE;
pb_ast_rewriter_util pbu(m);
pb_rewriter_util<pb_ast_rewriter_util> util(pbu);
@ -250,29 +252,73 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
default: {
bool all_unit = true;
unsigned sz = vec.size();
rational slack(0);
m_args.reset();
m_coeffs.reset();
for (unsigned i = 0; i < sz; ++i) {
m_args.push_back(vec[i].first);
m_coeffs.push_back(vec[i].second);
for (auto const& kv : vec) {
m_args.push_back(kv.first);
m_coeffs.push_back(kv.second);
SASSERT(kv.second.is_pos());
slack += kv.second;
all_unit &= m_coeffs.back().is_one();
}
if (is_eq) {
if (sz == 0) {
result = k.is_zero()?m.mk_true():m.mk_false();
}
else if (k.is_zero()) {
result = mk_not(m, mk_or(m, sz, m_args.c_ptr()));
}
else if (k.is_one() && all_unit && m_args.size() == 1) {
result = m_args.back();
}
else if (slack == k) {
result = mk_and(m, sz, m_args.c_ptr());
}
else {
result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
}
}
else if (all_unit && k.is_one()) {
else if (all_unit && k.is_one() && sz < 10) {
result = mk_or(m, sz, m_args.c_ptr());
}
else if (all_unit && k == rational(sz)) {
result = mk_and(m, sz, m_args.c_ptr());
}
else {
result = m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
expr_ref_vector conj(m), disj(m);
unsigned j = 0;
sz = m_args.size();
for (unsigned i = 0; i < sz; ++i) {
rational& c = m_coeffs[i];
if (slack < c + k) {
conj.push_back(m_args[i]);
slack -= c;
k -= c;
}
else if (c >= k && k.is_pos()) {
disj.push_back(m_args[i]);
}
else {
m_args[j] = m_args[i];
m_coeffs[j] = m_coeffs[i];
++j;
}
}
m_args.shrink(j);
m_coeffs.shrink(j);
sz = j;
if (sz > 0) {
disj.push_back(m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k));
}
if (!disj.empty()) {
conj.push_back(mk_or(disj));
}
result = mk_and(conj);
if (disj.size() > 1 || conj.size() > 1) {
st = BR_REWRITE3;
}
}
break;
}
@ -283,11 +329,11 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
tout << tmp << "\n";
tout << result << "\n";
);
TRACE("pb_validate",
validate_rewrite(f, num_args, args, result););
return BR_DONE;
return st;
}

16
src/ast/rewriter/pb_rewriter_def.h
View file

@ -45,25 +45,25 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
}
}
// remove constants
for (unsigned i = 0; i < args.size(); ++i) {
unsigned j = 0, sz = args.size();
for (unsigned i = 0; i < sz; ++i) {
if (m_util.is_true(args[i].first)) {
k -= args[i].second;
std::swap(args[i], args[args.size()-1]);
args.pop_back();
--i;
}
else if (m_util.is_false(args[i].first)) {
std::swap(args[i], args[args.size()-1]);
args.pop_back();
--i;
// no-op
}
else {
args[j++] = args[i];
}
}
args.shrink(j);
// sort and coalesce arguments:
typename PBU::compare cmp;
std::sort(args.begin(), args.end(), cmp);
// coallesce
unsigned i, j;
unsigned i;
for (i = 0, j = 1; j < args.size(); ++j) {
if (args[i].first == args[j].first) {
args[i].second += args[j].second;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -89,6 +89,7 @@ public:
~re2automaton();
eautomaton* operator()(expr* e);
void set_solver(expr_solver* solver);
bool has_solver() const { return m_solver; }
eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
};

17
src/cmd_context/basic_cmds.cpp
View file

@ -105,19 +105,19 @@ public:
char const * get_descr(cmd_context & ctx) const override {
return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective";
}
unsigned get_arity() const override { return VAR_ARITY; }
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_UINT; }
void set_next_arg(cmd_context & ctx, unsigned index) override { m_index = index; }
void execute(cmd_context & ctx) override {
if (!ctx.is_model_available() || ctx.get_check_sat_result() == nullptr)
throw cmd_exception("model is not available");
model_ref m;
if (ctx.ignore_check())
return;
if (!ctx.is_model_available(m) || !ctx.get_check_sat_result())
throw cmd_exception("model is not available");
if (m_index > 0 && ctx.get_opt()) {
ctx.get_opt()->get_box_model(m, m_index);
}
else {
ctx.get_check_sat_result()->get_model(m);
}
ctx.display_model(m);
}
void reset(cmd_context& ctx) override {
@ -127,10 +127,9 @@ public:
ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
throw cmd_exception("model is not available");
model_ref m;
ctx.get_check_sat_result()->get_model(m);
if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0)
throw cmd_exception("model is not available");
ctx.regular_stream() << "(";
dictionary<macro_decls> const & macros = ctx.get_macros();
bool first = true;
@ -620,7 +619,7 @@ public:
try {
ctx.regular_stream() << gparams::get_value(opt) << std::endl;
}
catch (const gparams::exception & ex) {
catch (const gparams::exception &) {
ctx.print_unsupported(opt, m_line, m_pos);
}
}

64
src/cmd_context/cmd_context.cpp
View file

@ -43,6 +43,7 @@ Notes:
#include "model/model_v2_pp.h"
#include "model/model_params.hpp"
#include "tactic/tactic_exception.h"
#include "tactic/generic_model_converter.h"
#include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h"
#include "cmd_context/interpolant_cmds.h"
@ -396,7 +397,7 @@ protected:
datalog::dl_decl_util m_dlutil;
format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len);
format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len, f->is_skolem());
if (!fs.more_than_one())
return f_name;
if (!fs.clash(f))
@ -406,7 +407,7 @@ protected:
format_ns::format * pp_fdecl_ref_core(symbol const & s, func_decls const & fs, func_decl * f) {
unsigned len;
format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len);
format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len, f->is_skolem());
if (!fs.more_than_one())
return f_name;
return pp_signature(f_name, f);
@ -498,6 +499,7 @@ cmd_context::~cmd_context() {
finalize_tactic_cmds();
finalize_probes();
reset(true);
m_mc0 = nullptr;
m_solver = nullptr;
m_check_sat_result = nullptr;
}
@ -870,6 +872,23 @@ void cmd_context::insert(symbol const & s, object_ref * r) {
m_object_refs.insert(s, r);
}
void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "cmd_context");
if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get());
func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m());
dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
func_decls & fs = e->get_data().m_value;
fs.insert(m(), fn);
VERIFY(fn->get_range() == m().get_sort(t));
m_mc0->add(fn, t);
}
void cmd_context::model_del(func_decl* f) {
if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "cmd_context");
if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get());
m_mc0->hide(f);
}
void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e) {
expr_ref eq(m());
app_ref lhs(m());
@ -1256,8 +1275,8 @@ void cmd_context::reset(bool finalize) {
reset_macros();
reset_func_decls();
restore_assertions(0);
if (m_solver)
m_solver = nullptr;
m_solver = nullptr;
m_mc0 = nullptr;
m_scopes.reset();
m_opt = nullptr;
m_pp_env = nullptr;
@ -1412,7 +1431,8 @@ void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(m_assertions.empty());
return;
}
if (old_sz == m_assertions.size()) return;
if (old_sz == m_assertions.size())
return;
SASSERT(old_sz < m_assertions.size());
SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
restore(m(), m_assertions, old_sz);
@ -1505,7 +1525,12 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex;
}
catch (z3_exception & ex) {
m_solver->set_reason_unknown(ex.msg());
if (m().canceled()) {
m_solver->set_reason_unknown(eh);
}
else {
m_solver->set_reason_unknown(ex.msg());
}
r = l_undef;
}
m_solver->set_status(r);
@ -1517,7 +1542,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
display_sat_result(r);
if (r == l_true) {
complete_model();
validate_model();
}
validate_check_sat_result(r);
@ -1525,9 +1549,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
// get_opt()->display_assignment(regular_stream());
}
if (r == l_true && m_params.m_dump_models) {
model_ref md;
get_check_sat_result()->get_model(md);
model_ref md;
if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
display_model(md);
}
}
@ -1600,6 +1623,7 @@ void cmd_context::display_dimacs() {
void cmd_context::display_model(model_ref& mdl) {
if (mdl) {
if (m_mc0) (*m_mc0)(mdl);
model_params p;
if (p.v1() || p.v2()) {
std::ostringstream buffer;
@ -1691,14 +1715,10 @@ struct contains_underspecified_op_proc {
/**
\brief Complete the model if necessary.
*/
void cmd_context::complete_model() {
if (!is_model_available() ||
gparams::get_value("model.completion") != "true")
void cmd_context::complete_model(model_ref& md) const {
if (gparams::get_value("model.completion") != "true" || !md.get())
return;
model_ref md;
get_check_sat_result()->get_model(md);
SASSERT(md.get() != 0);
params_ref p;
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
p.set_uint("sort_store", true);
@ -1761,12 +1781,11 @@ void cmd_context::complete_model() {
\brief Check if the current model satisfies the quantifier free formulas.
*/
void cmd_context::validate_model() {
model_ref md;
if (!validate_model_enabled())
return;
if (!is_model_available())
if (!is_model_available(md))
return;
model_ref md;
get_check_sat_result()->get_model(md);
SASSERT(md.get() != 0);
params_ref p;
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
@ -1807,6 +1826,7 @@ void cmd_context::validate_model() {
continue;
}
TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
IF_VERBOSE(10, verbose_stream() << "model check failed on: " << mk_pp(a, m()) << "\n";);
invalid_model = true;
}
}
@ -1892,12 +1912,12 @@ void cmd_context::display_assertions() {
regular_stream() << ")" << std::endl;
}
bool cmd_context::is_model_available() const {
bool cmd_context::is_model_available(model_ref& md) const {
if (produce_models() &&
has_manager() &&
(cs_state() == css_sat || cs_state() == css_unknown)) {
model_ref md;
get_check_sat_result()->get_model(md);
complete_model(md);
return md.get() != nullptr;
}
return false;
@ -1925,7 +1945,7 @@ void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
}
void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const {
mk_smt2_format(f, get_pp_env(), params_ref(), r);
mk_smt2_format(f, get_pp_env(), params_ref(), r, "declare-fun");
}
void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {

27
src/cmd_context/cmd_context.h
View file

@ -23,20 +23,21 @@ Notes:
#include<sstream>
#include<vector>
#include "ast/ast.h"
#include "ast/ast_printer.h"
#include "cmd_context/pdecl.h"
#include "util/dictionary.h"
#include "solver/solver.h"
#include "ast/datatype_decl_plugin.h"
#include "util/stopwatch.h"
#include "util/cmd_context_types.h"
#include "util/event_handler.h"
#include "util/sexpr.h"
#include "util/dictionary.h"
#include "util/scoped_ptr_vector.h"
#include "ast/ast.h"
#include "ast/ast_printer.h"
#include "ast/datatype_decl_plugin.h"
#include "tactic/generic_model_converter.h"
#include "solver/solver.h"
#include "solver/progress_callback.h"
#include "cmd_context/pdecl.h"
#include "cmd_context/tactic_manager.h"
#include "cmd_context/check_logic.h"
#include "solver/progress_callback.h"
#include "util/scoped_ptr_vector.h"
#include "cmd_context/context_params.h"
@ -194,6 +195,7 @@ protected:
static std::ostringstream g_error_stream;
generic_model_converter_ref m_mc0;
ast_manager * m_manager;
bool m_own_manager;
bool m_manager_initialized;
@ -323,6 +325,7 @@ public:
void set_numeral_as_real(bool f) { m_numeral_as_real = f; }
void set_interactive_mode(bool flag) { m_interactive_mode = flag; }
void set_ignore_check(bool flag) { m_ignore_check = flag; }
bool ignore_check() const { return m_ignore_check; }
void set_exit_on_error(bool flag) { m_exit_on_error = flag; }
bool exit_on_error() const { return m_exit_on_error; }
bool interactive_mode() const { return m_interactive_mode; }
@ -363,7 +366,7 @@ public:
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const;
void complete_model();
void complete_model(model_ref& mdl) const;
void validate_model();
void display_model(model_ref& mdl);
@ -382,6 +385,8 @@ public:
void insert_user_tactic(symbol const & s, sexpr * d);
void insert_aux_pdecl(pdecl * p);
void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
void model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t);
void model_del(func_decl* f);
func_decl * find_func_decl(symbol const & s) const;
func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
unsigned arity, sort * const * domain, sort * range) const;
@ -441,7 +446,9 @@ public:
dictionary<macro_decls> const & get_macros() const { return m_macros; }
bool is_model_available() const;
model_converter* get_model_converter() { return m_mc0.get(); }
bool is_model_available(model_ref& md) const;
double get_seconds() const { return m_watch.get_seconds(); }

18
src/cmd_context/echo_tactic.cpp
View file

@ -27,18 +27,15 @@ class echo_tactic : public skip_tactic {
public:
echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {}
void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
#pragma omp critical (echo_tactic)
{
m_ctx.regular_stream() << m_msg;
if (m_newline)
m_ctx.regular_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result);
}
};
@ -61,11 +58,8 @@ public:
m_p->dec_ref();
}
void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
double val = (*m_p)(*(in.get())).get_value();
#pragma omp critical (probe_value_tactic)
{
@ -75,7 +69,7 @@ public:
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
skip_tactic::operator()(in, result);
}
};

8
src/cmd_context/eval_cmd.cpp
View file

@ -56,16 +56,14 @@ public:
}
void execute(cmd_context & ctx) override {
if (!ctx.is_model_available())
model_ref md;
if (!ctx.is_model_available(md))
throw cmd_exception("model is not available");
if (!m_target)
throw cmd_exception("no arguments passed to eval");
model_ref md;
unsigned index = m_params.get_uint("model_index", 0);
check_sat_result * last_result = ctx.get_check_sat_result();
SASSERT(last_result);
if (index == 0 || !ctx.get_opt()) {
last_result->get_model(md);
// already have model.
}
else {
ctx.get_opt()->get_box_model(md, index);

4
src/cmd_context/pdecl.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include "cmd_context/pdecl.h"
#include "ast/datatype_decl_plugin.h"
#include <sstream>
using namespace format_ns;
class psort_inst_cache {
@ -866,7 +867,6 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
}
psort * pdecl_manager::register_psort(psort * n) {
TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
psort * r = m_table.insert_if_not_there(n);
if (r != n) {
del_decl_core(n);
@ -946,7 +946,7 @@ void pdecl_manager::del_decl_core(pdecl * p) {
}
void pdecl_manager::del_decl(pdecl * p) {
TRACE("pdecl_manager", p->display(tout); tout << "\n";);
TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";);
if (p->is_psort()) {
psort * _p = static_cast<psort*>(p);
if (_p->is_sort_wrapper())

11
src/cmd_context/tactic_cmds.cpp
View file

@ -200,6 +200,8 @@ public:
if (!m_tactic) {
throw cmd_exception("check-sat-using needs a tactic argument");
}
if (ctx.ignore_check())
return;
params_ref p = ctx.params().merge_default_params(ps());
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
tref->set_logic(ctx.get_logic());
@ -324,9 +326,6 @@ public:
unsigned rlimit = p.get_uint("rlimit", ctx.params().rlimit());
goal_ref_buffer result_goals;
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
std::string reason_unknown;
bool failed = false;
@ -337,7 +336,7 @@ public:
scoped_timer timer(timeout, &eh);
cmd_context::scoped_watch sw(ctx);
try {
exec(t, g, result_goals, mc, pc, core);
exec(t, g, result_goals);
}
catch (tactic_exception & ex) {
ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
@ -396,8 +395,8 @@ public:
}
}
if (!failed && mc && p.get_bool("print_model_converter", false))
mc->display(ctx.regular_stream());
if (!failed && g->mc() && p.get_bool("print_model_converter", false))
g->mc()->display(ctx.regular_stream());
if (p.get_bool("print_statistics", false))
display_statistics(ctx, tref.get());

10
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -241,19 +241,13 @@ public:
m_stats.reset();
}
void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
try {
m_imp->process(*in);
m_imp->collect_statistics(m_stats);
result.reset();
result.push_back(in.get());
mc = nullptr;
pc = nullptr;
core = nullptr;
}
catch (z3_exception & ex) {
// convert all Z3 exceptions into tactic exceptions

6
src/model/model.cpp
View file

@ -42,10 +42,8 @@ model::~model() {
void model::copy_const_interps(model const & source) {
decl2expr::iterator it1 = source.m_interp.begin();
decl2expr::iterator end1 = source.m_interp.end();
for (; it1 != end1; ++it1) {
register_decl(it1->m_key, it1->m_value);
for (auto const& kv : source.m_interp) {
register_decl(kv.m_key, kv.m_value);
}
}

6
src/model/model_pp.cpp
View file

@ -31,10 +31,8 @@ static void display_uninterp_sorts(std::ostream & out, model_core const & md) {
sort * s = md.get_uninterpreted_sort(i);
out << "(define-sort " << mk_pp(s, m);
ptr_vector<expr> const & univ = md.get_universe(s);
ptr_vector<expr>::const_iterator it = univ.begin();
ptr_vector<expr>::const_iterator end = univ.end();
for (; it != end; ++it) {
out << " " << mk_ismt2_pp(*it, m);
for (expr* e : univ) {
out << " " << mk_ismt2_pp(e, m);
}
out << ")\n";
}

6
src/muz/base/dl_rule.cpp
View file

@ -41,7 +41,7 @@ Revision History:
#include "ast/rewriter/expr_replacer.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "ast/scoped_proof.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/ast_util.h"
@ -326,8 +326,8 @@ namespace datalog {
rules.set_output_predicate(qpred);
if (m_ctx.get_model_converter()) {
filter_model_converter* mc = alloc(filter_model_converter, m);
mc->insert(qpred);
generic_model_converter* mc = alloc(generic_model_converter, m, "dl_rule");
mc->hide(qpred);
m_ctx.add_model_converter(mc);
}

27
src/muz/base/dl_util.cpp
View file

@ -389,24 +389,32 @@ namespace datalog {
public:
skip_model_converter() {}
model_converter * translate(ast_translation & translator) override {
model_converter * translate(ast_translation & translator) override {
return alloc(skip_model_converter);
}
void operator()(model_ref&) override {}
void display(std::ostream & out) override { }
void get_units(obj_map<expr, bool>& units) override {}
};
model_converter* mk_skip_model_converter() { return alloc(skip_model_converter); }
class skip_proof_converter : public proof_converter {
void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) override {
proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
SASSERT(num_source == 1);
result = source[0];
return proof_ref(source[0], m);
}
proof_converter * translate(ast_translation & translator) override {
return alloc(skip_proof_converter);
}
void display(std::ostream & out) override { out << "(skip-proof-converter)\n"; }
};
proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); }
@ -517,10 +525,9 @@ namespace datalog {
}
void collect_and_transform(const unsigned_vector & src, const unsigned_vector & translation,
unsigned_vector & res) {
unsigned n = src.size();
for(unsigned i=0; i<n; i++) {
unsigned translated = translation[src[i]];
unsigned_vector & res) {
for (unsigned s : src) {
unsigned translated = translation[s];
if(translated!=UINT_MAX) {
res.push_back(translated);
}
@ -529,10 +536,8 @@ namespace datalog {
void transform_set(const unsigned_vector & map, const idx_set & src, idx_set & result) {
idx_set::iterator it = src.begin();
idx_set::iterator end = src.end();
for(; it!=end; ++it) {
result.insert(map[*it]);
for (unsigned s : src) {
result.insert(map[s]);
}
}

27
src/muz/fp/horn_tactic.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include "ast/rewriter/expr_replacer.h"
#include "muz/base/dl_rule_transformer.h"
#include "muz/transforms/dl_mk_slice.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "muz/transforms/dl_transforms.h"
#include "muz/base/fixedpoint_params.hpp"
#include "ast/ast_util.h"
@ -177,12 +177,8 @@ class horn_tactic : public tactic {
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
mc = nullptr; pc = nullptr; core = nullptr;
tactic_report report("horn", *g);
bool produce_proofs = g->proofs_enabled();
@ -229,18 +225,22 @@ class horn_tactic : public tactic {
}
queries.reset();
queries.push_back(q);
filter_model_converter* mc1 = alloc(filter_model_converter, m);
mc1->insert(to_app(q)->get_decl());
mc = mc1;
generic_model_converter* mc1 = alloc(generic_model_converter, m, "horn");
mc1->hide(q);
g->add(mc1);
}
SASSERT(queries.size() == 1);
q = queries[0].get();
proof_converter_ref pc = g->pc();
model_converter_ref mc;
if (m_is_simplify) {
simplify(q, g, result, mc, pc);
}
else {
verify(q, g, result, mc, pc);
}
g->set(pc.get());
g->set(mc.get());
}
void verify(expr* q,
@ -383,12 +383,9 @@ public:
m_imp->collect_param_descrs(r);
}
void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
(*m_imp)(in, result, mc, pc, core);
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
(*m_imp)(in, result);
}
void collect_statistics(statistics & st) const override {

7
src/muz/pdr/pdr_context.cpp
View file

@ -199,11 +199,8 @@ namespace pdr {
void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) {
goal_ref g(alloc(goal, m, false, false, false));
for (expr* e : v) g->assert_expr(e);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tac(g, result, mc, pc, core);
tac(g, result);
SASSERT(result.size() == 1);
goal* r = result[0];
v.reset();
@ -387,7 +384,7 @@ namespace pdr {
md->register_decl(m_head, fi);
}
model_converter_ref mc = ctx.get_model_converter();
apply(mc, md, 0);
apply(mc, md);
if (p_orig->get_arity() == 0) {
result = md->get_const_interp(p_orig);
}

5
src/muz/pdr/pdr_farkas_learner.cpp
View file

@ -520,12 +520,9 @@ namespace pdr {
g->assert_expr(lemmas[i].get());
}
expr_ref tmp(m);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tactic_ref simplifier = mk_arith_bounds_tactic(m);
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result);
lemmas.reset();
SASSERT(result.size() == 1);
goal* r = result[0];

2
src/muz/pdr/pdr_manager.cpp
View file

@ -107,7 +107,7 @@ namespace pdr {
}
}
TRACE("pdr", model_smt2_pp(tout, m, *md, 0););
apply(const_cast<model_converter_ref&>(m_mc), md, 0);
apply(const_cast<model_converter_ref&>(m_mc), md);
}
expr_ref inductive_property::to_expr() const {

9
src/muz/spacer/spacer_context.cpp
View file

@ -528,7 +528,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
md->register_decl(m_head, fi);
}
model_converter_ref mc = ctx.get_model_converter();
apply(mc, md, 0);
apply(mc, md);
if (p_orig->get_arity() == 0) {
result = md->get_const_interp(p_orig);
} else {
@ -1367,9 +1367,6 @@ void pred_transformer::frames::simplify_formulas ()
// normalize level
unsigned level = i < m_size ? i : infty_level ();
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
// simplify lemmas of the current level
@ -1395,7 +1392,7 @@ void pred_transformer::frames::simplify_formulas ()
}
// more than one lemma at current level. simplify.
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result);
SASSERT(result.size () == 1);
goal *r = result[0];
@ -2063,8 +2060,8 @@ bool context::validate()
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
vector<relation_info> rs;
model_converter_ref mc;
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
inductive_property ex(m, mc, rs);
ex.to_model(model);

23
src/muz/spacer/spacer_itp_solver.h
View file

@ -104,19 +104,13 @@ public:
/* solver interface */
solver* translate(ast_manager &m, params_ref const &p) override
{return m_solver.translate(m, p);}
void updt_params(params_ref const &p) override
{m_solver.updt_params(p);}
void collect_param_descrs(param_descrs &r) override
{m_solver.collect_param_descrs(r);}
void set_produce_models(bool f) override
{m_solver.set_produce_models(f);}
void assert_expr(expr *t) override
{m_solver.assert_expr(t);}
void assert_expr(expr *t, expr *a) override
{NOT_IMPLEMENTED_YET();}
solver* translate(ast_manager &m, params_ref const &p) override { return m_solver.translate(m, p);}
void updt_params(params_ref const &p) override { m_solver.updt_params(p);}
void collect_param_descrs(param_descrs &r) override { m_solver.collect_param_descrs(r);}
void set_produce_models(bool f) override { m_solver.set_produce_models(f);}
void assert_expr_core(expr *t) override { m_solver.assert_expr(t);}
void assert_expr_core2(expr *t, expr *a) override { NOT_IMPLEMENTED_YET();}
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
void push() override;
void pop(unsigned n) override;
@ -141,8 +135,9 @@ public:
void collect_statistics(statistics &st) const override ;
virtual void reset_statistics();
void get_unsat_core(ptr_vector<expr> &r) override;
void get_model(model_ref &m) override {m_solver.get_model(m);}
void get_model_core(model_ref &m) override {m_solver.get_model(m);}
proof *get_proof() override {return m_solver.get_proof();}
std::string reason_unknown() const override
{return m_solver.reason_unknown();}

5
src/muz/spacer/spacer_legacy_frames.cpp
View file

@ -46,11 +46,8 @@ void pred_transformer::legacy_frames::simplify_formulas(tactic& tac,
ast_manager &m = m_pt.get_ast_manager();
goal_ref g(alloc(goal, m, false, false, false));
for (unsigned j = 0; j < v.size(); ++j) { g->assert_expr(v[j].get()); }
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tac(g, result, mc, pc, core);
tac(g, result);
SASSERT(result.size() == 1);
goal* r = result[0];
v.reset();

2
src/muz/spacer/spacer_manager.cpp
View file

@ -113,7 +113,7 @@ void inductive_property::to_model(model_ref& md) const
}
}
TRACE("spacer", model_smt2_pp(tout, m, *md, 0););
apply(const_cast<model_converter_ref&>(m_mc), md, 0);
apply(const_cast<model_converter_ref&>(m_mc), md);
}
expr_ref inductive_property::to_expr() const

10
src/muz/spacer/spacer_util.cpp
View file

@ -929,12 +929,9 @@ void simplify_bounds_old(expr_ref_vector& cube) {
}
expr_ref tmp(m);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
tactic_ref simplifier = mk_arith_bounds_tactic(m);
(*simplifier)(g, result, mc, pc, core);
(*simplifier)(g, result);
SASSERT(result.size() == 1);
goal* r = result[0];
@ -955,15 +952,12 @@ void simplify_bounds_new (expr_ref_vector &cube) {
g->assert_expr(cube.get(i));
}
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref dep(m);
goal_ref_buffer goals;
tactic_ref prop_values = mk_propagate_values_tactic(m);
tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
(*t)(g, goals, mc, pc, dep);
(*t)(g, goals);
SASSERT(goals.size() == 1);
g = goals[0];

18
src/muz/spacer/spacer_virtual_solver.cpp
View file

@ -50,7 +50,7 @@ virtual_solver::virtual_solver(virtual_solver_factory &factory,
// -- change m_context, but will add m_pred to
// -- the private field solver_na2as::m_assumptions
if (m_virtual)
{ solver_na2as::assert_expr(m.mk_true(), m_pred); }
{ solver_na2as::assert_expr_core2(m.mk_true(), m_pred); }
}
virtual_solver::~virtual_solver()
@ -210,7 +210,7 @@ void virtual_solver::get_unsat_core(ptr_vector<expr> &r)
}
}
void virtual_solver::assert_expr(expr *e)
void virtual_solver::assert_expr_core(expr *e)
{
SASSERT(!m_pushed || get_scope_level() > 0);
if (m.is_true(e)) { return; }
@ -266,16 +266,10 @@ solver* virtual_solver::translate(ast_manager& m, params_ref const& p)
UNREACHABLE();
return nullptr;
}
void virtual_solver::updt_params(params_ref const &p)
{ m_factory.updt_params(p); }
void virtual_solver::collect_param_descrs(param_descrs &r)
{ m_factory.collect_param_descrs(r); }
void virtual_solver::set_produce_models(bool f)
{ m_factory.set_produce_models(f); }
bool virtual_solver::get_produce_models()
{return m_factory.get_produce_models(); }
smt_params &virtual_solver::fparams()
{return m_factory.fparams();}
void virtual_solver::updt_params(params_ref const &p) { m_factory.updt_params(p); }
void virtual_solver::collect_param_descrs(param_descrs &r) { m_factory.collect_param_descrs(r); }
void virtual_solver::set_produce_models(bool f) { m_factory.set_produce_models(f); }
smt_params &virtual_solver::fparams() {return m_factory.fparams();}
void virtual_solver::to_smt2_benchmark(std::ostream &out,
smt::kernel &context,

14
src/muz/spacer/spacer_virtual_solver.h
View file

@ -77,10 +77,11 @@ public:
return solver_na2as::get_assumption(idx);
}
void get_unsat_core(ptr_vector<expr> &r) override;
void assert_expr(expr *e) override;
void assert_expr_core(expr *e) override;
void collect_statistics(statistics &st) const override {}
void get_model(model_ref &m) override {m_context.get_model(m);}
void get_model_core(model_ref &m) override {m_context.get_model(m);}
proof* get_proof() override;
std::string reason_unknown() const override
{return m_context.last_failure_as_string();}
@ -89,11 +90,10 @@ public:
ast_manager& get_manager() const override {return m;}
void get_labels(svector<symbol> &r) override;
void set_produce_models(bool f) override;
virtual bool get_produce_models();
virtual smt_params &fparams();
virtual void reset();
void set_progress_callback(progress_callback *callback) override
{UNREACHABLE();}
smt_params &fparams();
void reset();
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
void set_progress_callback(progress_callback *callback) override {UNREACHABLE();}
solver *translate(ast_manager &m, params_ref const &p) override;

2
src/muz/tab/tab_context.cpp
View file

@ -1602,7 +1602,7 @@ namespace datalog {
pc.invert();
prs.push_back(m.mk_asserted(root));
pc(m, 1, prs.c_ptr(), pr);
pr = pc(m, 1, prs.c_ptr());
return pr;
}

10
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -22,7 +22,7 @@ Revision History:
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "tactic/filter_model_converter.h"
#include "tactic/generic_model_converter.h"
#include "muz/transforms/dl_mk_interp_tail_simplifier.h"
#include "muz/base/fixedpoint_params.hpp"
#include "ast/scoped_proof.h"
@ -63,6 +63,10 @@ namespace datalog {
return alloc(bit_blast_model_converter, m);
}
void get_units(obj_map<expr, bool>& units) override {}
void display(std::ostream& out) override { out << "(bit-blast-model-converter)\n"; }
void operator()(model_ref & model) override {
for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
func_decl* p = m_new_funcs[i].get();
@ -297,12 +301,12 @@ namespace datalog {
}
if (m_context.get_model_converter()) {
filter_model_converter* fmc = alloc(filter_model_converter, m);
generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast");
bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m);
func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs();
func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs();
for (unsigned i = 0; i < old_funcs.size(); ++i) {
fmc->insert(new_funcs[i]);
fmc->hide(new_funcs[i]);
bvmc->insert(old_funcs[i], new_funcs[i]);
}
m_context.add_model_converter(concat(bvmc, fmc));

13
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -21,6 +21,7 @@ Author:
#include "muz/dataflow/dataflow.h"
#include "muz/dataflow/reachability.h"
#include "ast/ast_pp.h"
#include "tactic/generic_model_converter.h"
#include "ast/ast_util.h"
#include "tactic/extension_model_converter.h"
@ -101,14 +102,14 @@ namespace datalog {
// set to false each unreached predicate
if (res && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
for (auto const& kv : engine) {
if (!kv.m_value.is_reachable()) {
mc0->insert(kv.m_key, m.mk_false());
mc0->add(kv.m_key, m.mk_false());
}
}
for (func_decl* f : unreachable) {
mc0->insert(f, m.mk_false());
mc0->add(f, m.mk_false());
}
m_context.add_model_converter(mc0);
}
@ -137,7 +138,7 @@ namespace datalog {
res = nullptr;
}
if (res && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
for (func_decl* f : pruned_preds) {
const rule_vector& rules = source.get_predicate_rules(f);
expr_ref_vector fmls(m);
@ -152,7 +153,9 @@ namespace datalog {
}
fmls.push_back(mk_and(conj));
}
mc0->insert(f, mk_or(fmls));
expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->add(f, fml);
}
m_context.add_model_converter(mc0);
}

6
src/muz/transforms/dl_mk_karr_invariants.cpp
View file

@ -120,6 +120,8 @@ namespace datalog {
}
}
void get_units(obj_map<expr, bool>& units) override {}
void operator()(model_ref & mr) override {
for (unsigned i = 0; i < m_funcs.size(); ++i) {
func_decl* p = m_funcs[i].get();
@ -150,6 +152,10 @@ namespace datalog {
return mc;
}
void display(std::ostream& out) override {
out << "(add-invariant-model-converter)\n";
}
private:
void mk_body(matrix const& M, expr_ref& body) {
expr_ref_vector conj(m);

10
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -53,6 +53,10 @@ namespace datalog {
return alloc(qa_model_converter, m);
}
void display(std::ostream& out) override { display_add(out, m); }
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector<bool> const& bound) {
m_old_funcs.push_back(old_p);
m_new_funcs.push_back(new_p);
@ -81,7 +85,11 @@ namespace datalog {
SASSERT(body);
}
else {
body = m.mk_false();
expr_ref_vector args(m);
for (unsigned i = 0; i < p->get_arity(); ++i) {
args.push_back(m.mk_var(i, p->get_domain(i)));
}
body = m.mk_app(p, args.size(), args.c_ptr());
}
// Create quantifier wrapper around body.

13
src/muz/transforms/dl_mk_scale.cpp
View file

@ -38,13 +38,13 @@ namespace datalog {
m_new2old.insert(new_f, old_f);
}
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void operator()(model_ref& md) override {
model_ref old_model = alloc(model, m);
obj_map<func_decl, func_decl*>::iterator it = m_new2old.begin();
obj_map<func_decl, func_decl*>::iterator end = m_new2old.end();
for (; it != end; ++it) {
func_decl* old_p = it->m_value;
func_decl* new_p = it->m_key;
for (auto const& kv : m_new2old) {
func_decl* old_p = kv.m_value;
func_decl* new_p = kv.m_key;
func_interp* old_fi = alloc(func_interp, m, old_p->get_arity());
if (new_p->get_arity() == 0) {
@ -99,6 +99,9 @@ namespace datalog {
UNREACHABLE();
return nullptr;
}
void display(std::ostream& out) override { out << "(scale-model-converter)\n"; }
};

11
src/muz/transforms/dl_mk_slice.cpp
View file

@ -271,11 +271,12 @@ namespace datalog {
m_renaming.insert(orig_rule, unsigned_vector(sz, renaming));
}
void operator()(ast_manager& m, unsigned num_source, proof * const * source, proof_ref & result) override {
proof_ref operator()(ast_manager& m, unsigned num_source, proof * const * source) override {
SASSERT(num_source == 1);
result = source[0];
proof_ref result(source[0], m);
init_form2rule();
translate_proof(result);
return result;
}
proof_converter * translate(ast_translation & translator) override {
@ -283,6 +284,8 @@ namespace datalog {
// this would require implementing translation for the dl_context.
return nullptr;
}
void display(std::ostream& out) override { out << "(slice-proof-converter)\n"; }
};
class mk_slice::slice_model_converter : public model_converter {
@ -305,6 +308,8 @@ namespace datalog {
m_sliceable.insert(f, bv);
}
void get_units(obj_map<expr, bool>& units) override {}
void operator()(model_ref & md) override {
if (m_slice2old.empty()) {
return;
@ -396,6 +401,8 @@ namespace datalog {
return nullptr;
}
void display(std::ostream& out) override { out << "(slice-model-converter)\n"; }
};
mk_slice::mk_slice(context & ctx):

6
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include "ast/rewriter/rewriter_def.h"
#include "muz/transforms/dl_mk_subsumption_checker.h"
#include "muz/base/fixedpoint_params.hpp"
#include "tactic/extension_model_converter.h"
#include "tactic/generic_model_converter.h"
namespace datalog {
@ -241,9 +241,9 @@ namespace datalog {
}
tgt.inherit_predicates(orig);
if (!m_total_relations.empty() && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl-subsumption");
for (func_decl* p : m_total_relations) {
mc0->insert(p, m.mk_true());
mc0->add(p, m.mk_true());
}
m_context.add_model_converter(mc0);
}

21
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -129,12 +129,8 @@ class nlsat_tactic : public tactic {
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
goal_ref_buffer & result) {
SASSERT(g->is_well_sorted());
mc = nullptr; pc = nullptr; core = nullptr;
tactic_report report("nlsat", *g);
if (g->is_decided()) {
@ -166,9 +162,11 @@ class nlsat_tactic : public tactic {
if (!contains_unsupported(b2a, x2t)) {
// If mk_model is false it means that the model produced by nlsat
// assigns noninteger values to integer variables
model_converter_ref mc;
if (mk_model(*g.get(), b2a, x2t, mc)) {
// result goal is trivially SAT
g->reset();
g->add(mc.get());
}
}
}
@ -177,8 +175,8 @@ class nlsat_tactic : public tactic {
if (g->unsat_core_enabled()) {
vector<nlsat::assumption, false> assumptions;
m_solver.get_core(assumptions);
for (unsigned i = 0; i < assumptions.size(); ++i) {
expr_dependency* d = static_cast<expr_dependency*>(assumptions[i]);
for (nlsat::assumption a : assumptions) {
expr_dependency* d = static_cast<expr_dependency*>(a);
lcore = m.mk_join(lcore, d);
}
}
@ -232,15 +230,12 @@ public:
algebraic_numbers::manager::collect_param_descrs(r);
}
void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
try {
imp local_imp(in->m(), m_params);
scoped_set_imp setter(*this, local_imp);
local_imp(in, result, mc, pc, core);
local_imp(in, result);
}
catch (z3_error & ex) {
throw ex;

42
src/opt/maxres.cpp
View file

@ -52,17 +52,18 @@ Notes:
--*/
#include "solver/solver.h"
#include "opt/maxsmt.h"
#include "opt/maxres.h"
#include "ast/ast_pp.h"
#include "ast/pb_decl_plugin.h"
#include "ast/ast_util.h"
#include "model/model_smt2_pp.h"
#include "solver/solver.h"
#include "solver/mus.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "opt/opt_context.h"
#include "ast/pb_decl_plugin.h"
#include "opt/opt_params.hpp"
#include "ast/ast_util.h"
#include "smt/smt_solver.h"
#include "opt/opt_context.h"
#include "opt/opt_params.hpp"
#include "opt/maxsmt.h"
#include "opt/maxres.h"
using namespace opt;
@ -282,11 +283,13 @@ public:
m_last_index = 0;
bool first = index > 0;
SASSERT(index < asms.size() || asms.empty());
IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
while (index < asms.size() && is_sat == l_true) {
while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
index = next_index(asms, index);
}
first = false;
IF_VERBOSE(3, verbose_stream() << "hill climb " << index << "\n";);
// IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
m_last_index = index;
is_sat = check_sat(index, asms.c_ptr());
@ -323,6 +326,7 @@ public:
m_found_feasible_optimum = true;
}
virtual lbool operator()() {
m_defs.reset();
switch(m_st) {
@ -363,6 +367,7 @@ public:
m_lower = m_upper;
return l_true;
}
split_core(core);
cores.push_back(core);
if (core.size() >= m_max_core_size) {
break;
@ -489,7 +494,7 @@ public:
expr_ref fml(m);
remove_core(core);
SASSERT(!core.empty());
rational w = split_core(core);
rational w = core_weight(core);
TRACE("opt", display_vec(tout << "minimized core: ", core););
IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
max_resolve(core, w);
@ -555,19 +560,24 @@ public:
return m_asm2weight.find(e);
}
rational split_core(exprs const& core) {
rational core_weight(exprs const& core) {
if (core.empty()) return rational(0);
// find the minimal weight:
rational w = get_weight(core[0]);
for (unsigned i = 1; i < core.size(); ++i) {
w = std::min(w, get_weight(core[i]));
}
return w;
}
rational split_core(exprs const& core) {
rational w = core_weight(core);
// add fresh soft clauses for weights that are above w.
for (unsigned i = 0; i < core.size(); ++i) {
rational w2 = get_weight(core[i]);
for (expr* e : core) {
rational w2 = get_weight(e);
if (w2 > w) {
rational w3 = w2 - w;
new_assumption(core[i], w3);
new_assumption(e, w3);
}
}
return w;
@ -726,11 +736,13 @@ public:
m_model = mdl;
m_c.model_updated(mdl);
TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0););
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);
}
DEBUG_CODE(verify_assignment(););
// DEBUG_CODE(verify_assignment(););
m_upper = upper;
trace();
@ -769,6 +781,9 @@ public:
bool is_true(expr_ref_vector const& es) {
unsigned i = 0;
for (; i < es.size() && is_true(es[i]); ++i) { }
CTRACE("opt", i < es.size(), tout << mk_pp(es[i], m) << "\n";
model_smt2_pp(tout, m, *m_model, 0);
);
return i == es.size();
}
@ -865,6 +880,7 @@ public:
if (is_sat == l_false) {
IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
}
IF_VERBOSE(1, verbose_stream() << "verified\n";);
}
};

26
src/opt/maxsmt.cpp
View file

@ -105,7 +105,7 @@ namespace opt {
app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
app* result = m.mk_fresh_const(name, m.mk_bool_sort());
m_c.fm().insert(result->get_decl());
m_c.fm().hide(result);
return result;
}
@ -266,7 +266,7 @@ namespace opt {
}
}
IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << "\n";
IF_VERBOSE(5, verbose_stream() << "is-sat: " << is_sat << "\n";
if (is_sat == l_true) {
verbose_stream() << "Satisfying soft constraints\n";
display_answer(verbose_stream());
@ -353,12 +353,26 @@ namespace opt {
m_upper += w;
}
struct cmp_first {
bool operator()(std::pair<unsigned, rational> const& x, std::pair<unsigned, rational> const& y) const {
return x.first < y.first;
}
};
void maxsmt::display_answer(std::ostream& out) const {
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
expr* e = m_soft_constraints[i];
vector<std::pair<unsigned, rational>> sorted_weights;
unsigned n = m_weights.size();
for (unsigned i = 0; i < n; ++i) {
sorted_weights.push_back(std::make_pair(i, m_weights[i]));
}
std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first());
sorted_weights.reverse();
for (unsigned i = 0; i < n; ++i) {
unsigned idx = sorted_weights[i].first;
expr* e = m_soft_constraints[idx];
bool is_not = m.is_not(e, e);
out << m_weights[i] << ": " << mk_pp(e, m)
<< ((is_not != get_assignment(i))?" |-> true ":" |-> false ")
out << m_weights[idx] << ": " << mk_pp(e, m)
<< ((is_not != get_assignment(idx))?" |-> true ":" |-> false ")
<< "\n";
}

Some files were not shown because too many files have changed in this diff Show more