3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00

merge with Z3Prover/z3/master

This commit is contained in:
nilsbecker 2018-06-06 08:09:57 +02:00
commit f7b50ef796
452 changed files with 29240 additions and 34285 deletions

View file

@ -33,7 +33,7 @@ endif()
# Project version
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 7)
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}")
@ -218,12 +218,17 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
################################################################################
# C++ language version
################################################################################
# FIXME: Use CMake's own mechanism for selecting language version
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
z3_add_cxx_flag("-std=c++11" REQUIRED)
else()
message(AUTHOR_WARNING "Not setting C++ language version for compiler")
endif()
if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
# FIXME: Drop this when we upgrade to newer CMake versions.
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
z3_add_cxx_flag("-std=c++11" REQUIRED)
else()
message(AUTHOR_WARNING "Not setting C++ language version for compiler")
endif()
else ()
set(CMAKE_CXX_STANDARD 11)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
endif ()
################################################################################
# Platform detection

View file

@ -1,5 +1,55 @@
RELEASE NOTES
Version 4.8.0
=============
- New requirements:
- 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.
- New features
- 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.
- The SAT solver by default handle cardinality and PB constraints using a custom plugin
that operates directly on cardinality and PB constraints.
- 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.
Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
as lemmas (redundant) and are garbage collected if their glue level is high.
- Removed features:
- interpolation API
- duality engine for constrained Horn clauses.
- long deprecated API functions have been removed from z3_api.h
Version 4.7.1
=============
- New requirements:
- uses stdbool and stdint as part of z3.
- New features:
- none
- Removed features:
- none
- Notes:
This is a minor release prior to a set of planned major updates.
It uses minor version 7 to indicate that the use of stdbool and
stdint are breaking changes to consumers of the C-based API.
Version 4.6.0
=============

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

View file

@ -272,7 +272,6 @@ try:
cleanup_API(doc_path('../src/api/z3_rcf.h'), temp_path('z3_rcf.h'))
cleanup_API(doc_path('../src/api/z3_fixedpoint.h'), temp_path('z3_fixedpoint.h'))
cleanup_API(doc_path('../src/api/z3_optimization.h'), temp_path('z3_optimization.h'))
cleanup_API(doc_path('../src/api/z3_interp.h'), temp_path('z3_interp.h'))
cleanup_API(doc_path('../src/api/z3_fpa.h'), temp_path('z3_fpa.h'))
print("Removed annotations from z3_api.h.")

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

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);
@ -2286,46 +2290,6 @@ void unsat_core_and_proof_example() {
Z3_del_context(ctx);
}
void interpolation_example() {
Z3_context ctx = mk_context();
Z3_ast pa = mk_bool_var(ctx, "PredA");
Z3_ast pb = mk_bool_var(ctx, "PredB");
Z3_ast pc = mk_bool_var(ctx, "PredC");
Z3_ast args1[2] = {pa,pb}, args2[2] = {Z3_mk_not(ctx,pb),pc};
Z3_ast args3[2] = {Z3_mk_interpolant(ctx,Z3_mk_and(ctx,2,args1)),Z3_mk_and(ctx,2,args2)};
Z3_ast f = Z3_mk_and(ctx,2,args3);
Z3_ast_vector interpolant = 0;
Z3_model m = 0;
Z3_lbool result = Z3_L_UNDEF;
printf("\ninterpolation_example\n");
LOG_MSG("interpolation_example");
result = Z3_compute_interpolant(ctx,f,0,&interpolant,&m);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
printf("interpolant: %s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, interpolant, 0)));
printf("\n");
break;
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
case Z3_L_TRUE:
printf("sat\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
}
/* delete logical context */
if (m) Z3_model_dec_ref(ctx, m);
Z3_del_context(ctx);
}
#define MAX_RETRACTABLE_ASSERTIONS 1024
@ -2576,13 +2540,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);
}
@ -3008,7 +2974,6 @@ int main() {
binary_tree_example();
enum_example();
unsat_core_and_proof_example();
interpolation_example();
incremental_example1();
reference_counter_example();
smt2parser_example();

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

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

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

View file

@ -0,0 +1,36 @@
from z3 import *
from multiprocessing.pool import ThreadPool
from copy import deepcopy
pool = ThreadPool(8)
x = Int('x')
assert x.ctx == main_ctx()
def calculate(x, n, ctx):
""" Do a simple computation with a context"""
assert x.ctx == ctx
assert x.ctx != main_ctx()
# Parallel creation of z3 object
condition = And(x < 2, x > n, ctx)
# Parallel solving
solver = Solver(ctx=ctx)
solver.add(condition)
solver.check()
for i in range(100):
# Create new context for the computation
# Note that we need to do this sequentially, as parallel access to the current context or its objects
# will result in a segfault
i_context = Context()
x_i = deepcopy(x).translate(i_context)
# Kick off parallel computation
pool.apply_async(calculate, [x_i, i, i_context])
pool.close()
pool.join()

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

View file

@ -9,12 +9,12 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 7, 0, 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')
@ -32,16 +32,15 @@ def init_project_def():
add_lib('grobner', ['ast'], 'math/grobner')
add_lib('euclid', ['util'], 'math/euclid')
add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter'], 'tactic/core')
add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic')
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
add_lib('solver', ['model', 'tactic', 'proofs'])
add_lib('sat_tactic', ['tactic', 'sat', 'solver'], 'sat/tactic')
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
add_lib('solver', ['model', 'tactic', 'proofs'])
add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
add_lib('interp', ['solver'])
add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
add_lib('cmd_context', ['solver', 'rewriter'])
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
@ -56,7 +55,6 @@ def init_project_def():
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat','nlsat','tactic','nlsat_tactic'], 'qe')
add_lib('duality', ['smt', 'interp', 'qe'])
add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
add_lib('dataflow', ['muz'], 'muz/dataflow')
add_lib('transforms', ['muz', 'hilbert', 'dataflow'], 'muz/transforms')
@ -67,17 +65,15 @@ def init_project_def():
add_lib('tab', ['muz', 'transforms'], 'muz/tab')
add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
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('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'ddnf', 'spacer'], 'muz/fp')
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')
API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h', 'z3_spacer.h']
add_lib('api', ['portfolio', 'realclosure', 'interp', 'opt'],
API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
add_lib('api', ['portfolio', 'realclosure', 'opt'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)

View file

@ -1932,8 +1932,14 @@ class MLComponent(Component):
OCAML_FLAGS = ''
if DEBUG_MODE:
OCAML_FLAGS += '-g'
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
if OCAMLFIND:
# Load Big_int, which is no longer part of the standard library, via the num package: https://github.com/ocaml/num
OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package num' + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package num' + ' ' + OCAML_FLAGS
else:
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
src_dir = self.to_src_dir
mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
@ -2505,6 +2511,7 @@ def mk_config():
LDFLAGS = '%s -lrt' % LDFLAGS
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
elif sysname == 'FreeBSD':
CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS
OS_DEFINES = '-D_FREEBSD_'
@ -2803,6 +2810,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)

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

View file

@ -12,7 +12,6 @@ set(Z3_API_HEADER_FILES_TO_SCAN
z3_rcf.h
z3_fixedpoint.h
z3_optimization.h
z3_interp.h
z3_fpa.h
z3_spacer.h
)
@ -36,10 +35,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,14 +55,13 @@ 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)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
@ -79,7 +77,6 @@ add_subdirectory(tactic/bv)
add_subdirectory(smt/tactic)
add_subdirectory(tactic/sls)
add_subdirectory(qe)
add_subdirectory(duality)
add_subdirectory(muz/base)
add_subdirectory(muz/dataflow)
add_subdirectory(muz/transforms)
@ -89,10 +86,8 @@ add_subdirectory(muz/clp)
add_subdirectory(muz/tab)
add_subdirectory(muz/bmc)
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)
@ -160,7 +155,6 @@ set (libz3_public_headers
z3_fpa.h
z3.h
c++/z3++.h
z3_interp.h
z3_macros.h
z3_optimization.h
z3_polynomial.h

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

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

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;

View file

@ -48,7 +48,6 @@ z3_add_component(api
api_datatype.cpp
api_fpa.cpp
api_goal.cpp
api_interp.cpp
api_log.cpp
api_model.cpp
api_numeral.cpp
@ -67,7 +66,6 @@ z3_add_component(api
z3_replayer.cpp
${full_path_generated_files}
COMPONENT_DEPENDENCIES
interp
opt
portfolio
realclosure

View file

@ -195,7 +195,6 @@ extern "C" {
MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP);
MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP);
MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP);
MK_UNARY(Z3_mk_interpolant, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP);
Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));
@ -900,7 +899,6 @@ extern "C" {
case OP_NOT: return Z3_OP_NOT;
case OP_IMPLIES: return Z3_OP_IMPLIES;
case OP_OEQ: return Z3_OP_OEQ;
case OP_INTERP: return Z3_OP_INTERP;
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;

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

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

View file

@ -1,728 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
api_interp.cpp
Abstract:
API for interpolation
Author:
Ken McMillan
Revision History:
--*/
#include<sstream>
#include<vector>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_tactic.h"
#include "api/api_solver.h"
#include "api/api_model.h"
#include "api/api_stats.h"
#include "api/api_ast_vector.h"
#include "solver/tactic2solver.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "tactic/portfolio/smt_strategic_solver.h"
#include "smt/smt_solver.h"
#include "smt/smt_implied_equalities.h"
#include "interp/iz3interp.h"
#include "interp/iz3profiling.h"
#include "interp/iz3hash.h"
#include "interp/iz3pp.h"
#include "interp/iz3checker.h"
#include "ast/scoped_proof.h"
using namespace stl_ext;
// WARNING: don't make a hash_map with this if the range type
// has a destructor: you'll get an address dependency!!!
namespace stl_ext {
template <>
class hash < Z3_ast > {
public:
size_t operator()(const Z3_ast p) const {
return (size_t)p;
}
};
}
typedef interpolation_options_struct *Z3_interpolation_options;
extern "C" {
Z3_context Z3_mk_interpolation_context(Z3_config cfg){
if (!cfg) cfg = Z3_mk_config();
Z3_set_param_value(cfg, "PROOF", "true");
Z3_set_param_value(cfg, "MODEL", "true");
// Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false");
// Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
Z3_context ctx = Z3_mk_context(cfg);
return ctx;
}
void Z3_interpolate_proof(Z3_context ctx,
Z3_ast proof,
int num,
Z3_ast *cnsts,
unsigned *parents,
Z3_params options,
Z3_ast *interps,
int num_theory,
Z3_ast *theory)
{
if (num > 1){ // if we have interpolants to compute
ptr_vector<ast> pre_cnsts_vec(num); // get constraints in a vector
for (int i = 0; i < num; i++){
ast *a = to_ast(cnsts[i]);
pre_cnsts_vec[i] = a;
}
::vector<int> pre_parents_vec; // get parents in a vector
if (parents){
pre_parents_vec.resize(num);
for (int i = 0; i < num; i++)
pre_parents_vec[i] = parents[i];
}
ptr_vector<ast> theory_vec; // get background theory in a vector
if (theory){
theory_vec.resize(num_theory);
for (int i = 0; i < num_theory; i++)
theory_vec[i] = to_ast(theory[i]);
}
ptr_vector<ast> interpolants(num - 1); // make space for result
ast_manager &_m = mk_c(ctx)->m();
iz3interpolate(_m,
to_ast(proof),
pre_cnsts_vec,
pre_parents_vec,
interpolants,
theory_vec,
nullptr); // ignore params for now FIXME
// copy result back
for (unsigned i = 0; i < interpolants.size(); i++){
mk_c(ctx)->save_ast_trail(interpolants[i]);
interps[i] = of_ast(interpolants[i]);
_m.dec_ref(interpolants[i]);
}
}
}
static std::ostringstream itp_err;
int Z3_check_interpolant(Z3_context ctx,
unsigned num,
Z3_ast *cnsts,
unsigned *parents,
Z3_ast *itp,
Z3_string *error,
unsigned num_theory,
Z3_ast *theory){
ast_manager &_m = mk_c(ctx)->m();
itp_err.clear();
// need a solver -- make one here, but how?
params_ref p = params_ref::get_empty(); //FIXME
scoped_ptr<solver_factory> sf(mk_smt_solver_factory());
scoped_ptr<solver> sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA")));
ptr_vector<ast> cnsts_vec(num); // get constraints in a vector
for (unsigned i = 0; i < num; i++){
ast *a = to_ast(cnsts[i]);
cnsts_vec[i] = a;
}
ptr_vector<ast> itp_vec(num); // get interpolants in a vector
for (unsigned i = 0; i < num - 1; i++){
ast *a = to_ast(itp[i]);
itp_vec[i] = a;
}
::vector<int> parents_vec; // get parents in a vector
if (parents){
parents_vec.resize(num);
for (unsigned i = 0; i < num; i++)
parents_vec[i] = parents[i];
}
ptr_vector<ast> theory_vec; // get background theory in a vector
if (theory){
theory_vec.resize(num_theory);
for (unsigned i = 0; i < num_theory; i++)
theory_vec[i] = to_ast(theory[i]);
}
bool res = iz3check(_m,
sp.get(),
itp_err,
cnsts_vec,
parents_vec,
itp_vec,
theory_vec);
*error = res ? nullptr : itp_err.str().c_str();
return res;
}
static std::string Z3_profile_string;
Z3_string Z3_interpolation_profile(Z3_context ctx){
std::ostringstream f;
profiling::print(f);
Z3_profile_string = f.str();
return Z3_profile_string.c_str();
}
Z3_interpolation_options
Z3_mk_interpolation_options(){
return (Z3_interpolation_options) new interpolation_options_struct;
}
void
Z3_del_interpolation_options(Z3_interpolation_options opts){
delete opts;
}
void
Z3_set_interpolation_option(Z3_interpolation_options opts,
Z3_string name,
Z3_string value){
opts->map[name] = value;
}
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p){
Z3_TRY;
LOG_Z3_get_interpolant(c, pf, pat, p);
RESET_ERROR_CODE();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
ast *_pf = to_ast(pf);
ast *_pat = to_ast(pat);
ptr_vector<ast> interp;
ptr_vector<ast> cnsts; // to throw away
ast_manager &_m = mk_c(c)->m();
iz3interpolate(_m,
_pf,
cnsts,
_pat,
interp,
(interpolation_options_struct *)nullptr // ignore params for now
);
// copy result back
for (unsigned i = 0; i < interp.size(); i++){
v->m_ast_vector.push_back(interp[i]);
_m.dec_ref(interp[i]);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(nullptr);
}
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *out_interp, Z3_model *model){
Z3_TRY;
LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
RESET_ERROR_CODE();
// params_ref &_p = to_params(p)->m_params;
params_ref _p;
_p.set_bool("proof", true); // this is currently useless
scoped_proof_mode spm(mk_c(c)->m(), PGM_ENABLED);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
m_solver.get()->updt_params(_p); // why do we have to do this?
// some boilerplate stolen from Z3_solver_check
unsigned timeout = p?to_params(p)->m_params.get_uint("timeout", mk_c(c)->get_timeout()):UINT_MAX;
unsigned rlimit = p?to_params(p)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()):0;
bool use_ctrl_c = p?to_params(p)->m_params.get_bool("ctrl_c", false): false;
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
ast *_pat = to_ast(pat);
ptr_vector<ast> interp;
ptr_vector<ast> cnsts; // to throw away
ast_manager &_m = mk_c(c)->m();
model_ref m;
lbool _status;
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
_status = iz3interpolate(_m,
*(m_solver.get()),
_pat,
cnsts,
interp,
m,
nullptr // ignore params for now
);
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
RETURN_Z3_compute_interpolant Z3_L_UNDEF;
}
}
for (unsigned i = 0; i < cnsts.size(); i++)
_m.dec_ref(cnsts[i]);
Z3_lbool status = of_lbool(_status);
Z3_ast_vector_ref *v = nullptr;
*model = nullptr;
if (_status == l_false){
// copy result back
v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
for (unsigned i = 0; i < interp.size(); i++){
v->m_ast_vector.push_back(interp[i]);
_m.dec_ref(interp[i]);
}
}
else {
model_ref mr;
m_solver.get()->get_model(mr);
if(mr.get()){
Z3_model_ref *tmp_val = alloc(Z3_model_ref, *mk_c(c));
tmp_val->m_model = mr.get();
mk_c(c)->save_object(tmp_val);
*model = of_model(tmp_val);
}
}
*out_interp = of_ast_vector(v);
RETURN_Z3_compute_interpolant status;
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
};
static void tokenize(const std::string &str, std::vector<std::string> &tokens){
for (unsigned i = 0; i < str.size();){
if (str[i] == ' '){ i++; continue; }
unsigned beg = i;
while (i < str.size() && str[i] != ' ')i++;
if (i > beg)
tokens.push_back(str.substr(beg, i - beg));
}
}
static void get_file_params(const char *filename, hash_map<std::string, std::string> &params){
std::ifstream f(filename);
if (f){
std::string first_line;
std::getline(f, first_line);
// std::cout << "first line: '" << first_line << "'" << std::endl;
if (first_line.size() >= 2 && first_line[0] == ';' && first_line[1] == '!'){
std::vector<std::string> tokens;
tokenize(first_line.substr(2, first_line.size() - 2), tokens);
for (unsigned i = 0; i < tokens.size(); i++){
std::string &tok = tokens[i];
size_t eqpos = tok.find('=');
if (eqpos != std::string::npos){
std::string left = tok.substr(0, eqpos);
std::string right = tok.substr(eqpos + 1, tok.size() - eqpos - 1);
params[left] = right;
}
}
}
f.close();
}
}
extern "C" {
#if 0
static void iZ3_write_seq(Z3_context ctx, int num, Z3_ast *cnsts, const char *filename, int num_theory, Z3_ast *theory){
int num_fmlas = num+num_theory;
std::vector<Z3_ast> fmlas(num_fmlas);
if(num_theory)
std::copy(theory,theory+num_theory,fmlas.begin());
for(int i = 0; i < num_theory; i++)
fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]);
std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory);
Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]);
std::ofstream f(filename);
if(num_theory)
f << ";! THEORY=" << num_theory << "\n";
f << smt;
f.close();
}
void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, unsigned *parents, const char *filename, int num_theory, Z3_ast *theory){
if(!parents){
iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory);
return;
}
std::vector<Z3_ast> tcnsts(num);
hash_map<int,Z3_ast> syms;
for(int j = 0; j < num - 1; j++){
std::ostringstream oss;
oss << "$P" << j;
std::string name = oss.str();
Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str());
Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx));
syms[j] = symbol;
tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol);
}
tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx));
for(int j = num-2; j >= 0; j--){
int parent = parents[j];
// assert(parent >= 0 && parent < num);
tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]);
}
iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory);
}
#else
static Z3_ast and_vec(Z3_context ctx, svector<Z3_ast> &c){
return (c.size() > 1) ? Z3_mk_and(ctx, c.size(), &c[0]) : c[0];
}
static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, unsigned *parents){
Z3_ast res;
if (!parents){
res = Z3_mk_interpolant(ctx, cnsts[0]);
for (int i = 1; i < num - 1; i++){
Z3_ast bar[2] = { res, cnsts[i] };
res = Z3_mk_interpolant(ctx, Z3_mk_and(ctx, 2, bar));
}
if (num > 1){
Z3_ast bar[2] = { res, cnsts[num - 1] };
res = Z3_mk_and(ctx, 2, bar);
}
}
else {
std::vector<svector<Z3_ast> > chs(num);
for (int i = 0; i < num - 1; i++){
svector<Z3_ast> &c = chs[i];
c.push_back(cnsts[i]);
Z3_ast foo = Z3_mk_interpolant(ctx, and_vec(ctx, c));
chs[parents[i]].push_back(foo);
}
{
svector<Z3_ast> &c = chs[num - 1];
c.push_back(cnsts[num - 1]);
res = and_vec(ctx, c);
}
}
Z3_inc_ref(ctx, res);
return res;
}
void Z3_write_interpolation_problem(Z3_context ctx, unsigned num, Z3_ast *cnsts, unsigned *parents, const char *filename, unsigned num_theory, Z3_ast *theory){
std::ofstream f(filename);
if (num > 0){
#if 0
// Suggested shorthand:
ptr_vector<expr> cnsts_vec;
cnsts_vec.append(num, to_exprs(cnsts));
cnsts_vec.append(num_theory, to_exprs(theory));
#endif
ptr_vector<expr> cnsts_vec(num); // get constraints in a vector
for (unsigned i = 0; i < num; i++){
expr *a = to_expr(cnsts[i]);
cnsts_vec[i] = a;
}
for (unsigned i = 0; i < num_theory; i++){
expr *a = to_expr(theory[i]);
cnsts_vec.push_back(a);
}
Z3_ast tree = parents_vector_to_tree(ctx, num, cnsts, parents);
iz3pp(mk_c(ctx)->m(), cnsts_vec, to_expr(tree), f);
Z3_dec_ref(ctx, tree);
}
f.close();
#if 0
if(!parents){
iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory);
return;
}
std::vector<Z3_ast> tcnsts(num);
hash_map<int,Z3_ast> syms;
for(int j = 0; j < num - 1; j++){
std::ostringstream oss;
oss << "$P" << j;
std::string name = oss.str();
Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str());
Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx));
syms[j] = symbol;
tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol);
}
tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx));
for(int j = num-2; j >= 0; j--){
int parent = parents[j];
// assert(parent >= 0 && parent < num);
tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]);
}
iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory);
#endif
}
#endif
static std::vector<Z3_ast> read_cnsts;
static std::vector<unsigned> read_parents;
static std::ostringstream read_error;
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){
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);
assertions.resize(nconjs);
for (int k = 0; k < nconjs; k++)
assertions[k] = Z3_get_app_arg(ctx, app, k);
}
catch (...) {
read_error << "SMTLIB parse error: " << Z3_get_parser_error(ctx);
read_msg = read_error.str();
*error = read_msg.c_str();
return false;
}
Z3_set_error_handler(ctx, nullptr);
return true;
}
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[]){
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())
num_theory = atoi(file_params["THEORY"].c_str());
svector<Z3_ast> assertions;
if (!iZ3_parse(ctx, filename, error, assertions))
return false;
if (num_theory > assertions.size())
num_theory = assertions.size();
unsigned num = assertions.size() - 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; 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];
if (!parents){
*_num = num;
*cnsts = &read_cnsts[0];
return true;
}
for (unsigned j = 0; j < num; j++)
read_parents[j] = SHRT_MAX;
hash_map<Z3_ast, int> pred_map;
for (unsigned j = 0; j < num; j++){
Z3_ast lhs = nullptr, rhs = read_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);
Z3_ast lhs1 = Z3_get_app_arg(ctx, app1, 0);
Z3_ast rhs1 = Z3_get_app_arg(ctx, app1, 1);
if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, lhs1))) == Z3_OP_AND){
Z3_app app2 = Z3_to_app(ctx, lhs1);
int nconjs = Z3_get_app_num_args(ctx, app2);
for (int k = nconjs - 1; k >= 0; --k)
rhs1 = Z3_mk_implies(ctx, Z3_get_app_arg(ctx, app2, k), rhs1);
rhs = rhs1;
}
}
while (1){
Z3_app app = Z3_to_app(ctx, rhs);
Z3_func_decl func = Z3_get_app_decl(ctx, app);
Z3_decl_kind dk = Z3_get_decl_kind(ctx, func);
if (dk == Z3_OP_IMPLIES){
if (lhs){
Z3_ast child = lhs;
if (pred_map.find(child) == pred_map.end()){
read_error << "formula " << j + 1 << ": unknown: " << Z3_ast_to_string(ctx, child);
goto fail;
}
int child_num = pred_map[child];
if (read_parents[child_num] != SHRT_MAX){
read_error << "formula " << j + 1 << ": multiple reference: " << Z3_ast_to_string(ctx, child);
goto fail;
}
read_parents[child_num] = j;
}
lhs = Z3_get_app_arg(ctx, app, 0);
rhs = Z3_get_app_arg(ctx, app, 1);
}
else {
if (!lhs){
read_error << "formula " << j + 1 << ": should be (implies {children} fmla parent)";
goto fail;
}
read_cnsts[j] = lhs;
Z3_ast name = rhs;
if (pred_map.find(name) != pred_map.end()){
read_error << "formula " << j + 1 << ": duplicate symbol";
goto fail;
}
pred_map[name] = j;
break;
}
}
}
for (unsigned j = 0; j < num - 1; j++)
if (read_parents[j] == SHRT_MAX){
read_error << "formula " << j + 1 << ": unreferenced";
goto fail;
}
*_num = num;
*cnsts = &read_cnsts[0];
*parents = &read_parents[0];
return true;
fail:
read_msg = read_error.str();
*error = read_msg.c_str();
return false;
}
}
#if 0
/** Constant reprepresenting a root of a formula tree for tree interpolation */
#define IZ3_ROOT SHRT_MAX
/** This function uses Z3 to determine satisfiability of a set of
constraints. If UNSAT, an interpolant is returned, based on the
refutation generated by Z3. If SAT, a model is returned.
If "parents" is non-null, computes a tree interpolant. The tree is
defined by the array "parents". This array maps each formula in
the tree to its parent, where formulas are indicated by their
integer index in "cnsts". The parent of formula n must have index
greater than n. The last formula is the root of the tree. Its
parent entry should be the constant IZ3_ROOT.
If "parents" is null, computes a sequence interpolant.
\param ctx The Z3 context. Must be generated by iz3_mk_context
\param num The number of constraints in the sequence
\param cnsts Array of constraints (AST's in context ctx)
\param parents The parents vector defining the tree structure
\param options Interpolation options (may be NULL)
\param interps Array to return interpolants (size at least num-1, may be NULL)
\param model Returns a Z3 model if constraints SAT (may be NULL)
\param labels Returns relevant labels if SAT (may be NULL)
\param incremental
VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
context ctx. The model and interpolants returned are also
in this context.
The return code is as in Z3_check_assumptions, that is,
Z3_L_FALSE = constraints UNSAT (interpolants returned)
Z3_L_TRUE = constraints SAT (model returned)
Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
Currently, this function supports integer and boolean variables,
as well as arrays over these types, with linear arithmetic,
uninterpreted functions and quantifiers over integers (that is
AUFLIA). Interpolants are produced in AULIA. However, some
uses of array operations may cause quantifiers to appear in the
interpolants even when there are no quantifiers in the input formulas.
Although quantifiers may appear in the input formulas, Z3 may give up in
this case, returning Z3_L_UNDEF.
If "incremental" is true, cnsts must contain exactly the set of
formulas that are currently asserted in the context. If false,
there must be no formulas currently asserted in the context.
Setting "incremental" to true makes it posisble to incrementally
add and remove constraints from the context until the context
becomes UNSAT, at which point an interpolant is computed. Caution
must be used, however. Before popping the context, if you wish to
keep the interolant formulas, you *must* preserve them by using
Z3_persist_ast. Also, if you want to simplify the interpolant
formulas using Z3_simplify, you must first pop all of the
assertions in the context (or use a different context). Otherwise,
the formulas will be simplified *relative* to these constraints,
which is almost certainly not what you want.
Current limitations on tree interpolants. In a tree interpolation
problem, each constant (0-ary function symbol) must occur only
along one path from root to leaf. Function symbols (of arity > 0)
are considered to have global scope (i.e., may appear in any
interpolant formula).
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
*/
Z3_lbool Z3_API Z3_interpolate(Z3_context ctx,
unsigned num,
Z3_ast *cnsts,
unsigned *parents,
Z3_params options,
Z3_ast *interps,
Z3_model *model,
Z3_literals *labels,
unsigned incremental,
unsigned num_theory,
Z3_ast *theory);
#endif

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

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 {
@ -139,8 +140,16 @@ extern "C" {
r = to_optimize_ptr(o)->optimize();
}
catch (z3_exception& ex) {
mk_c(c)->handle_exception(ex);
if (!mk_c(c)->m().canceled()) {
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();
}
@ -296,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;

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

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]))) {
@ -361,7 +392,9 @@ extern "C" {
}
catch (z3_exception & ex) {
to_solver_ref(s)->set_reason_unknown(eh);
mk_c(c)->handle_exception(ex);
if (!mk_c(c)->m().canceled()) {
mk_c(c)->handle_exception(ex);
}
return Z3_L_UNDEF;
}
}
@ -552,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);
}
};

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

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

View file

@ -147,20 +147,12 @@ namespace z3 {
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
}
void init_interp(config & c) {
m_ctx = Z3_mk_interpolation_context(c);
m_enable_exceptions = true;
Z3_set_error_handler(m_ctx, 0);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
}
context(context const & s);
context & operator=(context const & s);
public:
struct interpolation {};
context() { config c; init(c); }
context(config & c) { init(c); }
context(config & c, interpolation) { init_interp(c); }
~context() { Z3_del_context(m_ctx); }
operator Z3_context() const { return m_ctx; }
@ -187,7 +179,7 @@ namespace z3 {
\brief The C++ API uses by defaults exceptions on errors.
For applications that don't work well with exceptions (there should be only few)
you have the ability to turn off exceptions. The tradeoffs are that applications
have to very careful about using check_error() after calls that may result in an
have to be very careful about using check_error() after calls that may result in an
erroneous state.
*/
void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
@ -329,17 +321,12 @@ 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
*/
check_result compute_interpolant(expr const& pat, params const& p, expr_vector& interp, model& m);
expr_vector get_interpolant(expr const& proof, expr const& pat, params const& p);
};
@ -440,6 +427,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 +832,6 @@ namespace z3 {
*/
friend expr operator!(expr const & a);
/**
\brief Return an expression representing <tt>a and b</tt>.
@ -901,6 +888,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 +1912,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 +2030,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 +2144,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 +2154,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 +2178,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 +2203,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; }
@ -2292,6 +2372,7 @@ namespace z3 {
class optimize : public object {
Z3_optimize m_opt;
public:
class handle {
unsigned m_h;
@ -2300,6 +2381,17 @@ namespace z3 {
unsigned h() const { return m_h; }
};
optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
optimize(optimize& o):object(o) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
m_opt = o.m_opt;
}
optimize& operator=(optimize const& o) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
Z3_optimize_dec_ref(ctx(), m_opt);
m_opt = o.m_opt;
m_ctx = o.m_ctx;
return *this;
}
~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
operator Z3_optimize() const { return m_opt; }
void add(expr const& e) {
@ -2864,22 +2956,19 @@ namespace z3 {
inline expr interpolant(expr const& a) {
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
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_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) {
Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
check_parser_error();
return expr(*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 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);
@ -2890,12 +2979,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);
@ -2906,33 +2996,12 @@ 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);
}
inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {
Z3_ast_vector interp = 0;
Z3_model mdl = 0;
Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
switch (r) {
case Z3_L_FALSE:
i = expr_vector(*this, interp);
break;
case Z3_L_TRUE:
m = model(*this, mdl);
break;
case Z3_L_UNDEF:
break;
}
return to_check_result(r);
}
inline expr_vector context::get_interpolant(expr const& proof, expr const& pat, params const& p) {
return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
}
inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
assert(src.size() == dst.size());
array<Z3_ast> _src(src.size());

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>

View file

@ -80,7 +80,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
Global.cs
Goal.cs
IDecRefQueue.cs
InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.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

View file

@ -317,14 +317,6 @@ namespace Microsoft.Z3
#endregion
#region Interpolation
/// <summary>
/// Indicates whether the term is marked for interpolation.
/// </summary>
/// <remarks></remarks>
public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
#endregion
#region Arithmetic Terms
/// <summary>
/// Indicates whether the term is of integer sort.

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>

View file

@ -1,164 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
using System.Runtime.InteropServices;
namespace Microsoft.Z3
{
/// <summary>
/// The InterpolationContext is suitable for generation of interpolants.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the C/C++ API, which is well documented.</remarks>
[ContractVerification(true)]
public class InterpolationContext : Context
{
/// <summary>
/// Constructor.
/// </summary>
public InterpolationContext() : base() { }
/// <summary>
/// Constructor.
/// </summary>
/// <remarks><seealso cref="Context"/></remarks>
public InterpolationContext(Dictionary<string, string> settings) : base(settings) { }
#region Terms
/// <summary>
/// Create an expression that marks a formula position for interpolation.
/// </summary>
public BoolExpr MkInterpolant(BoolExpr a)
{
Contract.Requires(a != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(a);
return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
}
#endregion
/// <summary>
/// Computes an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_get_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
Contract.Requires(pf != null);
Contract.Requires(pat != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(pf);
CheckContextMatch(pat);
CheckContextMatch(p);
ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
return seq.ToBoolExprArray();
}
/// <summary>
/// Computes an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_compute_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
{
Contract.Requires(pat != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
Contract.Ensures(Contract.ValueAtReturn(out model) != null);
CheckContextMatch(pat);
CheckContextMatch(p);
IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
interp = new ASTVector(this, i).ToBoolExprArray();
model = new Model(this, m);
return (Z3_lbool)r;
}
/// <summary>
/// Return a string summarizing cumulative time used for interpolation.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.</remarks>
public string InterpolationProfile()
{
return Native.Z3_interpolation_profile(nCtx);
}
/// <summary>
/// Checks the correctness of an interpolant.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.</remarks>
public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Contract.Requires(cnsts.Length == interps.Length + 1);
IntPtr n_err_str;
int r = Native.Z3_check_interpolant(nCtx,
(uint)cnsts.Length,
Expr.ArrayToNative(cnsts),
parents,
Expr.ArrayToNative(interps),
out n_err_str,
(uint)theory.Length,
Expr.ArrayToNative(theory));
error = Marshal.PtrToStringAnsi(n_err_str);
return r;
}
/// <summary>
/// Reads an interpolation problem from a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// 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;
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);
error = Marshal.PtrToStringAnsi(n_err_str);
cnsts = new Expr[num];
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]);
return r;
}
/// <summary>
/// Writes an interpolation problem to a file.
/// </summary>
/// <remarks>For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
{
Contract.Requires(cnsts.Length == parents.Length);
Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
}
}
}

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>

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

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.
**/

View file

@ -137,7 +137,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.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();
}
/**

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

View file

@ -1,216 +0,0 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
InterpolationContext.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
package com.microsoft.z3;
import com.microsoft.z3.enumerations.Z3_lbool;
import java.util.Map;
/**
* The InterpolationContext is suitable for generation of interpolants.
*
* Remarks: For more information on interpolation please refer
* too the C/C++ API, which is well documented.
**/
public class InterpolationContext extends Context
{
/**
* Constructor.
**/
public static InterpolationContext mkContext()
{
long m_ctx;
synchronized(creation_lock) {
m_ctx = Native.mkInterpolationContext(0);
}
return new InterpolationContext(m_ctx);
}
/**
* Constructor.
*
*
* Remarks:
* @see Context#Context
**/
public static InterpolationContext mkContext(Map<String, String> settings)
{
long m_ctx;
synchronized(creation_lock) {
long cfg = Native.mkConfig();
for (Map.Entry<String, String> kv : settings.entrySet())
Native.setParamValue(cfg, kv.getKey(), kv.getValue());
m_ctx = Native.mkInterpolationContext(cfg);
Native.delConfig(cfg);
}
return new InterpolationContext(m_ctx);
}
private InterpolationContext(long m_ctx) {
super(m_ctx);
}
/**
* Create an expression that marks a formula position for interpolation.
* @throws Z3Exception
**/
public BoolExpr MkInterpolant(BoolExpr a)
{
checkContextMatch(a);
return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
}
/**
* Computes an interpolant.
* Remarks: For more information on interpolation please refer
* too the function Z3_get_interpolant in the C/C++ API, which is
* well documented.
* @throws Z3Exception
**/
public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
checkContextMatch(pf);
checkContextMatch(pat);
checkContextMatch(p);
ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
return seq.ToBoolExprArray();
}
public class ComputeInterpolantResult
{
public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
public BoolExpr[] interp = null;
public Model model = null;
};
/**
* Computes an interpolant.
* Remarks: For more information on interpolation please refer
* too the function Z3_compute_interpolant in the C/C++ API, which is
* well documented.
* @throws Z3Exception
**/
public ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
{
checkContextMatch(pat);
checkContextMatch(p);
ComputeInterpolantResult res = new ComputeInterpolantResult();
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE)
res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
if (res.status == Z3_lbool.Z3_L_TRUE)
res.model = new Model(this, n_m.value);
return res;
}
///
/// Return a string summarizing cumulative time used for interpolation.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.
public String InterpolationProfile()
{
return Native.interpolationProfile(nCtx());
}
public class CheckInterpolantResult
{
public int return_value = 0;
public String error = null;
}
///
/// Checks the correctness of an interpolant.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.
public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
{
CheckInterpolantResult res = new CheckInterpolantResult();
Native.StringPtr n_err_str = new Native.StringPtr();
res.return_value = Native.checkInterpolant(nCtx(),
cnsts.length,
Expr.arrayToNative(cnsts),
parents,
Expr.arrayToNative(interps),
n_err_str,
theory.length,
Expr.arrayToNative(theory));
res.error = n_err_str.value;
return res;
}
public class ReadInterpolationProblemResult
{
public int return_value = 0;
public Expr[] cnsts;
public int[] parents;
public String error;
public Expr[] theory;
};
///
/// Reads an interpolation problem from a file.
///
/// 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)
{
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;
}
///
/// Writes an interpolation problem to a file.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.
public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
{
Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
}
}

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.
*

View file

@ -1654,7 +1654,6 @@ struct
mk_list f n
let get_subgoal (x:apply_result) (i:int) = Z3native.apply_result_get_subgoal (gc x) x i
let convert_model (x:apply_result) (i:int) (m:Model.model) = Z3native.apply_result_convert_model (gc x) x i m
let to_string (x:apply_result) = Z3native.apply_result_to_string (gc x) x
end
@ -1995,52 +1994,6 @@ struct
cs sort_names sorts cd decl_names decls
end
module Interpolation =
struct
let mk_interpolant = Z3native.mk_interpolant
let mk_interpolation_context (settings:(string * string) list) =
let cfg = Z3native.mk_config () in
let f e = Z3native.set_param_value cfg (fst e) (snd e) in
List.iter f settings;
let res = Z3native.mk_interpolation_context cfg in
Z3native.del_config cfg;
Z3native.set_ast_print_mode res (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT);
Z3native.set_internal_error_handler res;
res
let get_interpolant (ctx:context) (pf:expr) (pat:expr) (p:Params.params) =
let av = Z3native.get_interpolant ctx pf pat p in
AST.ASTVector.to_expr_list av
let compute_interpolant (ctx:context) (pat:expr) (p:Params.params) =
let (r, interp, model) = Z3native.compute_interpolant ctx pat p in
let res = lbool_of_int r in
match res with
| L_TRUE -> (res, None, Some model)
| L_FALSE -> (res, Some (AST.ASTVector.to_expr_list interp), None)
| _ -> (res, None, None)
let get_interpolation_profile = Z3native.interpolation_profile
let read_interpolation_problem (ctx:context) (filename:string) =
let (r, num, cnsts, parents, error, num_theory, theory) =
Z3native.read_interpolation_problem ctx filename
in
match r with
| 0 -> raise (Error "Interpolation problem could not be read.")
| _ -> (cnsts, parents, theory)
let check_interpolant (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (interps:Expr.expr list) (num_theory:int) (theory:Expr.expr list) =
let (r, str) = Z3native.check_interpolant ctx num cnsts parents interps num_theory theory in
match (lbool_of_int r) with
| L_UNDEF -> raise (Error "Interpolant could not be verified.")
| L_FALSE -> raise (Error "Interpolant could not be verified.")
| _ -> ()
let write_interpolation_problem (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (filename:string) (num_theory:int) (theory:Expr.expr list) =
Z3native.write_interpolation_problem ctx num cnsts parents filename num_theory theory
end
let set_global_param = Z3native.global_param_set

View file

@ -2362,7 +2362,7 @@ sig
(** Indicates whether the term is a proof by condensed transitivity of a relation
Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
Condensed transitivity proof.
It combines several symmetry and transitivity proofs.
Example:
T1: (R a b)
@ -2443,14 +2443,11 @@ sig
(** Indicates whether the term is a proof by rewriting
A proof for rewriting an expression t into an expression s.
This proof object is used if the parameter PROOF_MODE is 1.
This proof object can have n antecedents.
The antecedents are proofs for equalities used as substitution rules.
The object is also used in a few cases if the parameter PROOF_MODE is 2.
The cases are:
The object is also used in a few cases. The cases are:
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=true)
- When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) *)
- When converting bit-vectors to Booleans (BIT2BOOL=true) *)
val is_rewrite_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out.
@ -2967,11 +2964,6 @@ sig
(** Retrieves a subgoal from the apply_result. *)
val get_subgoal : apply_result -> int -> Goal.goal
(** Convert a model for a subgoal into a model for the original
goal [g], that the ApplyResult was obtained from.
#return A model for [g] *)
val convert_model : apply_result -> int -> Model.model -> Model.model
(** A string representation of the ApplyResult. *)
val to_string : apply_result -> string
end
@ -3427,51 +3419,6 @@ sig
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
end
(** Interpolation *)
module Interpolation :
sig
(** Create an AST node marking a formula position for interpolation.
The expression must have Boolean sort. *)
val mk_interpolant : context -> Expr.expr -> Expr.expr
(** The interpolation context is suitable for generation of interpolants.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val mk_interpolation_context : (string * string) list -> context
(** Gets an interpolant.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list
(** Computes an interpolant.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option)
(** Retrieves an interpolation profile.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val get_interpolation_profile : context -> string
(** Read an interpolation problem from file.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val read_interpolation_problem : context -> string -> (Expr.expr list * int list * Expr.expr list)
(** Check the correctness of an interpolant.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val check_interpolant : context -> int -> Expr.expr list -> int list -> Expr.expr list -> int -> Expr.expr list -> unit
(** Write an interpolation problem to file suitable for reading with
Z3_read_interpolation_problem.
For more information on interpolation please refer
too the C/C++ API, which is well documented. *)
val write_interpolation_problem : context -> int -> Expr.expr list -> int list -> string -> int -> Expr.expr list -> unit
end
(** Set a global (or module) parameter, which is shared by all Z3 contexts.

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.
@ -2754,6 +2765,8 @@ def _py2expr(a, ctx=None):
return IntVal(a, ctx)
if isinstance(a, float):
return RealVal(a, ctx)
if is_expr(a):
return a
if __debug__:
_z3_assert(False, "Python bool, int, long or float expected")
@ -4388,6 +4401,117 @@ def is_store(a):
"""
return is_app_of(a, Z3_OP_STORE)
#########################################
#
# Sets
#
#########################################
def SetSort(s):
""" Create a set sort over element sort s"""
return ArraySort(s, BoolSort())
def EmptySet(s):
"""Create the empty set
>>> EmptySet(IntSort())
K(Int, False)
"""
ctx = s.ctx
return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
def FullSet(s):
"""Create the full set
>>> FullSet(IntSort())
K(Int, True)
"""
ctx = s.ctx
return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
def SetUnion(*args):
""" Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetUnion(a, b)
union(a, b)
"""
args = _get_args(args)
ctx = _ctx_from_ast_arg_list(args)
_args, sz = _to_ast_array(args)
return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx)
def SetIntersect(*args):
""" Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetIntersect(a, b)
intersect(a, b)
"""
args = _get_args(args)
ctx = _ctx_from_ast_arg_list(args)
_args, sz = _to_ast_array(args)
return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx)
def SetAdd(s, e):
""" Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)
"""
ctx = _ctx_from_ast_arg_list([s,e])
e = _py2expr(e, ctx)
return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
def SetDel(s, e):
""" Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
"""
ctx = _ctx_from_ast_arg_list([s,e])
e = _py2expr(e, ctx)
return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
def SetComplement(s):
""" The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)
"""
ctx = s.ctx
return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx)
def SetDifference(a, b):
""" The set difference of a and b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetDifference(a, b)
difference(a, b)
"""
ctx = _ctx_from_ast_arg_list([a, b])
return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
def IsMember(e, s):
""" Check if e is a member of set s
>>> a = Const('a', SetSort(IntSort()))
>>> IsMember(1, a)
a[1]
"""
ctx = _ctx_from_ast_arg_list([s,e])
e = _py2expr(e, ctx)
return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
def IsSubset(a, b):
""" Check if a is a subset of b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> IsSubset(a, b)
subset(a, b)
"""
ctx = _ctx_from_ast_arg_list([a, b])
return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
#########################################
#
# Datatypes
@ -5032,6 +5156,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 +5192,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 +6252,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 +6559,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 +6604,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 +7377,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 +8353,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,151 +8377,11 @@ 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)
def Interpolant(a,ctx=None):
"""Create an interpolation operator.
The argument is an interpolation pattern (see tree_interpolant).
>>> x = Int('x')
>>> print(Interpolant(x>0))
interp(x > 0)
"""
ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
s = BoolSort(ctx)
a = s.cast(a)
return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
def tree_interpolant(pat,p=None,ctx=None):
"""Compute interpolant for a tree of formulas.
The input is an interpolation pattern over a set of formulas C.
The pattern pat is a formula combining the formulas in C using
logical conjunction and the "interp" operator (see Interp). This
interp operator is logically the identity operator. It marks the
sub-formulas of the pattern for which interpolants should be
computed. The interpolant is a map sigma from marked subformulas
to formulas, such that, for each marked subformula phi of pat
(where phi sigma is phi with sigma(psi) substituted for each
subformula psi of phi such that psi in dom(sigma)):
1) phi sigma implies sigma(phi), and
2) sigma(phi) is in the common uninterpreted vocabulary between
the formulas of C occurring in phi and those not occurring in
phi
and moreover pat sigma implies false. In the simplest case
an interpolant for the pattern "(and (interp A) B)" maps A
to an interpolant for A /\ B.
The return value is a vector of formulas representing sigma. This
vector contains sigma(phi) for each marked subformula of pat, in
pre-order traversal. This means that subformulas of phi occur before phi
in the vector. Also, subformulas that occur multiply in pat will
occur multiply in the result vector.
If pat is satisfiable, raises an object of class ModelRef
that represents a model of pat.
If neither a proof of unsatisfiability nor a model is obtained
(for example, because of a timeout, or because models are disabled)
then None is returned.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
>>> x = Int('x')
>>> y = Int('y')
>>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)))
[Not(x >= 0), Not(y <= 2)]
# >>> g = And(Interpolant(x<0),x<2)
# >>> try:
# ... print tree_interpolant(g).sexpr()
# ... except ModelRef as m:
# ... print m.sexpr()
(define-fun x () Int
(- 1))
"""
f = pat
ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
ptr = (AstVectorObj * 1)()
mptr = (Model * 1)()
if p is None:
p = ParamsRef(ctx)
res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
if res == Z3_L_FALSE:
return AstVector(ptr[0],ctx)
if mptr[0]:
raise ModelRef(mptr[0], ctx)
return None
def binary_interpolant(a,b,p=None,ctx=None):
"""Compute an interpolant for a binary conjunction.
If a & b is unsatisfiable, returns an interpolant for a & b.
This is a formula phi such that
1) a implies phi
2) b implies not phi
3) All the uninterpreted symbols of phi occur in both a and b.
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a &b.
If neither a proof of unsatisfiability nor a model is obtained
(for example, because of a timeout, or because models are disabled)
then None is returned.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
x = Int('x')
print(binary_interpolant(x<0,x>2))
Not(x >= 0)
"""
f = And(Interpolant(a),b)
ti = tree_interpolant(f,p,ctx)
return ti[0] if ti is not None else None
def sequence_interpolant(v,p=None,ctx=None):
"""Compute interpolant for a sequence of formulas.
If len(v) == N, and if the conjunction of the formulas in v is
unsatisfiable, the interpolant is a sequence of formulas w
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
and v[i+1]..v[n]
Requires len(v) >= 1.
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a & b.
If neither a proof of unsatisfiability nor a model is obtained
(for example, because of a timeout, or because models are disabled)
then None is returned.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
x = Int('x')
y = Int('y')
print(sequence_interpolant([x < 0, y == x , y > 2]))
[Not(x >= 0), Not(y >= 0)]
"""
f = v[0]
for i in range(1,len(v)):
f = And(Interpolant(f),v[i])
return tree_interpolant(f,p,ctx)
#########################################
#
@ -9826,6 +9846,14 @@ def String(name, ctx=None):
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
def SubString(s, offset, length):
"""Extract substring or subsequence starting at offset"""
return Extract(s, offset, length)
def SubSeq(s, offset, length):
"""Extract substring or subsequence starting at offset"""
return Extract(s, offset, length)
def Strings(names, ctx=None):
"""Return a tuple of String constants. """
ctx = _get_ctx(ctx)

View file

@ -32,7 +32,6 @@ Notes:
#include "z3_rcf.h"
#include "z3_fixedpoint.h"
#include "z3_optimization.h"
#include "z3_interp.h"
#include "z3_fpa.h"
#include "z3_spacer.h"
#endif

View file

@ -83,14 +83,14 @@ typedef const char * Z3_string;
typedef Z3_string * Z3_string_ptr;
/**
\brief True value. It is just an alias for \c 1.
\brief True value. It is just an alias for \c true.
*/
#define Z3_TRUE 1
#define Z3_TRUE true
/**
\brief False value. It is just an alias for \c 0.
\brief False value. It is just an alias for \c false.
*/
#define Z3_FALSE 0
#define Z3_FALSE false
/**
\brief Lifted Boolean type: \c false, \c undefined, \c true.
@ -212,8 +212,6 @@ typedef enum
- Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms.
It captures equisatisfiability and equivalence modulo renamings.
- Z3_OP_INTERP Marks a sub-formula for interpolation.
- Z3_OP_ANUM Arithmetic numeral.
- Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
@ -991,7 +989,6 @@ typedef enum {
Z3_OP_NOT,
Z3_OP_IMPLIES,
Z3_OP_OEQ,
Z3_OP_INTERP,
// Arithmetic
Z3_OP_ANUM = 0x200,
@ -5175,9 +5172,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 +5186,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 +5447,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 +5463,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 +5822,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 +5921,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 +6028,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 +6042,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 +6123,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

View file

@ -1,284 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
z3_interp.h
Abstract:
API for interpolation
Author:
Kenneth McMillan (kenmcmil)
Notes:
--*/
#ifndef Z3_INTERPOLATION_H_
#define Z3_INTERPOLATION_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name Interpolation facilities */
/*@{*/
/**
\brief Create an AST node marking a formula position for interpolation.
The node \c a must have Boolean sort.
def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a);
/** \brief This function generates a Z3 context suitable for generation of
interpolants. Formulas can be generated as abstract syntax trees in
this context using the Z3 C API.
Interpolants are also generated as AST's in this context.
If cfg is non-null, it will be used as the base configuration
for the Z3 context. This makes it possible to set Z3 options
to be used during interpolation. This feature should be used
with some caution however, as it may be that certain Z3 options
are incompatible with interpolation.
def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
*/
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg);
/** Compute an interpolant from a refutation. This takes a proof of
"false" from a set of formulas C, and an interpolation
pattern. The pattern pat is a formula combining the formulas in C
using logical conjunction and the "interp" operator (see
#Z3_mk_interpolant). This interp operator is logically the identity
operator. It marks the sub-formulas of the pattern for which interpolants should
be computed. The interpolant is a map sigma from marked subformulas to
formulas, such that, for each marked subformula phi of pat (where phi sigma
is phi with sigma(psi) substituted for each subformula psi of phi such that
psi in dom(sigma)):
1) phi sigma implies sigma(phi), and
2) sigma(phi) is in the common uninterpreted vocabulary between
the formulas of C occurring in phi and those not occurring in
phi
and moreover pat sigma implies false. In the simplest case
an interpolant for the pattern "(and (interp A) B)" maps A
to an interpolant for A /\ B.
The return value is a vector of formulas representing sigma. The
vector contains sigma(phi) for each marked subformula of pat, in
pre-order traversal. This means that subformulas of phi occur before phi
in the vector. Also, subformulas that occur multiply in pat will
occur multiply in the result vector.
In particular, calling Z3_get_interpolant on a pattern of the
form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
result in a sequence interpolant for A_1, A_2,... A_N.
Neglecting interp markers, the pattern must be a conjunction of
formulas in C, the set of premises of the proof. Otherwise an
error is flagged.
Any premises of the proof not present in the pattern are
treated as "background theory". Predicate and function symbols
occurring in the background theory are treated as interpreted and
thus always allowed in the interpolant.
Interpolant may not necessarily be computable from all
proofs. To be sure an interpolant can be computed, the proof
must be generated by an SMT solver for which interpolation is
supported, and the premises must be expressed using only
theories and operators for which interpolation is supported.
Currently, the only SMT solver that is supported is the legacy
SMT solver. Such a solver is available as the default solver in
\c Z3_context objects produced by #Z3_mk_interpolation_context.
Currently, the theories supported are equality with
uninterpreted functions, linear integer arithmetic, and the
theory of arrays (in SMT-LIB terms, this is AUFLIA).
Quantifiers are allowed. Use of any other operators (including
"labels") may result in failure to compute an interpolant from a
proof.
Parameters:
\param c logical context.
\param pf a refutation from premises (assertions) C
\param pat an interpolation pattern over C
\param p parameters
def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
*/
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
/* Compute an interpolant for an unsatisfiable conjunction of formulas.
This takes as an argument an interpolation pattern as in
#Z3_get_interpolant. This is a conjunction, some subformulas of
which are marked with the "interp" operator (see #Z3_mk_interpolant).
The conjunction is first checked for unsatisfiability. The result
of this check is returned in the out parameter "status". If the result
is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
and returned as a vector of formulas. Otherwise the return value is
an empty formula.
See #Z3_get_interpolant for a discussion of supported theories.
The advantage of this function over #Z3_get_interpolant is that
it is not necessary to create a suitable SMT solver and generate
a proof. The disadvantage is that it is not possible to use the
solver incrementally.
Parameters:
\param c logical context.
\param pat an interpolation pattern
\param p parameters for solver creation
\param status returns the status of the sat check
\param model returns model if satisfiable
Return value: status of SAT check
def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
*/
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
Z3_ast pat,
Z3_params p,
Z3_ast_vector *interp,
Z3_model *model);
/** Return a string summarizing cumulative time used for
interpolation. This string is purely for entertainment purposes
and has no semantics.
\param ctx The context (currently ignored)
def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
*/
Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
/**
\brief Read an interpolation problem from file.
\param ctx The Z3 context. This resets the error handler of ctx.
\param filename The file name to read.
\param num Returns length of sequence.
\param cnsts Returns sequence of formulas (do not free)
\param parents Returns the parents vector (or NULL for sequence)
\param error Returns an error message in case of failure (do not free the string)
\param num_theory Number of theory terms
\param theory Theory terms
Returns true on success.
File formats: Currently two formats are supported, based on
SMT-LIB2. For sequence interpolants, the sequence of constraints is
represented by the sequence of "assert" commands in the file.
For tree interpolants, one symbol of type bool is associated to
each vertex of the tree. For each vertex v there is an "assert"
of the form:
(implies (and c1 ... cn f) v)
where c1 .. cn are the children of v (which must precede v in the file)
and f is the formula associated to node v. The last formula in the
file is the root vertex, and is represented by the predicate "false".
A solution to a tree interpolation problem can be thought of as a
valuation of the vertices that makes all the implications true
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)))
*/
int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
unsigned *num,
Z3_ast *cnsts[],
unsigned *parents[],
Z3_string filename,
Z3_string_ptr error,
unsigned *num_theory,
Z3_ast *theory[]);
/** Check the correctness of an interpolant. The Z3 context must
have no constraints asserted when this call is made. That means
that after interpolating, you must first fully pop the Z3
context before calling this. See Z3_interpolate for meaning of parameters.
\param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
\param num The number of constraints in the sequence
\param cnsts Array of constraints (AST's in context ctx)
\param parents The parents vector (or NULL for sequence)
\param interps The interpolant to check
\param error Returns an error message if interpolant incorrect (do not free the string)
\param num_theory Number of theory terms
\param theory Theory terms
Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
incorrect, and Z3_L_UNDEF if unknown.
def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST)))
*/
int Z3_API Z3_check_interpolant(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_ast *interps,
Z3_string_ptr error,
unsigned num_theory,
Z3_ast theory[]);
/** Write an interpolation problem to file suitable for reading with
Z3_read_interpolation_problem. The output file is a sequence
of SMT-LIB2 format commands, suitable for reading with command-line Z3
or other interpolating solvers.
\param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
\param num The number of constraints in the sequence
\param cnsts Array of constraints
\param parents The parents vector (or NULL for sequence)
\param filename The file name to write
\param num_theory Number of theory terms
\param theory Theory terms
def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
*/
void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_string filename,
unsigned num_theory,
Z3_ast theory[]);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif

View file

@ -646,7 +646,6 @@ basic_decl_plugin::basic_decl_plugin():
m_iff_decl(nullptr),
m_xor_decl(nullptr),
m_not_decl(nullptr),
m_interp_decl(nullptr),
m_implies_decl(nullptr),
m_proof_sort(nullptr),
@ -865,7 +864,6 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_iff_decl = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true);
m_xor_decl = mk_bool_op_decl("xor", OP_XOR, 2, true, true);
m_not_decl = mk_bool_op_decl("not", OP_NOT, 1);
m_interp_decl = mk_bool_op_decl("interp", OP_INTERP, 1);
m_implies_decl = mk_implies_decl();
m_proof_sort = m->mk_sort(symbol("Proof"), sort_info(id, PROOF_SORT));
@ -890,7 +888,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("or", OP_OR));
op_names.push_back(builtin_name("xor", OP_XOR));
op_names.push_back(builtin_name("not", OP_NOT));
op_names.push_back(builtin_name("interp", OP_INTERP));
op_names.push_back(builtin_name("=>", OP_IMPLIES));
if (logic == symbol::null) {
// user friendly aliases
@ -902,7 +899,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("||", OP_OR));
op_names.push_back(builtin_name("equals", OP_EQ));
op_names.push_back(builtin_name("equiv", OP_IFF));
op_names.push_back(builtin_name("@@", OP_INTERP));
}
}
@ -923,7 +919,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_and_decl);
DEC_REF(m_or_decl);
DEC_REF(m_not_decl);
DEC_REF(m_interp_decl);
DEC_REF(m_iff_decl);
DEC_REF(m_xor_decl);
DEC_REF(m_implies_decl);
@ -1056,7 +1051,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
@ -1099,7 +1093,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
@ -1348,6 +1341,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 +1503,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 +2218,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 << "!";

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(); }
};
// -----------------------------------
@ -1038,7 +1041,7 @@ enum basic_sort_kind {
};
enum basic_op_kind {
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP,
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
@ -1060,7 +1063,6 @@ protected:
func_decl * m_iff_decl;
func_decl * m_xor_decl;
func_decl * m_not_decl;
func_decl * m_interp_decl;
func_decl * m_implies_decl;
ptr_vector<func_decl> m_eq_decls; // cached eqs
ptr_vector<func_decl> m_ite_decls; // cached ites
@ -1451,6 +1453,8 @@ public:
void show_id_gen();
void update_fresh_id(ast_manager const& other);
protected:
reslimit m_limit;
small_object_allocator m_alloc;
@ -2049,7 +2053,6 @@ public:
app * mk_true() const { return m_true; }
app * mk_false() const { return m_false; }
app * mk_bool_val(bool b) { return b?m_true:m_false; }
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
func_decl* mk_and_decl() {

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

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

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

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,25 +915,28 @@ 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);
}
else {
var_name = it->str ();\
var_name = it->str ();
}
buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
}
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;
}

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)

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 << ")";
}

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 {

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

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;

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

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

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

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

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

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

View file

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

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;

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()):

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

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

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,10 +39,12 @@ 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;
typedef ptr_vector<expr> literal_vector;
typedef expr* pliteral;
typedef ptr_vector<expr> pliteral_vector;
psort_nw<card2bv_rewriter> m_sort;
ast_manager& m;
imp& m_imp;
@ -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.
Translating Pseudo-Boolean Constraints into SAT,
Niklas Een, Niklas Soerensson, 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(bool full, expr* e, expr_ref& r) {
app* a;
return (is_app(e) && (a = to_app(e), mk_app(full, 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,53 +802,95 @@ 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);
}
TRACE("pb", tout << "full: " << full << " " << expr_ref(m.mk_app(f, sz, args), m) << " " << result << "\n";
);
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
literal mk_false() { return m.mk_false(); }
literal mk_true() { return m.mk_true(); }
literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); }
literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
pliteral mk_false() { return m.mk_false(); }
pliteral mk_true() { return m.mk_true(); }
pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); }
pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); }
pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
std::ostream& pp(std::ostream& out, literal lit) { return out << mk_ismt2_pp(lit, m); }
std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_ismt2_pp(lit, m); }
literal trail(literal l) {
pliteral trail(pliteral l) {
m_trail.push_back(l);
return l;
}
literal fresh() {
expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m);
pliteral 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));
void mk_clause(unsigned n, pliteral const* 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 +902,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 +914,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(bool full, expr* e, expr_ref& r, proof_ref& p) {
expr_ref ee(e, m());
if (m_cfg.m_r.mk_app(full, 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);
void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) {
// m_rw(e, result, result_proof);
m_rw.rewrite(full, e, result, result_proof);
}
void push() {
m_fresh_lim.push_back(m_fresh.size());
@ -453,6 +1007,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,11 +1019,13 @@ 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); }
func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
void pb2bv_rewriter::operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(full, e, result, result_proof); }
void pb2bv_rewriter::push() { m_imp->push(); }
void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }

View file

@ -31,11 +31,12 @@ 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();
func_decl_ref_vector const& fresh_constants() const;
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);
void flush_side_constraints(expr_ref_vector& side_constraints);

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

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;

View file

@ -431,7 +431,8 @@ struct poly_rewriter<Config>::hoist_cmul_lt {
hoist_cmul_lt(poly_rewriter<Config> & r):m_r(r) {}
bool operator()(expr * t1, expr * t2) const {
expr * pp1, * pp2;
expr * pp1 = nullptr;
expr * pp2 = nullptr;
numeral c1, c2;
bool is_mul1 = m_r.is_mul(t1, c1, pp1);
bool is_mul2 = m_r.is_mul(t2, c2, pp2);

View file

@ -336,9 +336,9 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
UNREACHABLE();
}
// TODO: add rewrite rules support
expr * def;
proof * def_pr;
quantifier * def_q;
expr * def = nullptr;
proof * def_pr = nullptr;
quantifier * def_q = nullptr;
// When get_macro succeeds, then
// we know that:
// forall X. f(X) = def[X]

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

View file

@ -8,14 +8,12 @@ z3_add_component(cmd_context
context_params.cpp
echo_tactic.cpp
eval_cmd.cpp
interpolant_cmds.cpp
parametric_cmd.cpp
pdecl.cpp
simplify_cmd.cpp
tactic_cmds.cpp
tactic_manager.cpp
COMPONENT_DEPENDENCIES
interp
rewriter
solver
EXTRA_REGISTER_MODULE_HEADERS

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;
@ -395,7 +394,7 @@ class set_option_cmd : public set_get_option_cmd {
env_params::updt_params();
ctx.global_params_updated();
}
catch (gparams::exception ex) {
catch (const gparams::exception & ex) {
throw cmd_exception(ex.msg());
}
}
@ -620,7 +619,7 @@ public:
try {
ctx.regular_stream() << gparams::get_value(opt) << std::endl;
}
catch (gparams::exception ex) {
catch (const gparams::exception &) {
ctx.print_unsupported(opt, m_line, m_pos);
}
}

View file

@ -43,9 +43,9 @@ 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"
#include "cmd_context/cmd_context.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
@ -396,7 +396,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 +406,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);
@ -483,7 +483,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
install_basic_cmds(*this);
install_ext_basic_cmds(*this);
install_core_tactic_cmds(*this);
install_interpolant_cmds(*this);
SASSERT(m != 0 || !has_manager());
if (m_main_ctx) {
set_verbose_stream(diagnostic_stream());
@ -498,6 +497,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 +870,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 +1273,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 +1429,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);
@ -1500,12 +1518,20 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
scoped_rlimit _rlimit(m().limit(), rlimit);
try {
r = m_solver->check_sat(num_assumptions, assumptions);
if (r == l_undef && m().canceled()) {
m_solver->set_reason_unknown(eh);
}
}
catch (z3_error & ex) {
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 +1543,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 +1550,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 +1624,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 +1716,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 +1782,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 +1827,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 +1913,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 +1946,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 {

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

View file

@ -135,7 +135,7 @@ void context_params::set(char const * param, char const * value) {
}
void context_params::updt_params() {
updt_params(gparams::get());
updt_params(gparams::get_ref());
}
void context_params::updt_params(params_ref const & p) {

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

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

View file

@ -271,7 +271,7 @@ UNARY_CMD(elim_unused_vars_cmd, "dbg-elim-unused-vars", "<expr>", "eliminate unu
return;
}
expr_ref r(ctx.m());
elim_unused_vars(ctx.m(), to_quantifier(arg), gparams::get(), r);
elim_unused_vars(ctx.m(), to_quantifier(arg), gparams::get_ref(), r);
SASSERT(!is_quantifier(r) || !to_quantifier(r)->may_have_unused_vars());
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;

View file

@ -1,263 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
interpolant_cmds.cpp
Abstract:
Commands for interpolation.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#include<sstream>
#include "cmd_context/cmd_context.h"
#include "cmd_context/cmd_util.h"
#include "util/scoped_timer.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "cmd_context/parametric_cmd.h"
#include "util/mpq.h"
#include "ast/expr2var.h"
#include "ast/pp.h"
#include "interp/iz3interp.h"
#include "interp/iz3checker.h"
#include "interp/iz3profiling.h"
#include "interp/interp_params.hpp"
#include "ast/scoped_proof.h"
static void show_interpolant_and_maybe_check(cmd_context & ctx,
ptr_vector<ast> &cnsts,
expr *t,
ptr_vector<ast> &interps,
params_ref &m_params,
bool check)
{
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
ctx.regular_stream() << "(interpolants";
for(unsigned i = 0; i < interps.size(); i++){
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
s(to_expr(interps[i]),r,pr);
ctx.regular_stream() << "\n " << r;
}
ctx.regular_stream() << ")\n";
s.cleanup();
// verify, for the paranoid...
if(check || interp_params(m_params).check()){
std::ostringstream err;
ast_manager &_m = ctx.m();
// need a solver -- make one here FIXME is this right?
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p;
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
scoped_ptr<solver> sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());
if(iz3check(_m,sp.get(),err,cnsts,t,interps))
ctx.regular_stream() << "correct\n";
else
ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
}
for(unsigned i = 0; i < interps.size(); i++){
ctx.m().dec_ref(interps[i]);
}
interp_params itp_params(m_params);
if(itp_params.profile())
profiling::print(ctx.regular_stream());
}
static void check_can_interpolate(cmd_context & ctx){
if (!ctx.produce_interpolants())
throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
}
static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check) {
check_can_interpolate(ctx);
// get the proof, if there is one
if (!ctx.has_manager() ||
ctx.cs_state() != cmd_context::css_unsat)
throw cmd_exception("proof is not available");
expr_ref pr(ctx.m());
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
throw cmd_exception("proof is not available");
// get the assertions from the context
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
ptr_vector<ast> cnsts((unsigned)(end - it));
for (int i = 0; it != end; ++it, ++i)
cnsts[i] = *it;
// compute an interpolant
ptr_vector<ast> interps;
try {
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,nullptr);
}
catch (iz3_bad_tree &) {
throw cmd_exception("interpolation pattern contains non-asserted formula");
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
}
static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
get_interpolant_and_maybe_check(ctx,t,m_params,false);
}
#if 0
static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
get_interpolant_and_maybe_check(ctx,t,m_params,true);
}
#endif
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
// create a fresh solver suitable for interpolation
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p;
ast_manager &_m = ctx.m();
// TODO: the following is a HACK to enable proofs in the old smt solver
// When we stop using that solver, this hack can be removed
scoped_proof_mode spm(_m,PGM_ENABLED);
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
p.set_bool("proof", true);
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
ptr_vector<ast> cnsts;
ptr_vector<ast> interps;
model_ref m;
// compute an interpolant
lbool res;
try {
res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, nullptr);
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
switch(res){
case l_false:
ctx.regular_stream() << "unsat\n";
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
break;
case l_true:
ctx.regular_stream() << "sat\n";
// TODO: how to return the model to the context, if it exists?
break;
case l_undef:
ctx.regular_stream() << "unknown\n";
// TODO: how to return the model to the context, if it exists?
break;
}
for(unsigned i = 0; i < cnsts.size(); i++)
ctx.m().dec_ref(cnsts[i]);
}
static expr *make_tree(cmd_context & ctx, const ptr_vector<expr> &exprs){
if(exprs.size() == 0)
throw cmd_exception("not enough arguments");
expr *foo = exprs[0];
for(unsigned i = 1; i < exprs.size(); i++){
foo = ctx.m().mk_and(ctx.m().mk_interp(foo),exprs[i]);
}
return foo;
}
static void get_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
expr_ref foo(make_tree(ctx, exprs),ctx.m());
get_interpolant(ctx,foo.get(),m_params);
}
static void compute_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
expr_ref foo(make_tree(ctx, exprs),ctx.m());
compute_interpolant_and_maybe_check(ctx,foo.get(),m_params,false);
}
// UNARY_CMD(get_interpolant_cmd, "get-interpolant", "<fmla>", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
// UNARY_CMD(get_and_check_interpolant_cmd, "get-and-check-interpolant", "<fmla>", "get and check interpolant for marked positions in fmla", CPK_EXPR, expr *, get_and_check_interpolant(ctx, arg););
class get_interpolant_cmd : public parametric_cmd {
protected:
ptr_vector<expr> m_targets;
public:
get_interpolant_cmd(char const * name = "get-interpolant"):parametric_cmd(name) {}
char const * get_usage() const override { return "<fmla>+"; }
char const * get_main_descr() const override {
return "get interpolant for formulas";
}
void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
}
void prepare(cmd_context & ctx) override {
parametric_cmd::prepare(ctx);
m_targets.resize(0);
}
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
return CPK_EXPR;
}
void set_next_arg(cmd_context & ctx, expr * arg) override {
m_targets.push_back(arg);
}
void execute(cmd_context & ctx) override {
get_interpolant(ctx,m_targets,m_params);
}
};
class compute_interpolant_cmd : public get_interpolant_cmd {
public:
compute_interpolant_cmd(char const * name = "compute-interpolant"):get_interpolant_cmd(name) {}
void execute(cmd_context & ctx) override {
compute_interpolant(ctx,m_targets,m_params);
}
};
void install_interpolant_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_interpolant_cmd));
ctx.insert(alloc(compute_interpolant_cmd));
// ctx.insert(alloc(get_and_check_interpolant_cmd));
}

View file

@ -1,24 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
interpolant_cmds.h
Abstract:
Commands for interpolation.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#ifndef INTERPOLANT_CMDS_H_
#define INTERPOLANT_CMDS_H_
class cmd_context;
void install_interpolant_cmds(cmd_context & ctx);
#endif

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

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

View file

@ -1,11 +0,0 @@
z3_add_component(duality
SOURCES
duality_profiling.cpp
duality_rpfp.cpp
duality_solver.cpp
duality_wrapper.cpp
COMPONENT_DEPENDENCIES
interp
qe
smt
)

File diff suppressed because it is too large Load diff

View file

@ -1,144 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
duality_profiling.cpp
Abstract:
collection performance information for duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#include <map>
#include <iostream>
#include <string>
#include <string.h>
#include <stdlib.h>
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#endif
#include "duality/duality_wrapper.h"
#include "interp/iz3profiling.h"
namespace Duality {
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
typedef std::map<const char*, struct node> nmap;
struct node {
std::string name;
clock_t time;
clock_t start_time;
nmap sub;
struct node *parent;
node();
} top;
node::node(){
time = 0;
parent = nullptr;
}
struct node *current;
struct init {
init(){
top.name = "TOTAL";
current = &top;
}
} initializer;
struct time_entry {
clock_t t;
time_entry(){t = 0;};
void add(clock_t incr){t += incr;}
};
struct ltstr
{
bool operator()(const char* s1, const char* s2) const
{
return strcmp(s1, s2) < 0;
}
};
typedef std::map<const char*, time_entry, ltstr> tmap;
static std::ostream *pfs;
void print_node(node &top, int indent, tmap &totals){
for(int i = 0; i < indent; i++) (*pfs) << " ";
(*pfs) << top.name;
int dots = 70 - 2 * indent - top.name.size();
for(int i = 0; i <dots; i++) (*pfs) << ".";
output_time(*pfs, top.time);
(*pfs) << std::endl;
if(indent != 0)totals[top.name.c_str()].add(top.time);
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
print_node(it->second,indent+1,totals);
}
void print_profile(std::ostream &os) {
pfs = &os;
top.time = 0;
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
top.time += it->second.time;
tmap totals;
print_node(top,0,totals);
(*pfs) << "TOTALS:" << std::endl;
for(tmap::iterator it = totals.begin(); it != totals.end(); it++){
(*pfs) << (it->first) << " ";
output_time(*pfs, it->second.t);
(*pfs) << std::endl;
}
profiling::print(os); // print the interpolation stats
}
void timer_start(const char *name){
node &child = current->sub[name];
if(child.name.empty()){ // a new node
child.parent = current;
child.name = name;
}
child.start_time = current_time();
current = &child;
}
void timer_stop(const char *name){
if (current->name != name || !current->parent) {
#if 0
std::cerr << "imbalanced timer_start and timer_stop";
exit(1);
#endif
// in case we lost a timer stop due to an exception
while (current->name != name && current->parent)
current = current->parent;
if (current->parent) {
current->time += (current_time() - current->start_time);
current = current->parent;
}
return;
}
current->time += (current_time() - current->start_time);
current = current->parent;
}
}

View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
duality_profiling.h
Abstract:
collection performance information for duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef DUALITYPROFILING_H
#define DUALITYPROFILING_H
#include <ostream>
namespace Duality {
/** Start a timer with given name */
void timer_start(const char *);
/** Stop a timer with given name */
void timer_stop(const char *);
/** Print out timings */
void print_profile(std::ostream &s);
/** Show the current time. */
void show_time();
}
#endif

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -1,744 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
wrapper.cpp
Abstract:
wrap various objects in the style expected by duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "duality/duality_wrapper.h"
#include <iostream>
#include "smt/smt_solver.h"
#include "interp/iz3interp.h"
#include "util/statistics.h"
#include "ast/expr_abstract.h"
#include "util/stopwatch.h"
#include "model/model_smt2_pp.h"
#include "qe/qe_lite.h"
namespace Duality {
solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) {
params_ref p;
p.set_bool("proof", true); // this is currently useless
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
extensional = mbqi && (true || _extensional);
if(extensional)
p.set_bool("array.extensional",true);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
m_solver->updt_params(p); // why do we have to do this?
canceled = false;
m_mode = m().proof_mode();
}
expr context::constant(const std::string &name, const sort &ty){
symbol s = str_symbol(name.c_str());
return cook(m().mk_const(m().mk_const_decl(s, ty)));
}
expr context::make(decl_kind op, int n, ::expr **args){
switch(op) {
case True: return mki(m_basic_fid,OP_TRUE,n,args);
case False: return mki(m_basic_fid,OP_FALSE,n,args);
case Equal: return mki(m_basic_fid,OP_EQ,n,args);
case Distinct: return mki(m_basic_fid,OP_DISTINCT,n,args);
case Ite: return mki(m_basic_fid,OP_ITE,n,args);
case And: return mki(m_basic_fid,OP_AND,n,args);
case Or: return mki(m_basic_fid,OP_OR,n,args);
case Iff: return mki(m_basic_fid,OP_IFF,n,args);
case Xor: return mki(m_basic_fid,OP_XOR,n,args);
case Not: return mki(m_basic_fid,OP_NOT,n,args);
case Implies: return mki(m_basic_fid,OP_IMPLIES,n,args);
case Oeq: return mki(m_basic_fid,OP_OEQ,n,args);
case Interp: return mki(m_basic_fid,OP_INTERP,n,args);
case Leq: return mki(m_arith_fid,OP_LE,n,args);
case Geq: return mki(m_arith_fid,OP_GE,n,args);
case Lt: return mki(m_arith_fid,OP_LT,n,args);
case Gt: return mki(m_arith_fid,OP_GT,n,args);
case Plus: return mki(m_arith_fid,OP_ADD,n,args);
case Sub: return mki(m_arith_fid,OP_SUB,n,args);
case Uminus: return mki(m_arith_fid,OP_UMINUS,n,args);
case Times: return mki(m_arith_fid,OP_MUL,n,args);
case Div: return mki(m_arith_fid,OP_DIV,n,args);
case Idiv: return mki(m_arith_fid,OP_IDIV,n,args);
case Rem: return mki(m_arith_fid,OP_REM,n,args);
case Mod: return mki(m_arith_fid,OP_MOD,n,args);
case Power: return mki(m_arith_fid,OP_POWER,n,args);
case ToReal: return mki(m_arith_fid,OP_TO_REAL,n,args);
case ToInt: return mki(m_arith_fid,OP_TO_INT,n,args);
case IsInt: return mki(m_arith_fid,OP_IS_INT,n,args);
case Store: return mki(m_array_fid,OP_STORE,n,args);
case Select: return mki(m_array_fid,OP_SELECT,n,args);
case ConstArray: return mki(m_array_fid,OP_CONST_ARRAY,n,args);
case ArrayDefault: return mki(m_array_fid,OP_ARRAY_DEFAULT,n,args);
case ArrayMap: return mki(m_array_fid,OP_ARRAY_MAP,n,args);
case SetUnion: return mki(m_array_fid,OP_SET_UNION,n,args);
case SetIntersect: return mki(m_array_fid,OP_SET_INTERSECT,n,args);
case SetDifference: return mki(m_array_fid,OP_SET_DIFFERENCE,n,args);
case SetComplement: return mki(m_array_fid,OP_SET_COMPLEMENT,n,args);
case SetSubSet: return mki(m_array_fid,OP_SET_SUBSET,n,args);
case AsArray: return mki(m_array_fid,OP_AS_ARRAY,n,args);
default:
assert(0);
return expr(*this);
}
}
expr context::mki(family_id fid, ::decl_kind dk, int n, ::expr **args){
return cook(m().mk_app(fid, dk, 0, nullptr, n, (::expr **)args));
}
expr context::make(decl_kind op, const std::vector<expr> &args){
static std::vector< ::expr*> a(10);
if(a.size() < args.size())
a.resize(args.size());
for(unsigned i = 0; i < args.size(); i++)
a[i] = to_expr(args[i].raw());
return make(op,args.size(), args.size() ? VEC2PTR(a) : nullptr);
}
expr context::make(decl_kind op){
return make(op,0,nullptr);
}
expr context::make(decl_kind op, const expr &arg0){
::expr *a = to_expr(arg0.raw());
return make(op,1,&a);
}
expr context::make(decl_kind op, const expr &arg0, const expr &arg1){
::expr *args[2];
args[0] = to_expr(arg0.raw());
args[1] = to_expr(arg1.raw());
return make(op,2,args);
}
expr context::make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2){
::expr *args[3];
args[0] = to_expr(arg0.raw());
args[1] = to_expr(arg1.raw());
args[2] = to_expr(arg2.raw());
return make(op,3,args);
}
expr context::make_quant(decl_kind op, const std::vector<expr> &bvs, const expr &body){
if(bvs.size() == 0) return body;
std::vector< ::expr *> foo(bvs.size());
std::vector< ::symbol> names;
std::vector< ::sort *> types;
std::vector< ::expr *> bound_asts;
unsigned num_bound = bvs.size();
for (unsigned i = 0; i < num_bound; ++i) {
app* a = to_app(bvs[i].raw());
::symbol s(to_app(a)->get_decl()->get_name());
names.push_back(s);
types.push_back(m().get_sort(a));
bound_asts.push_back(a);
}
expr_ref abs_body(m());
expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body);
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),
0,
::symbol(),
::symbol(),
0, nullptr,
0, nullptr
);
return cook(result.get());
}
expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body){
if(_sorts.size() == 0) return body;
std::vector< ::symbol> names;
std::vector< ::sort *> types;
std::vector< ::expr *> bound_asts;
unsigned num_bound = _sorts.size();
for (unsigned i = 0; i < num_bound; ++i) {
names.push_back(_names[i]);
types.push_back(to_sort(_sorts[i].raw()));
}
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),
0,
::symbol(),
::symbol(),
0, nullptr,
0, nullptr
);
return cook(result.get());
}
decl_kind func_decl::get_decl_kind() const {
return ctx().get_decl_kind(*this);
}
decl_kind context::get_decl_kind(const func_decl &t){
::func_decl *d = to_func_decl(t.raw());
if (null_family_id == d->get_family_id())
return Uninterpreted;
// return (opr)d->get_decl_kind();
if (m_basic_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_TRUE: return True;
case OP_FALSE: return False;
case OP_EQ: return Equal;
case OP_DISTINCT: return Distinct;
case OP_ITE: return Ite;
case OP_AND: return And;
case OP_OR: return Or;
case OP_IFF: return Iff;
case OP_XOR: return Xor;
case OP_NOT: return Not;
case OP_IMPLIES: return Implies;
case OP_OEQ: return Oeq;
case OP_INTERP: return Interp;
default:
return OtherBasic;
}
}
if (m_arith_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_LE: return Leq;
case OP_GE: return Geq;
case OP_LT: return Lt;
case OP_GT: return Gt;
case OP_ADD: return Plus;
case OP_SUB: return Sub;
case OP_UMINUS: return Uminus;
case OP_MUL: return Times;
case OP_DIV: return Div;
case OP_IDIV: return Idiv;
case OP_REM: return Rem;
case OP_MOD: return Mod;
case OP_POWER: return Power;
case OP_TO_REAL: return ToReal;
case OP_TO_INT: return ToInt;
case OP_IS_INT: return IsInt;
default:
return OtherArith;
}
}
if (m_array_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_STORE: return Store;
case OP_SELECT: return Select;
case OP_CONST_ARRAY: return ConstArray;
case OP_ARRAY_DEFAULT: return ArrayDefault;
case OP_ARRAY_MAP: return ArrayMap;
case OP_SET_UNION: return SetUnion;
case OP_SET_INTERSECT: return SetIntersect;
case OP_SET_DIFFERENCE: return SetDifference;
case OP_SET_COMPLEMENT: return SetComplement;
case OP_SET_SUBSET: return SetSubSet;
case OP_AS_ARRAY: return AsArray;
default:
return OtherArray;
}
}
return Other;
}
sort_kind context::get_sort_kind(const sort &s){
family_id fid = to_sort(s.raw())->get_family_id();
::decl_kind k = to_sort(s.raw())->get_decl_kind();
if (m().is_uninterp(to_sort(s.raw()))) {
return UninterpretedSort;
}
else if (fid == m_basic_fid && k == BOOL_SORT) {
return BoolSort;
}
else if (fid == m_arith_fid && k == INT_SORT) {
return IntSort;
}
else if (fid == m_arith_fid && k == REAL_SORT) {
return RealSort;
}
else if (fid == m_array_fid && k == ARRAY_SORT) {
return ArraySort;
}
else {
return UnknownSort;
}
}
expr func_decl::operator()(unsigned n, expr const * args) const {
std::vector< ::expr *> _args(n);
for(unsigned i = 0; i < n; i++)
_args[i] = to_expr(args[i].raw());
return ctx().cook(m().mk_app(to_func_decl(raw()),n,VEC2PTR(_args)));
}
int solver::get_num_decisions(){
::statistics st;
m_solver->collect_statistics(st);
std::ostringstream ss;
st.display(ss);
std::string stats = ss.str();
int pos = stats.find("decisions:");
if(pos < 0) return 0; // for some reason, decisions are not reported if there are none
pos += 10;
int end = stats.find('\n',pos);
std::string val = stats.substr(pos,end-pos);
return atoi(val.c_str());
}
void context::print_expr(std::ostream &s, const ast &e){
s << mk_pp(e.raw(), m());
}
expr expr::simplify(const params &_p) const {
::expr * a = to_expr(raw());
params_ref p = _p.get();
th_rewriter m_rw(m(), p);
expr_ref result(m());
m_rw(a, result);
return ctx().cook(result);
}
expr expr::simplify() const {
params p;
return simplify(p);
}
expr context::make_var(int idx, const sort &s){
::sort * a = to_sort(s.raw());
return cook(m().mk_var(idx,a));
}
expr expr::qe_lite() const {
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
qe(result,pf);
return ctx().cook(result);
}
expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
uint_set uis;
for(std::set<int>::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it)
uis.insert(*it);
qe(uis,index_of_bound,result);
return ctx().cook(result);
}
expr clone_quantifier(const expr &q, const expr &b){
return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
}
expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = thing->is_forall();
unsigned num_patterns = patterns.size();
std::vector< ::expr *> _patterns(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
_patterns[i] = to_expr(patterns[i].raw());
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, VEC2PTR(_patterns), to_expr(b.raw())));
}
expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = dk == Forall;
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw())));
}
void expr::get_patterns(std::vector<expr> &pats) const {
quantifier *thing = to_quantifier(raw());
unsigned num_patterns = thing->get_num_patterns();
:: expr * const *it = thing->get_patterns();
pats.resize(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
pats[i] = expr(ctx(),it[i]);
}
unsigned func_decl::arity() const {
return (to_func_decl(raw())->get_arity());
}
sort func_decl::domain(unsigned i) const {
return sort(ctx(),(to_func_decl(raw())->get_domain(i)));
}
sort func_decl::range() const {
return sort(ctx(),(to_func_decl(raw())->get_range()));
}
func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
std::vector < ::sort * > _domain(domain.size());
for(unsigned i = 0; i < domain.size(); i++)
_domain[i] = to_sort(domain[i].raw());
::func_decl* d = m().mk_fresh_func_decl(prefix,
_domain.size(),
VEC2PTR(_domain),
to_sort(range.raw()));
return func_decl(*this,d);
}
func_decl context::fresh_func_decl(char const * prefix, sort const & range){
::func_decl* d = m().mk_fresh_func_decl(prefix,
0,
nullptr,
to_sort(range.raw()));
return func_decl(*this,d);
}
#if 0
lbool interpolating_solver::interpolate(
const std::vector<expr> &assumptions,
std::vector<expr> &interpolants,
model &model,
Z3_literals &labels,
bool incremental)
{
Z3_model _model = 0;
Z3_literals _labels = 0;
Z3_lbool lb;
std::vector<Z3_ast> _assumptions(assumptions.size());
std::vector<Z3_ast> _interpolants(assumptions.size()-1);
for(unsigned i = 0; i < assumptions.size(); i++)
_assumptions[i] = assumptions[i];
std::vector<Z3_ast> _theory(theory.size());
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
lb = Z3_interpolate(
ctx(),
_assumptions.size(),
VEC2PTR(_assumptions),
0,
0,
VEC2PTR(_interpolants),
&_model,
&_labels,
incremental,
_theory.size(),
VEC2PTR(_theory));
if(lb == Z3_L_FALSE){
interpolants.resize(_interpolants.size());
for (unsigned i = 0; i < _interpolants.size(); ++i) {
interpolants[i] = expr(ctx(),_interpolants[i]);
}
}
if (_model) {
model = iz3wrapper::model(ctx(), _model);
}
if(_labels){
labels = _labels;
}
return lb;
}
#endif
static int linearize_assumptions(int num,
TermTree *assumptions,
std::vector<std::vector <expr> > &linear_assumptions,
std::vector<int> &parents){
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents);
// linear_assumptions[num].push_back(assumptions->getTerm());
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
parents[assumptions->getChildren()[i]->getNumber()] = num;
parents[num] = SHRT_MAX; // in case we have no parent
linear_assumptions[num].push_back(assumptions->getTerm());
std::vector<expr> &ts = assumptions->getTerms();
for(unsigned i = 0; i < ts.size(); i++)
linear_assumptions[num].push_back(ts[i]);
return num + 1;
}
static int unlinearize_interpolants(int num,
TermTree* assumptions,
const std::vector<expr> &interpolant,
TermTree * &tree_interpolant)
{
std::vector<TermTree *> chs(assumptions->getChildren().size());
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
num = unlinearize_interpolants(num, assumptions->getChildren()[i], interpolant,chs[i]);
expr f;
if(num < (int)interpolant.size()) // last interpolant is missing, presumed false
f = interpolant[num];
tree_interpolant = new TermTree(f,chs);
return num + 1;
}
lbool interpolating_solver::interpolate_tree(TermTree *assumptions,
TermTree *&interpolant,
model &model,
literals &labels,
bool incremental
)
{
int size = assumptions->number(0);
std::vector<std::vector<expr> > linear_assumptions(size);
std::vector<int> parents(size);
linearize_assumptions(0,assumptions,linear_assumptions,parents);
ptr_vector< ::ast> _interpolants(size-1);
vector<ptr_vector< ::ast> >_assumptions(size);
for(int i = 0; i < size; i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
_assumptions[i].push_back(linear_assumptions[i][j]);
::vector<int> _parents; _parents.resize(parents.size());
for(unsigned i = 0; i < parents.size(); i++)
_parents[i] = parents[i];
ptr_vector< ::ast> _theory(theory.size());
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
if(!incremental){
push();
for(unsigned i = 0; i < linear_assumptions.size(); i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
add(linear_assumptions[i][j]);
}
check_result res = unsat;
if(!m_solver->get_proof())
res = check();
if(res == unsat){
interpolation_options_struct opts;
if(weak_mode)
opts.set("weak","1");
::ast *proof = m_solver->get_proof();
try {
iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
}
// If there's an interpolation bug, throw a char *
// exception so duality can catch it and restart.
catch (const interpolation_failure &f) {
throw f.msg();
}
std::vector<expr> linearized_interpolants(_interpolants.size());
for(unsigned i = 0; i < _interpolants.size(); i++)
linearized_interpolants[i] = expr(ctx(),_interpolants[i]);
// since iz3interpolant returns interpolants with one ref count, we decrement here
for(unsigned i = 0; i < _interpolants.size(); i++)
m().dec_ref(_interpolants[i]);
unlinearize_interpolants(0,assumptions,linearized_interpolants,interpolant);
interpolant->setTerm(ctx().bool_val(false));
}
model_ref _m;
m_solver->get_model(_m);
model = Duality::model(ctx(),_m.get());
#if 0
if(_labels){
labels = _labels;
}
#endif
if(!incremental)
pop();
return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef);
}
void interpolating_solver::SetWeakInterpolants(bool weak){
weak_mode = weak;
}
void interpolating_solver::SetPrintToFile(const std::string &filename){
print_filename = filename;
}
void interpolating_solver::AssertInterpolationAxiom(const expr & t){
add(t);
theory.push_back(t);
}
void interpolating_solver::RemoveInterpolationAxiom(const expr & t){
// theory.remove(t);
}
const char *interpolating_solver::profile(){
// return Z3_interpolation_profile(ctx());
return "";
}
static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
if(memo.find(pf) != memo.end())return;
memo.insert(pf);
pfrule dk = pf.rule();
if(dk == PR_ASSERTED){
expr con = pf.conc();
assumps.push_back(con);
}
else {
unsigned nprems = pf.num_prems();
for(unsigned i = 0; i < nprems; i++){
proof arg = pf.prem(i);
get_assumptions_rec(memo,arg,assumps);
}
}
}
void proof::get_assumptions(std::vector<expr> &assumps){
stl_ext::hash_set<ast> memo;
get_assumptions_rec(memo,*this,assumps);
}
void ast::show() const{
std::cout << mk_pp(raw(), m()) << std::endl;
}
void model::show() const {
model_smt2_pp(std::cout, m(), *m_model, 0);
std::cout << std::endl;
}
void model::show_hash() const {
std::ostringstream ss;
model_smt2_pp(ss, m(), *m_model, 0);
hash_space::hash<std::string> hasher;
unsigned h = hasher(ss.str());
std::cout << "model hash: " << h << "\n";
}
void solver::show() {
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
}
void solver::print(const char *filename) {
std::ofstream f(filename);
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(f, m_solver->get_assertion(n-1));
}
void solver::show_assertion_ids() {
#if 0
unsigned n = m_solver->get_num_assertions();
std::cerr << "assertion ids: ";
for (unsigned i = 0; i < n-1; ++i)
std::cerr << " " << m_solver->get_assertion(i)->get_id();
std::cerr << "\n";
#else
unsigned n = m_solver->get_num_assertions();
std::cerr << "assertion ids hash: ";
unsigned h = 0;
for (unsigned i = 0; i < n-1; ++i)
h += m_solver->get_assertion(i)->get_id();
std::cerr << h << "\n";
#endif
}
void include_ast_show(ast &a){
a.show();
}
void include_model_show(model &a){
a.show();
}
void show_ast(::ast *a, ast_manager &m) {
std::cout << mk_pp(a, m) << std::endl;
}
bool expr::is_label (bool &pos,std::vector<symbol> &names) const {
buffer< ::symbol> _names;
bool res = m().is_label(to_expr(raw()),pos,_names);
if(res)
for(unsigned i = 0; i < _names.size(); i++)
names.push_back(symbol(ctx(),_names[i]));
return res;
}
double current_time()
{
static stopwatch sw;
static bool started = false;
if(!started){
sw.start();
started = true;
}
return sw.get_current_seconds();
}
}

File diff suppressed because it is too large Load diff

View file

@ -1,18 +0,0 @@
z3_add_component(interp
SOURCES
iz3base.cpp
iz3checker.cpp
iz3interp.cpp
iz3mgr.cpp
iz3pp.cpp
iz3profiling.cpp
iz3proof.cpp
iz3proof_itp.cpp
iz3scopes.cpp
iz3translate.cpp
iz3translate_direct.cpp
COMPONENT_DEPENDENCIES
solver
PYG_FILES
interp_params.pyg
)

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