mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'develop' into regex-develop

Browse source
This commit is contained in:
Murphy Berzish 2018-01-03 16:12:33 -05:00
parent 0f20944aeb a5180edc76
commit 09dc5cd0f8
118 changed files with 2238 additions and 5701 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
CMakeLists.txt
View file

@ -33,7 +33,7 @@ endif()
# Project version
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 5)
set(Z3_VERSION_MINOR 6)
set(Z3_VERSION_PATCH 1)
set(Z3_VERSION_TWEAK 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
@ -257,6 +257,46 @@ list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
"${CMAKE_BINARY_DIR}/src"
"${CMAKE_SOURCE_DIR}/src"
)
################################################################################
# Linux specific configuration
################################################################################
if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
# Try to detect if it is necessary to link against librt.
# Note that glibc < 2.17 required librt to be linked to use clock_gettime()
# and friends.
set(CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE
"
#include <time.h>
int main() {
timespec res;
int result = clock_gettime(CLOCK_REALTIME, &res);
return result == 0;
}
"
)
check_cxx_source_compiles(
"${CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE}"
CLOCK_GETTIME_NO_REQUIRE_LIBRT
)
if (NOT CLOCK_GETTIME_NO_REQUIRE_LIBRT)
# Try again with librt
message(STATUS "Failed to link against clock_gettime(), trying with librt")
set(CMAKE_REQUIRED_LIBRARIES_OLD "${CMAKE_REQUIRED_LIBRARIES}")
set(CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES} rt")
check_cxx_source_compiles(
"${CLOCK_GETTIME_REQUIRES_LIBRT_TEST_CODE}"
CLOCK_GETTIME_REQUIRES_LIBRT
)
set(CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES_OLD}")
if (CLOCK_GETTIME_REQUIRES_LIBRT)
list(APPEND Z3_DEPENDENT_LIBS "rt")
else()
message(FATAL_ERROR "Failed to link against clock_gettime()")
endif()
endif()
endif()
################################################################################
# GNU multiple precision library support
################################################################################

4
README-CMake.md
View file

@ -5,7 +5,7 @@ of the project written in the ``CMakeLists.txt`` files and emits a build
system for that project of your choice using one of CMake's "generators".
This allows CMake to support many different platforms and build tools.
You can run ``cmake --help`` to see the list of supported "generators"
on your platform. Example generators include "UNIX Makfiles" and "Visual Studio
on your platform. Example generators include "UNIX Makefiles" and "Visual Studio
12 2013".
## Getting started
@ -44,7 +44,7 @@ cmake -G "Unix Makefiles" ../
make -j4 # Replace 4 with an appropriate number
```
Note that on some platforms "Unix Makesfiles" is the default generator so on those
Note that on some platforms "Unix Makefiles" is the default generator so on those
platforms you don't need to pass ``-G "Unix Makefiles"`` command line option to
``cmake``.

18
RELEASE_NOTES
View file

@ -1,7 +1,12 @@
RELEASE NOTES
Version 4.5.x
Version 4.6.0
=============
- New requirements:
- C++11 capable compiler to build Z3.
- C++ API now requires C++11 or newer.
- New features (including):
- A new string solver from University of Waterloo
- A new linear real arithmetic solver
@ -10,6 +15,10 @@ Version 4.5.x
issuing the command (get-objectives). Pareto front objectives are accessed by
issuing multiple (check-sat) calls until it returns unsat.
- Removed features:
- Removed support for SMT-LIB 1.x
Version 4.5.0
=============
@ -45,10 +54,9 @@ Version 4.5.0
over compound formulas, introduce a fresh predicate whose
arguments are the relevant free variables in the formula and add a rule
that uses the fresh predicate in the head and formula in the body.
- minimization of unsat cores is avaialble as an option for the SAT and SMT cores.
- Minimization of unsat cores is available as an option for the SAT and SMT cores.
By setting smt.core.minimize=true resp. sat.core.minimize=true
cores produced by these modules are minimized.
cores produced by these modules are minimized.
- A multitude of bugs has been fixed.
@ -704,7 +712,7 @@ The following bugs are fixed in this release:
bvshl when using a shift amount that evaluates to the length
of the bit-vector. Thanks to Trevor Hansen and Robert Brummayer.
- Incorrect NNF conversion in linear quantifier elimniation routines.
- Incorrect NNF conversion in linear quantifier elimination routines.
Thanks to Josh Berdine.
- Missing constant folding of extraction for large bit-vectors.

2
cmake/Z3Config.cmake.in
View file

@ -2,7 +2,7 @@
# @AUTO_GEN_MSG@
#
# This file is intended to be consumed by clients who wish to use Z3 from CMake.
# It can be use by doing `find_package(Z3 config)` from within a
# It can be used by doing `find_package(Z3 config)` from within a
# `CMakeLists.txt` file. If CMake doesn't find this package automatically you
# can give it a hint by passing `-DZ3_DIR=<path>` to the CMake invocation where
# `<path>` is the path to the directory containing this file.

2
contrib/suppressions/sanitizers/README.md
View file

@ -1,4 +1,4 @@
# Sanitizer supression files
# Sanitizer suppression files
This directory contains files used to suppress
ASan/LSan/UBSan warnings/errors.

7
doc/mk_api_doc.py
View file

@ -226,12 +226,14 @@ try:
website_dox_substitutions = {}
bullet_point_prefix='\n - '
if Z3PY_ENABLED:
print("Python documentation enabled")
website_dox_substitutions['PYTHON_API'] = (
'{prefix}<a class="el" href="namespacez3py.html">Python API</a> '
'(also available in <a class="el" href="z3.html">pydoc format</a>)'
).format(
prefix=bullet_point_prefix)
else:
print("Python documentation disabled")
website_dox_substitutions['PYTHON_API'] = ''
if DOTNET_ENABLED:
website_dox_substitutions['DOTNET_API'] = (
@ -250,7 +252,7 @@ try:
website_dox_substitutions['JAVA_API'] = ''
if ML_ENABLED:
website_dox_substitutions['OCAML_API'] = (
'<a class="el" href="ml/index.html">ML/OCaml API</a>'
'{prefix}<a class="el" href="ml/index.html">ML/OCaml API</a>'
).format(
prefix=bullet_point_prefix)
else:
@ -316,7 +318,7 @@ try:
if ML_ENABLED:
ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml')
mk_dir(ml_output_dir)
if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0:
if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '%s/api/ml/z3enums.mli' % BUILD_DIR, '%s/api/ml/z3.mli' % BUILD_DIR]) != 0:
print("ERROR: ocamldoc failed.")
exit(1)
print("Generated ML/OCaml documentation.")
@ -326,3 +328,4 @@ except Exception:
exctype, value = sys.exc_info()[:2]
print("ERROR: failed to generate documentation: %s" % value)
exit(1)

16
examples/c++/CMakeLists.txt
View file

@ -13,6 +13,22 @@ find_package(Z3
# use this option.
NO_DEFAULT_PATH
)
################################################################################
# Z3 C++ API bindings require C++11
################################################################################
if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
# Legacy CMake support
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11")
else()
message(FATAL_ERROR "Setting C++ version to C++11 not supported for \"${CMAKE_CXX_COMPILER_ID}\"")
endif()
else ()
set(CMAKE_CXX_STANDARD 11)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
endif ()
message(STATUS "Z3_FOUND: ${Z3_FOUND}")
message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
message(STATUS "Z3_DIR: ${Z3_DIR}")

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

@ -1138,8 +1138,11 @@ static void parse_example() {
decls.push_back(c.function("a", 0, 0, B));
expr 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))");
}
int main() {
try {

91
examples/c/test_capi.c
View file

@ -395,11 +395,10 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
t_name = Z3_mk_string_symbol(ctx, "T");
Z3_parse_smtlib_string(ctx,
"(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))",
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);
q = Z3_get_smtlib_formula(ctx, 0);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
Z3_solver_assert(ctx, s, q);
}
@ -1547,7 +1546,7 @@ void two_contexts_example1()
}
/**
\brief Demonstrates how error codes can be read insted of registering an error handler.
\brief Demonstrates how error codes can be read instead of registering an error handler.
*/
void error_code_example1()
{
@ -1632,35 +1631,6 @@ void error_code_example2() {
}
}
/**
\brief Demonstrates how to use the SMTLIB parser.
*/
void parser_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
unsigned i, num_formulas;
printf("\nparser_example1\n");
LOG_MSG("parser_example1");
Z3_parse_smtlib_string(ctx,
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
0, 0, 0,
0, 0, 0);
num_formulas = Z3_get_smtlib_num_formulas(ctx);
for (i = 0; i < num_formulas; i++) {
Z3_ast f = Z3_get_smtlib_formula(ctx, i);
printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
Z3_solver_assert(ctx, s, f);
}
check(ctx, s, Z3_L_TRUE);
del_solver(ctx, s);
Z3_del_context(ctx);
}
/**
\brief Demonstrates how to initialize the parser symbol table.
@ -1690,12 +1660,11 @@ void parser_example2()
names[0] = Z3_mk_string_symbol(ctx, "a");
names[1] = Z3_mk_string_symbol(ctx, "b");
Z3_parse_smtlib_string(ctx,
"(benchmark tst :formula (> a b))",
f = Z3_parse_smtlib2_string(ctx,
"(assert (> a b))",
0, 0, 0,
/* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */
2, names, decls);
f = Z3_get_smtlib_formula(ctx, 0);
printf("formula: %s\n", Z3_ast_to_string(ctx, f));
Z3_solver_assert(ctx, s, f);
check(ctx, s, Z3_L_TRUE);
@ -1737,11 +1706,10 @@ void parser_example3()
assert_comm_axiom(ctx, s, g);
Z3_parse_smtlib_string(ctx,
"(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))",
thm = Z3_parse_smtlib2_string(ctx,
"(assert (forall ((x Int) (y Int)) (=> (= x y) (= (g x 0) (g 0 y)))))",
0, 0, 0,
1, &g_name, &g);
thm = Z3_get_smtlib_formula(ctx, 0);
printf("formula: %s\n", Z3_ast_to_string(ctx, thm));
prove(ctx, s, thm, Z3_TRUE);
@ -1749,41 +1717,6 @@ void parser_example3()
Z3_del_context(ctx);
}
/**
\brief Display the declarations, assumptions and formulas in a SMT-LIB string.
*/
void parser_example4()
{
Z3_context ctx;
unsigned i, num_decls, num_assumptions, num_formulas;
printf("\nparser_example4\n");
LOG_MSG("parser_example4");
ctx = mk_context();
Z3_parse_smtlib_string(ctx,
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
0, 0, 0,
0, 0, 0);
num_decls = Z3_get_smtlib_num_decls(ctx);
for (i = 0; i < num_decls; i++) {
Z3_func_decl d = Z3_get_smtlib_decl(ctx, i);
printf("declaration %d: %s\n", i, Z3_func_decl_to_string(ctx, d));
}
num_assumptions = Z3_get_smtlib_num_assumptions(ctx);
for (i = 0; i < num_assumptions; i++) {
Z3_ast a = Z3_get_smtlib_assumption(ctx, i);
printf("assumption %d: %s\n", i, Z3_ast_to_string(ctx, a));
}
num_formulas = Z3_get_smtlib_num_formulas(ctx);
for (i = 0; i < num_formulas; i++) {
Z3_ast f = Z3_get_smtlib_formula(ctx, i);
printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
}
Z3_del_context(ctx);
}
/**
\brief Demonstrates how to handle parser errors using Z3 error handling support.
*/
@ -1802,9 +1735,9 @@ void parser_example5() {
s = mk_solver(ctx);
Z3_del_config(cfg);
Z3_parse_smtlib_string(ctx,
Z3_parse_smtlib2_string(ctx,
/* the following string has a parsing error: missing parenthesis */
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
"(declare-const x Int) declare-const y Int) (assert (and (> x y) (> x 0)))",
0, 0, 0,
0, 0, 0);
e = Z3_get_error_code(ctx);
@ -1817,7 +1750,7 @@ void parser_example5() {
err:
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e));
if (ctx != NULL) {
printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx));
printf("Error message: '%s'.\n",Z3_get_parser_error(ctx));
del_solver(ctx, s);
Z3_del_context(ctx);
}
@ -2600,7 +2533,7 @@ void reference_counter_example() {
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "model", "true");
// Create a Z3 context where the user is reponsible for managing
// Create a Z3 context where the user is responsible for managing
// Z3_ast reference counters.
ctx = Z3_mk_context_rc(cfg);
Z3_del_config(cfg);
@ -3065,10 +2998,8 @@ int main() {
two_contexts_example1();
error_code_example1();
error_code_example2();
parser_example1();
parser_example2();
parser_example3();
parser_example4();
parser_example5();
numeral_example();
ite_example();

68
examples/dotnet/Program.cs
View file

@ -173,10 +173,9 @@ namespace test_mapi
throw new Exception("function must be binary, and argument types must be equal to return type");
}
string bench = string.Format("(benchmark comm :formula (forall (x {0}) (y {1}) (= ({2} x y) ({3} y x))))",
string bench = string.Format("(assert (forall ((x {0}) (y {1})) (= ({2} x y) ({3} y x))))",
t.Name, t.Name, f.Name, f.Name);
ctx.ParseSMTLIBString(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f });
return ctx.SMTLIBFormulas[0];
return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f });
}
/// <summary>
@ -623,7 +622,7 @@ namespace test_mapi
Console.WriteLine("{0}", q1);
}
// Quantifier with de-Brujin indices.
// Quantifier with de-Bruijn indices.
{
Expr x = ctx.MkBound(1, ctx.IntSort);
Expr y = ctx.MkBound(0, ctx.IntSort);
@ -965,21 +964,6 @@ namespace test_mapi
}
}
/// <summary>
/// Shows how to read an SMT1 file.
/// </summary>
static void SMT1FileTest(string filename)
{
Console.Write("SMT File test ");
using (Context ctx = new Context(new Dictionary<string, string>() { { "MODEL", "true" } }))
{
ctx.ParseSMTLIBFile(filename);
BoolExpr a = ctx.MkAnd(ctx.SMTLIBFormulas);
Console.WriteLine("read formula: " + a);
}
}
/// <summary>
/// Shows how to read an SMT2 file.
@ -1399,11 +1383,10 @@ namespace test_mapi
{
Console.WriteLine("ParserExample1");
ctx.ParseSMTLIBString("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
foreach (BoolExpr f in ctx.SMTLIBFormulas)
Console.WriteLine("formula {0}", f);
var fml = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
Console.WriteLine("formula {0}", fml);
Model m = Check(ctx, ctx.MkAnd(ctx.SMTLIBFormulas), Status.SATISFIABLE);
Model m = Check(ctx, fml, Status.SATISFIABLE);
}
/// <summary>
@ -1412,15 +1395,11 @@ namespace test_mapi
public static void ParserExample2(Context ctx)
{
Console.WriteLine("ParserExample2");
Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") };
FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort());
FuncDecl b = ctx.MkConstDecl(declNames[1], ctx.MkIntSort());
FuncDecl[] decls = new FuncDecl[] { a, b };
ctx.ParseSMTLIBString("(benchmark tst :formula (> a b))",
null, null, declNames, decls);
BoolExpr f = ctx.SMTLIBFormulas[0];
BoolExpr f = ctx.ParseSMTLIB2String("(assert (> a b))", null, null, declNames, decls);
Console.WriteLine("formula: {0}", f);
Check(ctx, f, Status.SATISFIABLE);
}
@ -1438,39 +1417,15 @@ namespace test_mapi
BoolExpr ca = CommAxiom(ctx, g);
ctx.ParseSMTLIBString("(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))",
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 });
BoolExpr thm = ctx.SMTLIBFormulas[0];
Console.WriteLine("formula: {0}", thm);
Prove(ctx, thm, false, ca);
}
/// <summary>
/// Display the declarations, assumptions and formulas in a SMT-LIB string.
/// </summary>
public static void ParserExample4(Context ctx)
{
Console.WriteLine("ParserExample4");
ctx.ParseSMTLIBString
("(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))");
foreach (var decl in ctx.SMTLIBDecls)
{
Console.WriteLine("Declaration: {0}", decl);
}
foreach (var f in ctx.SMTLIBAssumptions)
{
Console.WriteLine("Assumption: {0}", f);
}
foreach (var f in ctx.SMTLIBFormulas)
{
Console.WriteLine("Formula: {0}", f);
}
}
/// <summary>
/// Demonstrates how to handle parser errors using Z3 error handling support.
/// </summary>
@ -1481,9 +1436,9 @@ namespace test_mapi
try
{
ctx.ParseSMTLIBString(
ctx.ParseSMTLIB2String(
/* the following string has a parsing error: missing parenthesis */
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))");
"(declare-const x Int (declare-const y Int)) (assert (> x y))");
}
catch (Z3Exception e)
{
@ -1990,7 +1945,7 @@ namespace test_mapi
BoolExpr p2 = ctx.MkBoolConst("P2");
BoolExpr p3 = ctx.MkBoolConst("P3");
BoolExpr p4 = ctx.MkBoolConst("P4");
BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
Expr[] assumptions = new Expr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
@ -2213,7 +2168,6 @@ namespace test_mapi
BitvectorExample2(ctx);
ParserExample1(ctx);
ParserExample2(ctx);
ParserExample4(ctx);
ParserExample5(ctx);
ITEExample(ctx);
EvalExample1(ctx);

67
examples/java/JavaExample.java
View file

@ -170,10 +170,9 @@ class JavaExample
String bench = "(benchmark comm :formula (forall (x " + t.getName()
+ ") (y " + t.getName() + ") (= (" + f.getName() + " x y) ("
+ f.getName() + " y x))))";
ctx.parseSMTLIBString(bench, new Symbol[] { t.getName() },
return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
new Sort[] { t }, new Symbol[] { f.getName() },
new FuncDecl[] { f });
return ctx.getSMTLIBFormulas()[0];
}
// / "Hello world" example: create a Z3 logical context, and delete it.
@ -661,7 +660,7 @@ class JavaExample
System.out.println(q1);
}
// Quantifier with de-Brujin indices.
// Quantifier with de-Bruijn indices.
{
Expr x = ctx.mkBound(1, ctx.getIntSort());
Expr y = ctx.mkBound(0, ctx.getIntSort());
@ -1028,21 +1027,6 @@ class JavaExample
}
}
// / Shows how to read an SMT1 file.
void smt1FileTest(String filename)
{
System.out.print("SMT File test ");
{
HashMap<String, String> cfg = new HashMap<String, String>();
Context ctx = new Context(cfg);
ctx.parseSMTLIBFile(filename, null, null, null, null);
BoolExpr a = ctx.mkAnd(ctx.getSMTLIBFormulas());
System.out.println("read formula: " + a);
}
}
// / Shows how to read an SMT2 file.
@ -1459,15 +1443,13 @@ class JavaExample
System.out.println("ParserExample1");
Log.append("ParserExample1");
ctx.parseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
BoolExpr f = ctx.parseSMTLIB2String(
"(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
null, null, null, null);
for (BoolExpr f : ctx.getSMTLIBFormulas())
System.out.println("formula " + f);
System.out.println("formula " + f);
@SuppressWarnings("unused")
Model m = check(ctx, ctx.mkAnd(ctx.getSMTLIBFormulas()),
Status.SATISFIABLE);
Model m = check(ctx, f, Status.SATISFIABLE);
}
// / Demonstrates how to initialize the parser symbol table.
@ -1482,9 +1464,8 @@ class JavaExample
FuncDecl b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort());
FuncDecl[] decls = new FuncDecl[] { a, b };
ctx.parseSMTLIBString("(benchmark tst :formula (> a b))", null, null,
BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
declNames, decls);
BoolExpr f = ctx.getSMTLIBFormulas()[0];
System.out.println("formula: " + f);
check(ctx, f, Status.SATISFIABLE);
}
@ -1502,39 +1483,14 @@ class JavaExample
BoolExpr ca = commAxiom(ctx, g);
ctx.parseSMTLIBString(
"(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))",
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 });
BoolExpr thm = ctx.getSMTLIBFormulas()[0];
System.out.println("formula: " + thm);
prove(ctx, thm, false, ca);
}
// / Display the declarations, assumptions and formulas in a SMT-LIB string.
public void parserExample4(Context ctx)
{
System.out.println("ParserExample4");
Log.append("ParserExample4");
ctx.parseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
null, null, null, null);
for (FuncDecl decl : ctx.getSMTLIBDecls())
{
System.out.println("Declaration: " + decl);
}
for (BoolExpr f : ctx.getSMTLIBAssumptions())
{
System.out.println("Assumption: " + f);
}
for (BoolExpr f : ctx.getSMTLIBFormulas())
{
System.out.println("Formula: " + f);
}
}
// / Demonstrates how to handle parser errors using Z3 error handling
// support.
@ -1546,12 +1502,12 @@ class JavaExample
try
{
ctx.parseSMTLIBString(
ctx.parseSMTLIB2String(
/*
* the following string has a parsing error: missing
* parenthesis
*/
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
"(declare-const x Int (declare-const y Int)) (assert (> x y))",
null, null, null, null);
} catch (Z3Exception e)
{
@ -2341,7 +2297,6 @@ class JavaExample
p.bitvectorExample2(ctx);
p.parserExample1(ctx);
p.parserExample2(ctx);
p.parserExample4(ctx);
p.parserExample5(ctx);
p.iteExample(ctx);
p.evalExample1(ctx);

2
examples/maxsat/README
View file

@ -9,4 +9,4 @@ On OSX and Linux, you must install z3 first using
sudo make install
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library.
This directory contains a test file (ex.smt) that can be use as input for the maxsat test application.
This directory contains a test file (ex.smt) that can be used as input for the maxsat test application.

20
examples/maxsat/ex.smt
View file

@ -1,11 +1,11 @@
(benchmark ex
:logic AUFLIA
:extrafuns ((x Int) (y Int) (z Int))
:assumption (> x 0)
:assumption (<= x -1)
:assumption (or (> x 0) (< y 1))
:assumption (> y 2)
:assumption (> y 3)
:assumption (<= y -1)
:formula (= z (+ x y)))
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert-soft (> x 0))
(assert-soft (<= x -1))
(assert-soft (or (> x 0) (< y 1)))
(assert-soft (> y 2))
(assert-soft (> y 3))
(assert-soft (<= y -1))
(assert (= z (+ x y)))

65
examples/maxsat/maxsat.c
View file

@ -116,41 +116,6 @@ Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2)
}
/**
\brief Get hard constraints from a SMT-LIB file. We assume hard constraints
are formulas preceeded with the keyword :formula.
Return an array containing all formulas read by the last Z3_parse_smtlib_file invocation.
It will store the number of formulas in num_cnstrs.
*/
Z3_ast * get_hard_constraints(Z3_context ctx, unsigned * num_cnstrs)
{
Z3_ast * result;
unsigned i;
*num_cnstrs = Z3_get_smtlib_num_formulas(ctx);
result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs));
for (i = 0; i < *num_cnstrs; i++) {
result[i] = Z3_get_smtlib_formula(ctx, i);
}
return result;
}
/**
\brief Get soft constraints from a SMT-LIB file. We assume soft constraints
are formulas preceeded with the keyword :assumption.
Return an array containing all assumptions read by the last Z3_parse_smtlib_file invocation.
It will store the number of formulas in num_cnstrs.
*/
Z3_ast * get_soft_constraints(Z3_context ctx, unsigned * num_cnstrs)
{
Z3_ast * result;
unsigned i;
*num_cnstrs = Z3_get_smtlib_num_assumptions(ctx);
result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs));
for (i = 0; i < *num_cnstrs; i++) {
result[i] = Z3_get_smtlib_assumption(ctx, i);
}
return result;
}
/**
\brief Free the given array of cnstrs that was allocated using get_hard_constraints or get_soft_constraints.
@ -610,14 +575,37 @@ int smtlib_maxsat(char * file_name, int approach)
{
Z3_context ctx;
Z3_solver s;
unsigned i;
Z3_optimize opt;
unsigned num_hard_cnstrs, num_soft_cnstrs;
Z3_ast * hard_cnstrs, * soft_cnstrs;
Z3_ast_vector hard, objs;
Z3_app soft;
unsigned result = 0;
ctx = mk_context();
s = mk_solver(ctx);
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
Z3_optimize_from_file(ctx, opt, file_name);
hard = Z3_optimize_get_assertions(ctx, opt);
Z3_ast_vector_inc_ref(ctx, hard);
num_hard_cnstrs = Z3_ast_vector_size(ctx, hard);
hard_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_hard_cnstrs));
for (i = 0; i < num_hard_cnstrs; i++) {
hard_cnstrs[i] = Z3_ast_vector_get(ctx, hard, i);
}
objs = Z3_optimize_get_objectives(ctx, opt);
Z3_ast_vector_inc_ref(ctx, objs);
// soft constraints are stored in a single objective which is a sum
// of if-then-else expressions.
soft = Z3_to_app(ctx, Z3_ast_vector_get(ctx, objs, 0));
num_soft_cnstrs = Z3_get_app_num_args(ctx, soft);
soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs));
for (i = 0; i < num_soft_cnstrs; ++i) {
soft_cnstrs[i] = Z3_get_app_arg(ctx, Z3_to_app(ctx, Z3_get_app_arg(ctx, soft, i)), 0);
}
switch (approach) {
case NAIVE_MAXSAT:
result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
@ -633,6 +621,7 @@ int smtlib_maxsat(char * file_name, int approach)
free_cnstr_array(hard_cnstrs);
free_cnstr_array(soft_cnstrs);
Z3_solver_dec_ref(ctx, s);
Z3_optimize_dec_ref(ctx, opt);
return result;
}

5
scripts/mk_project.py
View file

@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 5, 1, 0)
set_version(4, 6, 1, 0)
add_lib('util', [])
add_lib('lp', ['util'], 'util/lp')
add_lib('polynomial', ['util'], 'math/polynomial')
@ -75,10 +75,9 @@ def init_project_def():
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('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('smtparser', ['portfolio'], 'parsers/smt')
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', 'smtparser', 'realclosure', 'interp', 'opt'],
add_lib('api', ['portfolio', 'realclosure', 'interp', '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)

2
scripts/mk_util.py
View file

@ -1990,7 +1990,7 @@ class MLComponent(Component):
out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
out.write('\t%s -linkall -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
out.write('\n')
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))

1
src/CMakeLists.txt
View file

@ -98,7 +98,6 @@ add_subdirectory(sat/sat_solver)
add_subdirectory(tactic/smtlogics)
add_subdirectory(tactic/fpa)
add_subdirectory(tactic/portfolio)
add_subdirectory(parsers/smt)
add_subdirectory(opt)
add_subdirectory(api)
add_subdirectory(api/dll)

1
src/api/CMakeLists.txt
View file

@ -71,5 +71,4 @@ z3_add_component(api
opt
portfolio
realclosure
smtparser
)

30
src/api/api_ast.cpp
View file

@ -832,30 +832,9 @@ extern "C" {
case Z3_PRINT_LOW_LEVEL:
buffer << mk_ll_pp(to_ast(a), mk_c(c)->m());
break;
case Z3_PRINT_SMTLIB_COMPLIANT: {
ast_smt_pp pp(mk_c(c)->m());
pp_params params;
pp.set_simplify_implies(params.simplify_implies());
ast* a1 = to_ast(a);
pp.set_logic(mk_c(c)->fparams().m_logic);
if (!is_expr(a1)) {
buffer << mk_pp(a1, mk_c(c)->m());
break;
}
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB_COMPLIANT) {
pp.display_expr(buffer, to_expr(a1));
break;
}
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
pp.display_expr_smt2(buffer, to_expr(a1));
break;
}
break;
}
case Z3_PRINT_SMTLIB2_COMPLIANT: {
case Z3_PRINT_SMTLIB2_COMPLIANT:
buffer << mk_ismt2_pp(to_ast(a), mk_c(c)->m());
break;
}
default:
UNREACHABLE();
}
@ -893,12 +872,7 @@ extern "C" {
for (unsigned i = 0; i < num_assumptions; ++i) {
pp.add_assumption(to_expr(assumptions[i]));
}
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
pp.display_smt2(buffer, to_expr(formula));
}
else {
pp.display(buffer, to_expr(formula));
}
pp.display_smt2(buffer, to_expr(formula));
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}

42
src/api/api_context.cpp
View file

@ -19,7 +19,6 @@ Revision History:
--*/
#include<typeinfo>
#include "api/api_context.h"
#include "parsers/smt/smtparser.h"
#include "util/version.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
@ -89,8 +88,6 @@ namespace api {
m_print_mode = Z3_PRINT_SMTLIB_FULL;
m_searching = false;
m_smtlib_parser = 0;
m_smtlib_parser_has_decls = false;
m_interruptable = 0;
m_error_handler = &default_error_handler;
@ -111,13 +108,13 @@ namespace api {
context::~context() {
reset_parser();
m_last_obj = 0;
u_map<api::object*>::iterator it = m_allocated_objects.begin();
while (it != m_allocated_objects.end()) {
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*it->m_value).name()););
api::object* val = it->m_value;
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*val).name()););
m_allocated_objects.remove(it->m_key);
dealloc(it->m_value);
dealloc(val);
it = m_allocated_objects.begin();
}
}
@ -304,39 +301,6 @@ namespace api {
}
}
// ------------------------
//
// Parser interface for backward compatibility
//
// ------------------------
void context::reset_parser() {
if (m_smtlib_parser) {
dealloc(m_smtlib_parser);
m_smtlib_parser = 0;
m_smtlib_parser_has_decls = false;
m_smtlib_parser_decls.reset();
m_smtlib_parser_sorts.reset();
}
SASSERT(!m_smtlib_parser_has_decls);
}
void context::extract_smtlib_parser_decls() {
if (m_smtlib_parser) {
if (!m_smtlib_parser_has_decls) {
smtlib::symtable * table = m_smtlib_parser->get_benchmark()->get_symtable();
table->get_func_decls(m_smtlib_parser_decls);
table->get_sorts(m_smtlib_parser_sorts);
m_smtlib_parser_has_decls = true;
}
}
else {
m_smtlib_parser_decls.reset();
m_smtlib_parser_sorts.reset();
}
}
// ------------------------
//
// RCF manager

12
src/api/api_context.h
View file

@ -220,19 +220,11 @@ namespace api {
// ------------------------
//
// Parser interface for backward compatibility
// Parser interface
//
// ------------------------
// TODO: move to a "parser" object visible to the external world.
std::string m_smtlib_error_buffer;
smtlib::parser * m_smtlib_parser;
bool m_smtlib_parser_has_decls;
ptr_vector<func_decl> m_smtlib_parser_decls;
ptr_vector<sort> m_smtlib_parser_sorts;
void reset_parser();
void extract_smtlib_parser_decls();
std::string m_parser_error_buffer;
};

30
src/api/api_interp.cpp
View file

@ -510,31 +510,15 @@ extern "C" {
read_error.clear();
try {
std::string foo(filename);
if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){
Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
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);
}
else {
Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0);
int numa = Z3_get_smtlib_num_assumptions(ctx);
int numf = Z3_get_smtlib_num_formulas(ctx);
int num = numa + numf;
assertions.resize(num);
for (int j = 0; j < num; j++){
if (j < numa)
assertions[j] = Z3_get_smtlib_assumption(ctx, j);
else
assertions[j] = Z3_get_smtlib_formula(ctx, j - numa);
}
}
Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
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_smtlib_error(ctx);
read_error << "SMTLIB parse error: " << Z3_get_parser_error(ctx);
read_msg = read_error.str();
*error = read_msg.c_str();
return false;

12
src/api/api_model.cpp
View file

@ -212,6 +212,18 @@ extern "C" {
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context target) {
Z3_TRY;
LOG_Z3_model_translate(c, m, target);
RESET_ERROR_CODE();
Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
dst->m_model = to_model_ref(m)->translate(tr);
mk_c(target)->save_object(dst);
RETURN_Z3(of_model(dst));
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a) {
Z3_TRY;

54
src/api/api_opt.cpp
View file

@ -16,17 +16,19 @@ Revision History:
--*/
#include<iostream>
#include "util/cancel_eh.h"
#include "util/file_path.h"
#include "util/scoped_timer.h"
#include "parsers/smt2/smt2parser.h"
#include "opt/opt_context.h"
#include "opt/opt_cmds.h"
#include "opt/opt_parse.h"
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_stats.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "api/api_model.h"
#include "opt/opt_context.h"
#include "opt/opt_cmds.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "parsers/smt2/smt2parser.h"
#include "api/api_ast_vector.h"
extern "C" {
@ -281,16 +283,40 @@ extern "C" {
static void Z3_optimize_from_stream(
Z3_context c,
Z3_optimize opt,
std::istream& s) {
ast_manager& m = mk_c(c)->m();
std::istream& s,
char const* ext) {
ast_manager& m = mk_c(c)->m();
if (ext && std::string("opb") == ext) {
unsigned_vector h;
parse_opb(*to_optimize_ptr(opt), s, h);
return;
}
if (ext && std::string("wcnf") == ext) {
unsigned_vector h;
parse_wcnf(*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;
ctx->set_regular_stream(errstrm);
ctx->set_ignore_check(true);
if (!parse_smt2_commands(*ctx.get(), s)) {
try {
if (!parse_smt2_commands(*ctx.get(), s)) {
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
}
catch (z3_exception& e) {
errstrm << e.msg();
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
}
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {
@ -298,6 +324,8 @@ extern "C" {
}
}
void Z3_API Z3_optimize_from_string(
Z3_context c,
Z3_optimize d,
@ -306,7 +334,7 @@ extern "C" {
//LOG_Z3_optimize_from_string(c, d, s);
std::string str(s);
std::istringstream is(str);
Z3_optimize_from_stream(c, d, is);
Z3_optimize_from_stream(c, d, is, nullptr);
Z3_CATCH;
}
@ -322,7 +350,7 @@ extern "C" {
strm << "Could not open file " << s;
throw default_exception(strm.str());
}
Z3_optimize_from_stream(c, d, is);
Z3_optimize_from_stream(c, d, is, get_extension(s));
Z3_CATCH;
}
@ -335,8 +363,8 @@ extern "C" {
mk_c(c)->save_object(v);
expr_ref_vector hard(mk_c(c)->m());
to_optimize_ptr(o)->get_hard_constraints(hard);
for (unsigned i = 0; i < hard.size(); i++) {
v->m_ast_vector.push_back(hard[i].get());
for (expr* h : hard) {
v->m_ast_vector.push_back(h);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);

244
src/api/api_parsers.cpp
View file

@ -22,232 +22,16 @@ Revision History:
#include "api/api_util.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
#include "parsers/smt/smtparser.h"
#include "solver/solver_na2as.h"
extern "C" {
void init_smtlib_parser(Z3_context c,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const types[],
unsigned num_decls,
Z3_symbol const decl_names[],
Z3_func_decl const decls[]) {
mk_c(c)->reset_parser();
mk_c(c)->m_smtlib_parser = smtlib::parser::create(mk_c(c)->m());
mk_c(c)->m_smtlib_parser->initialize_smtlib();
smtlib::symtable * table = mk_c(c)->m_smtlib_parser->get_benchmark()->get_symtable();
for (unsigned i = 0; i < num_sorts; i++) {
table->insert(to_symbol(sort_names[i]), to_sort(types[i]));
}
for (unsigned i = 0; i < num_decls; i++) {
table->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
}
}
void Z3_API Z3_parse_smtlib_string(Z3_context c,
const char * str,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
unsigned num_decls,
Z3_symbol const decl_names[],
Z3_func_decl const decls[]) {
Z3_TRY;
LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
bool ok = false;
RESET_ERROR_CODE();
init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try {
ok = mk_c(c)->m_smtlib_parser->parse_string(str);
}
catch (...) {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs->str();
outs = nullptr;
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);
}
Z3_CATCH;
}
void Z3_API Z3_parse_smtlib_file(Z3_context c,
const char * file_name,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const types[],
unsigned num_decls,
Z3_symbol const decl_names[],
Z3_func_decl const decls[]) {
Z3_string Z3_API Z3_get_parser_error(Z3_context c) {
Z3_TRY;
LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
bool ok = false;
RESET_ERROR_CODE();
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try {
ok = mk_c(c)->m_smtlib_parser->parse_file(file_name);
}
catch(...) {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs->str();
outs = nullptr;
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);
}
Z3_CATCH;
}
unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c) {
Z3_TRY;
LOG_Z3_get_smtlib_num_formulas(c);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas();
}
SET_ERROR_CODE(Z3_NO_PARSER);
return 0;
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_formula(c, i);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas()) {
ast * f = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_formulas()[i];
mk_c(c)->save_ast_trail(f);
RETURN_Z3(of_ast(f));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c) {
Z3_TRY;
LOG_Z3_get_smtlib_num_assumptions(c);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms();
}
SET_ERROR_CODE(Z3_NO_PARSER);
return 0;
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_assumption(c, i);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms()) {
ast * a = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_axioms()[i];
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c) {
Z3_TRY;
LOG_Z3_get_smtlib_num_decls(c);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
mk_c(c)->extract_smtlib_parser_decls();
return mk_c(c)->m_smtlib_parser_decls.size();
}
SET_ERROR_CODE(Z3_NO_PARSER);
return 0;
Z3_CATCH_RETURN(0);
}
Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_decl(c, i);
LOG_Z3_get_parser_error(c);
RESET_ERROR_CODE();
mk_c(c)->extract_smtlib_parser_decls();
if (mk_c(c)->m_smtlib_parser) {
if (i < mk_c(c)->m_smtlib_parser_decls.size()) {
func_decl * d = mk_c(c)->m_smtlib_parser_decls[i];
mk_c(c)->save_ast_trail(d);
RETURN_Z3(of_func_decl(d));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c) {
Z3_TRY;
LOG_Z3_get_smtlib_num_sorts(c);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
mk_c(c)->extract_smtlib_parser_decls();
return mk_c(c)->m_smtlib_parser_sorts.size();
}
SET_ERROR_CODE(Z3_NO_PARSER);
return 0;
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_sort(c, i);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
mk_c(c)->extract_smtlib_parser_decls();
if (i < mk_c(c)->m_smtlib_parser_sorts.size()) {
sort* s = mk_c(c)->m_smtlib_parser_sorts[i];
mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_get_smtlib_error(Z3_context c) {
Z3_TRY;
LOG_Z3_get_smtlib_error(c);
RESET_ERROR_CODE();
return mk_c(c)->m_smtlib_error_buffer.c_str();
return mk_c(c)->m_parser_error_buffer.c_str();
Z3_CATCH_RETURN("");
}
@ -268,10 +52,26 @@ extern "C" {
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
}
for (unsigned i = 0; i < num_sorts; ++i) {
psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
sort* srt = to_sort(sorts[i]);
symbol name(to_symbol(sort_names[i]));
if (!ctx->find_psort_decl(name)) {
psort* ps = ctx->pm().mk_psort_cnst(srt);
ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps));
}
}
if (!parse_smt2_commands(*ctx.get(), is)) {
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
try {
if (!parse_smt2_commands(*ctx.get(), is)) {
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());
}
}
catch (z3_exception& e) {
errstrm << e.msg();
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());

63
src/api/api_solver.cpp
View file

@ -28,11 +28,17 @@ Revision History:
#include "solver/tactic2solver.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "util/file_path.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 "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" {
@ -121,6 +127,63 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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);
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
bool initialized = to_solver(s)->m_solver.get() != 0;
if (!initialized)
init_solver(c, s);
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {
to_solver_ref(s)->assert_expr(*it);
}
// 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) {
Z3_TRY;
LOG_Z3_solver_from_string(c, s, c_str);
std::string str(c_str);
std::istringstream is(str);
solver_from_stream(c, s, is);
Z3_CATCH;
}
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) {
Z3_TRY;
LOG_Z3_solver_from_file(c, s, file_name);
char const* ext = get_extension(file_name);
std::ifstream is(file_name);
if (!is) {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR);
}
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);
parse_dimacs(is, solver);
sat2goal s2g;
model_converter_ref mc;
atom2bool_var a2b(m);
goal g(m);
s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
for (unsigned i = 0; i < g.size(); ++i) {
to_solver_ref(s)->assert_expr(g.form(i));
}
}
else {
solver_from_stream(c, s, is);
}
Z3_CATCH;
}
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_help(c, s);

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

@ -174,6 +174,15 @@ namespace z3 {
return e;
}
void check_parser_error() const {
Z3_error_code e = Z3_get_error_code(*this);
if (e != Z3_OK && enable_exceptions()) {
Z3_string s = Z3_get_parser_error(*this);
if (s && *s) Z3_THROW(exception(s));
}
check_error();
}
/**
\brief The C++ API uses by defaults exceptions on errors.
For applications that don't work well with exceptions (there should be only few)
@ -1527,6 +1536,38 @@ namespace z3 {
m_vector = s.m_vector;
return *this;
}
/*
Disabled pending C++98 build upgrade
bool contains(T const& x) const {
for (T y : *this) if (eq(x, y)) return true;
return false;
}
*/
class iterator {
ast_vector_tpl const* m_vector;
unsigned m_index;
public:
iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {}
iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
bool operator==(iterator const& other) {
return other.m_index == m_index;
};
bool operator!=(iterator const& other) {
return other.m_index != m_index;
};
iterator& operator++() {
++m_index;
return *this;
}
iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
T * operator->() const { return &(operator*()); }
T operator*() const { return (*m_vector)[m_index]; }
};
iterator begin() const { return iterator(this, 0); }
iterator end() const { return iterator(this, size()); }
friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
};
@ -1768,9 +1809,11 @@ namespace z3 {
Z3_model_inc_ref(ctx(), m);
}
public:
struct translate {};
model(context & c):object(c) { init(Z3_mk_model(c)); }
model(context & c, Z3_model m):object(c) { init(m); }
model(model const & s):object(s) { init(s.m_model); }
model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
~model() { Z3_model_dec_ref(ctx(), m_model); }
operator Z3_model() const { return m_model; }
model & operator=(model const & s) {
@ -1902,6 +1945,11 @@ namespace z3 {
return *this;
}
void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
@ -1914,6 +1962,11 @@ namespace z3 {
void add(expr const & e, char const * p) {
add(e, ctx().bool_const(p));
}
// fails for some compilers:
// void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
check_result check(unsigned n, expr * const assumptions) {
array<Z3_ast> _assumptions(n);
@ -1994,6 +2047,8 @@ 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); }
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
@ -2774,13 +2829,12 @@ namespace z3 {
inline expr context::parse_string(char const* s) {
Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
check_error();
return expr(*this, r);
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_error();
check_parser_error();
return expr(*this, r);
}
@ -2796,7 +2850,7 @@ namespace z3 {
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_error();
check_parser_error();
return expr(*this, r);
}
@ -2812,7 +2866,7 @@ namespace z3 {
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_error();
check_parser_error();
return expr(*this, r);
}

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

@ -2262,7 +2262,7 @@ namespace Microsoft.Z3
/// Maps f on the argument arrays.
/// </summary>
/// <remarks>
/// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
/// Each element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
/// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
/// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
/// <seealso cref="MkArraySort(Sort, Sort)"/>
@ -2862,7 +2862,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2878,7 +2878,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2894,7 +2894,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2910,7 +2910,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -3211,7 +3211,7 @@ namespace Microsoft.Z3
/// Create an existential Quantifier.
/// </summary>
/// <remarks>
/// Creates an existential quantifier using de-Brujin indexed variables.
/// Creates an existential quantifier using de-Bruijn indexed variables.
/// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
/// </remarks>
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
@ -3320,160 +3320,10 @@ namespace Microsoft.Z3
#endregion
#region SMT Files & Strings
/// <summary>
/// Convert a benchmark into an SMT-LIB formatted string.
/// </summary>
/// <param name="name">Name of the benchmark. The argument is optional.</param>
/// <param name="logic">The benchmark logic. </param>
/// <param name="status">The status string (sat, unsat, or unknown)</param>
/// <param name="attributes">Other attributes, such as source, difficulty or category.</param>
/// <param name="assumptions">Auxiliary assumptions.</param>
/// <param name="formula">Formula to be checked for consistency in conjunction with assumptions.</param>
/// <returns>A string representation of the benchmark.</returns>
public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
BoolExpr[] assumptions, BoolExpr formula)
{
Contract.Requires(assumptions != null);
Contract.Requires(formula != null);
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
formula.NativeObject);
}
/// <summary>
/// Parse the given string using the SMT-LIB parser.
/// </summary>
/// <remarks>
/// The symbol table of the parser can be initialized using the given sorts and declarations.
/// The symbols in the arrays <paramref name="sortNames"/> and <paramref name="declNames"/>
/// don't need to match the names of the sorts and declarations in the arrays <paramref name="sorts"/>
/// and <paramref name="decls"/>. This is a useful feature since we can use arbitrary names to
/// reference sorts and declarations.
/// </remarks>
public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
{
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_string(nCtx, str,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
/// <summary>
/// Parse the given file using the SMT-LIB parser.
/// </summary>
/// <seealso cref="ParseSMTLIBString"/>
public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
{
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_file(nCtx, fileName,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
/// <summary>
/// The number of SMTLIB formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
/// <summary>
/// The formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public BoolExpr[] SMTLIBFormulas
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
uint n = NumSMTLIBFormulas;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
return res;
}
}
/// <summary>
/// The number of SMTLIB assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
/// <summary>
/// The assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public BoolExpr[] SMTLIBAssumptions
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
uint n = NumSMTLIBAssumptions;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
return res;
}
}
/// <summary>
/// The number of SMTLIB declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
/// <summary>
/// The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public FuncDecl[] SMTLIBDecls
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumSMTLIBDecls;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
return res;
}
}
/// <summary>
/// The number of SMTLIB sorts parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
/// <summary>
/// The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
/// </summary>
public Sort[] SMTLIBSorts
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
uint n = NumSMTLIBSorts;
Sort[] res = new Sort[n];
for (uint i = 0; i < n; i++)
res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
return res;
}
}
/// <summary>
/// Parse the given string using the SMT-LIB2 parser.
/// </summary>
/// <seealso cref="ParseSMTLIBString"/>
/// <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)
{

14
src/api/dotnet/Expr.cs
View file

@ -959,7 +959,7 @@ namespace Microsoft.Z3
/// Tn: (R t_n s_n)
/// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
/// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
/// That is, reflexivity proofs are supressed to save space.
/// That is, reflexivity proofs are suppressed to save space.
/// </remarks>
public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
@ -1002,7 +1002,7 @@ namespace Microsoft.Z3
public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
/// <summary>
/// Indicates whether the term is a proof by eliminiation of not-or
/// Indicates whether the term is a proof by elimination of not-or
/// </summary>
/// <remarks>
/// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
@ -1112,7 +1112,7 @@ namespace Microsoft.Z3
public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
/// <summary>
/// Indicates whether the term is a hypthesis marker.
/// Indicates whether the term is a hypothesis marker.
/// </summary>
/// <remarks>Mark a hypothesis in a natural deduction style proof.</remarks>
public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
@ -1433,7 +1433,7 @@ namespace Microsoft.Z3
/// <remarks>
/// Filter (restrict) a relation with respect to a predicate.
/// The first argument is a relation.
/// The second argument is a predicate with free de-Brujin indices
/// The second argument is a predicate with free de-Bruijn indices
/// corresponding to the columns of the relation.
/// So the first column in the relation has index 0.
/// </remarks>
@ -1649,7 +1649,7 @@ namespace Microsoft.Z3
public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
/// <summary>
/// Indicates whether the term is a floating-point divison term
/// Indicates whether the term is a floating-point division term
/// </summary>
public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
@ -1709,7 +1709,7 @@ namespace Microsoft.Z3
public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
/// <summary>
/// Indicates whether the term is a floating-point greater-than or erqual term
/// Indicates whether the term is a floating-point greater-than or equal term
/// </summary>
public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
@ -1789,7 +1789,7 @@ namespace Microsoft.Z3
#region Bound Variables
/// <summary>
/// The de-Burijn index of a bound variable.
/// The de-Bruijn index of a bound variable.
/// </summary>
/// <remarks>
/// Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain

2
src/api/dotnet/Model.cs
View file

@ -253,7 +253,7 @@ namespace Microsoft.Z3
/// The uninterpreted sorts that the model has an interpretation for.
/// </summary>
/// <remarks>
/// Z3 also provides an intepretation for uninterpreted sorts used in a formula.
/// Z3 also provides an interpretation for uninterpreted sorts used in a formula.
/// The interpretation for a sort is a finite set of distinct values. We say this finite set is
/// the "universe" of the sort.
/// </remarks>

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

@ -31,98 +31,108 @@ namespace Microsoft.Z3
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, bool value)
public Params Add(Symbol name, bool value)
{
Contract.Requires(name != null);
Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, uint value)
public Params Add(Symbol name, uint value)
{
Contract.Requires(name != null);
Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, double value)
public Params Add(Symbol name, double value)
{
Contract.Requires(name != null);
Contract.Requires(name != null);
Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, string value)
public Params Add(Symbol name, string value)
{
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, Symbol value)
public Params Add(Symbol name, Symbol value)
{
Contract.Requires(name != null);
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, bool value)
public Params Add(string name, bool value)
{
Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, uint value)
public Params Add(string name, uint value)
{
Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, double value)
public Params Add(string name, double value)
{
Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, Symbol value)
public Params Add(string name, Symbol value)
{
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, string value)
public Params Add(string name, string value)
{
Contract.Requires(name != null);
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
return this;
}
/// <summary>

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

@ -57,6 +57,49 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Retrieves parameter descriptions for solver.
/// </summary>
@ -140,11 +183,11 @@ namespace Microsoft.Z3
/// using the Boolean constants in ps.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// This API is an alternative to <see cref="Check(Expr[])"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// provided using <see cref="Check(Expr[])"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
{
@ -165,11 +208,11 @@ namespace Microsoft.Z3
/// using the Boolean constant p.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// This API is an alternative to <see cref="Check(Expr[])"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// provided using <see cref="Check(Expr[])"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
{
@ -181,6 +224,22 @@ namespace Microsoft.Z3
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
}
/// <summary>
/// Load solver assertions from a file.
/// </summary>
public void FromFile(string file)
{
Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);
}
/// <summary>
/// Load solver assertions from a string.
/// </summary>
public void FromString(string str)
{
Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);
}
/// <summary>
/// The number of assertions in the solver.
/// </summary>
@ -225,6 +284,25 @@ namespace Microsoft.Z3
return lboolToStatus(r);
}
/// <summary>
/// Checks whether the assertions in the solver are consistent or not.
/// </summary>
/// <remarks>
/// <seealso cref="Model"/>
/// <seealso cref="UnsatCore"/>
/// <seealso cref="Proof"/>
/// </remarks>
public Status Check(IEnumerable<BoolExpr> assumptions)
{
Z3_lbool r;
BoolExpr[] asms = assumptions.ToArray();
if (asms.Length == 0)
r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
else
r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));
return lboolToStatus(r);
}
/// <summary>
/// Retrieve fixed assignments to the set of variables in the form of consequences.
/// Each consequence is an implication of the form

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

@ -2234,7 +2234,7 @@ public class Context implements AutoCloseable {
}
/**
* Create a Term of a given sort. This function can be use to create
* Create a Term of a given sort. This function can be used to create
* numerals that fit in a machine integer. It is slightly faster than
* {@code MakeNumeral} since it is not necessary to parse a string.
*
@ -2250,7 +2250,7 @@ public class Context implements AutoCloseable {
}
/**
* Create a Term of a given sort. This function can be use to create
* Create a Term of a given sort. This function can be used to create
* numerals that fit in a machine integer. It is slightly faster than
* {@code MakeNumeral} since it is not necessary to parse a string.
*
@ -2438,7 +2438,7 @@ public class Context implements AutoCloseable {
}
/**
* Creates an existential quantifier using de-Brujin indexed variables.
* Creates an existential quantifier using de-Bruijn indexed variables.
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
@ -2540,147 +2540,8 @@ public class Context implements AutoCloseable {
AST.arrayToNative(assumptions), formula.getNativeObject());
}
/**
* Parse the given string using the SMT-LIB parser.
* Remarks: The symbol
* table of the parser can be initialized using the given sorts and
* declarations. The symbols in the arrays {@code sortNames} and
* {@code declNames} don't need to match the names of the sorts
* and declarations in the arrays {@code sorts} and {@code decls}. This is a useful feature since we can use arbitrary names
* to reference sorts and declarations.
**/
public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
Symbol[] declNames, FuncDecl[] decls)
{
int csn = Symbol.arrayLength(sortNames);
int cs = Sort.arrayLength(sorts);
int cdn = Symbol.arrayLength(declNames);
int cd = AST.arrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
AST.arrayLength(decls), Symbol.arrayToNative(declNames),
AST.arrayToNative(decls));
}
/**
* Parse the given file using the SMT-LIB parser.
* @see #parseSMTLIBString
**/
public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
{
int csn = Symbol.arrayLength(sortNames);
int cs = Sort.arrayLength(sorts);
int cdn = Symbol.arrayLength(declNames);
int cd = AST.arrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
AST.arrayLength(decls), Symbol.arrayToNative(declNames),
AST.arrayToNative(decls));
}
/**
* The number of SMTLIB formulas parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public int getNumSMTLIBFormulas()
{
return Native.getSmtlibNumFormulas(nCtx());
}
/**
* The formulas parsed by the last call to {@code ParseSMTLIBString} or
* {@code ParseSMTLIBFile}.
**/
public BoolExpr[] getSMTLIBFormulas()
{
int n = getNumSMTLIBFormulas();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
res[i] = (BoolExpr) Expr.create(this,
Native.getSmtlibFormula(nCtx(), i));
return res;
}
/**
* The number of SMTLIB assumptions parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public int getNumSMTLIBAssumptions()
{
return Native.getSmtlibNumAssumptions(nCtx());
}
/**
* The assumptions parsed by the last call to {@code ParseSMTLIBString}
* or {@code ParseSMTLIBFile}.
**/
public BoolExpr[] getSMTLIBAssumptions()
{
int n = getNumSMTLIBAssumptions();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
res[i] = (BoolExpr) Expr.create(this,
Native.getSmtlibAssumption(nCtx(), i));
return res;
}
/**
* The number of SMTLIB declarations parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public int getNumSMTLIBDecls()
{
return Native.getSmtlibNumDecls(nCtx());
}
/**
* The declarations parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public FuncDecl[] getSMTLIBDecls()
{
int n = getNumSMTLIBDecls();
FuncDecl[] res = new FuncDecl[n];
for (int i = 0; i < n; i++)
res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
return res;
}
/**
* The number of SMTLIB sorts parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public int getNumSMTLIBSorts()
{
return Native.getSmtlibNumSorts(nCtx());
}
/**
* The declarations parsed by the last call to
* {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
**/
public Sort[] getSMTLIBSorts()
{
int n = getNumSMTLIBSorts();
Sort[] res = new Sort[n];
for (int i = 0; i < n; i++)
res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
return res;
}
/**
* Parse the given string using the SMT-LIB2 parser.
* @see #parseSMTLIBString
*
* @return A conjunction of assertions in the scope (up to push/pop) at the
* end of the string.

10
src/api/java/Expr.java
View file

@ -1421,7 +1421,7 @@ public class Expr extends AST
* Remarks: T1:
* (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ...
* t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is
* suppressed. That is, reflexivity proofs are supressed to save space.
* suppressed. That is, reflexivity proofs are suppressed to save space.
*
* @throws Z3Exception on error
* @return a boolean
@ -1473,7 +1473,7 @@ public class Expr extends AST
}
/**
* Indicates whether the term is a proof by eliminiation of not-or
* Indicates whether the term is a proof by elimination of not-or
* Remarks: * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)
* @throws Z3Exception on error
* @return a boolean
@ -1605,7 +1605,7 @@ public class Expr extends AST
}
/**
* Indicates whether the term is a hypthesis marker.
* Indicates whether the term is a hypothesis marker.
* Remarks: Mark a
* hypothesis in a natural deduction style proof.
* @throws Z3Exception on error
@ -1987,7 +1987,7 @@ public class Expr extends AST
* Indicates whether the term is a relation filter
* Remarks: Filter
* (restrict) a relation with respect to a predicate. The first argument is
* a relation. The second argument is a predicate with free de-Brujin
* a relation. The second argument is a predicate with free de-Bruijn
* indices corresponding to the columns of the relation. So the first column
* in the relation has index 0.
* @throws Z3Exception on error
@ -2094,7 +2094,7 @@ public class Expr extends AST
}
/**
* The de-Burijn index of a bound variable.
* The de-Bruijn index of a bound variable.
* Remarks: Bound variables are
* indexed by de-Bruijn indices. It is perhaps easiest to explain the
* meaning of de-Bruijn indices by indicating the compilation process from

2
src/api/java/Model.java
View file

@ -239,7 +239,7 @@ public class Model extends Z3Object {
/**
* The uninterpreted sorts that the model has an interpretation for.
* Remarks: Z3 also provides an intepretation for uninterpreted sorts used
* Remarks: Z3 also provides an interpretation for uninterpreted sorts used
* in a formula. The interpretation for a sort is a finite set of distinct
* values. We say this finite set is the "universe" of the sort.
*

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

@ -1,3 +1,4 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
@ -120,6 +121,23 @@ 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
* unsat) core

52
src/api/ml/z3.ml
View file

@ -1975,56 +1975,6 @@ struct
(List.length assumptions) assumptions
formula
let parse_smtlib_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = List.length sort_names in
let cs = List.length sorts in
let cdn = List.length decl_names in
let cd = List.length decls in
if (csn <> cs || cdn <> cd) then
raise (Error "Argument size mismatch")
else
Z3native.parse_smtlib_string ctx str
cs sort_names sorts cd decl_names decls
let parse_smtlib_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = (List.length sort_names) in
let cs = (List.length sorts) in
let cdn = (List.length decl_names) in
let cd = (List.length decls) in
if (csn <> cs || cdn <> cd) then
raise (Error "Argument size mismatch")
else
Z3native.parse_smtlib_file ctx file_name
cs sort_names sorts cd decl_names decls
let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx
let get_smtlib_formulas (ctx:context) =
let n = get_num_smtlib_formulas ctx in
let f i = Z3native.get_smtlib_formula ctx i in
mk_list f n
let get_num_smtlib_assumptions (ctx:context) = Z3native.get_smtlib_num_assumptions ctx
let get_smtlib_assumptions (ctx:context) =
let n = get_num_smtlib_assumptions ctx in
let f i = Z3native.get_smtlib_assumption ctx i in
mk_list f n
let get_num_smtlib_decls (ctx:context) = Z3native.get_smtlib_num_decls ctx
let get_smtlib_decls (ctx:context) =
let n = get_num_smtlib_decls ctx in
let f i = Z3native.get_smtlib_decl ctx i in
mk_list f n
let get_num_smtlib_sorts (ctx:context) = Z3native.get_smtlib_num_sorts ctx
let get_smtlib_sorts (ctx:context) =
let n = get_num_smtlib_sorts ctx in
let f i = Z3native.get_smtlib_sort ctx i in
mk_list f n
let parse_smtlib2_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = List.length sort_names in
let cs = List.length sorts in
@ -2044,7 +1994,7 @@ struct
if csn <> cs || cdn <> cd then
raise (Error "Argument size mismatch")
else
Z3native.parse_smtlib2_string ctx file_name
Z3native.parse_smtlib2_file ctx file_name
cs sort_names sorts cd decl_names decls
end

67
src/api/ml/z3.mli
View file

@ -536,7 +536,7 @@ sig
@return A Term with the given value and sort *)
val mk_numeral_string : context -> string -> Sort.sort -> expr
(** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer.
(** Create a numeral of a given sort. This function can be used to create numerals that fit in a machine integer.
It is slightly faster than [MakeNumeral] since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
@ -667,7 +667,7 @@ sig
end
(** The de-Burijn index of a bound variable.
(** The de-Bruijn index of a bound variable.
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
the meaning of de-Bruijn indices by indicating the compilation process from
@ -830,7 +830,7 @@ sig
(** Maps f on the argument arrays.
Eeach element of [args] must be of an array sort [[domain_i -> range_i]].
Each element of [args] must be of an array sort [[domain_i -> range_i]].
The function declaration [f] must have type [ range_1 .. range_n -> range].
[v] must have sort range. The sort of the result is [[domain_i -> range]].
{!Z3Array.mk_sort}
@ -962,7 +962,7 @@ sig
Filter (restrict) a relation with respect to a predicate.
The first argument is a relation.
The second argument is a predicate with free de-Brujin indices
The second argument is a predicate with free de-Bruijn indices
corresponding to the columns of the relation.
So the first column in the relation has index 0. *)
val is_filter : Expr.expr -> bool
@ -2085,7 +2085,7 @@ sig
(** Indicates whether an expression is a floating-point lt expression *)
val is_lt : Expr.expr -> bool
(** Indicates whether an expression is a floating-point geqexpression *)
(** Indicates whether an expression is a floating-point geq expression *)
val is_geq : Expr.expr -> bool
(** Indicates whether an expression is a floating-point gt expression *)
@ -2233,7 +2233,7 @@ sig
(** Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. *)
val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
(** C1onversion of a floating-point term into an unsigned bit-vector. *)
(** Conversion of a floating-point term into an unsigned bit-vector. *)
val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
(** Conversion of a floating-point term into a signed bit-vector. *)
@ -2385,7 +2385,7 @@ sig
Tn: (R t_n s_n)
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are supressed to save space. *)
That is, reflexivity proofs are suppressed to save space. *)
val is_monotonicity : Expr.expr -> bool
(** Indicates whether the term is a quant-intro proof
@ -2417,7 +2417,7 @@ sig
[and-elim T1]: l_i *)
val is_and_elimination : Expr.expr -> bool
(** Indicates whether the term is a proof by eliminiation of not-or
(** Indicates whether the term is a proof by elimination of not-or
Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
T1: (not (or l_1 ... l_n))
@ -2500,7 +2500,7 @@ sig
A proof of (or (not (forall (x) (P x))) (P a)) *)
val is_quant_inst : Expr.expr -> bool
(** Indicates whether the term is a hypthesis marker.
(** Indicates whether the term is a hypothesis marker.
Mark a hypothesis in a natural deduction style proof. *)
val is_hypothesis : Expr.expr -> bool
@ -2882,7 +2882,7 @@ sig
(** The uninterpreted sorts that the model has an interpretation for.
Z3 also provides an intepretation for uninterpreted sorts used in a formula.
Z3 also provides an interpretation for uninterpreted sorts used in a formula.
The interpretation for a sort is a finite set of distinct values. We say this finite set is
the "universe" of the sort.
{!get_num_sorts}
@ -3056,7 +3056,7 @@ sig
(** Create a tactic that fails if the probe evaluates to false. *)
val fail_if : context -> Probe.probe -> tactic
(** Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
(** Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
or trivially unsatisfiable (i.e., contains `false'). *)
val fail_if_not_decided : context -> tactic
@ -3105,7 +3105,7 @@ sig
(** True if the entry is float-valued. *)
val is_float : statistics_entry -> bool
(** The string representation of the the entry's value. *)
(** The string representation of the entry's value. *)
val to_string_value : statistics_entry -> string
(** The string representation of the entry (key and value) *)
@ -3370,7 +3370,7 @@ sig
(** Assert a constraints into the optimize solver. *)
val add : optimize -> Expr.expr list -> unit
(** Asssert a soft constraint.
(** Assert a soft constraint.
Supply integer weight and string that identifies a group
of soft constraints. *)
val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle
@ -3441,51 +3441,12 @@ sig
@return A string representation of the benchmark. *)
val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string
(** Parse the given string using the SMT-LIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays in the third and fifth argument
don't need to match the names of the sorts and declarations in the arrays in the fourth
and sixth argument. This is a useful feature since we can use arbitrary names to
reference sorts and declarations. *)
val parse_smtlib_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** Parse the given file using the SMT-LIB parser.
{!parse_smtlib_string} *)
val parse_smtlib_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** The number of SMTLIB formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_formulas : context -> int
(** The formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_formulas : context -> Expr.expr list
(** The number of SMTLIB assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_assumptions : context -> int
(** The assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_assumptions : context -> Expr.expr list
(** The number of SMTLIB declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_decls : context -> int
(** The declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_decls : context -> FuncDecl.func_decl list
(** The number of SMTLIB sorts parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_sorts : context -> int
(** The sort declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_sorts : context -> Sort.sort list
(** Parse the given string using the SMT-LIB2 parser.
{!parse_smtlib_string}
@return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
(** Parse the given file using the SMT-LIB2 parser.
{!parse_smtlib2_string} *)
(** Parse the given file using the SMT-LIB2 parser. *)
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
end

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

@ -182,7 +182,7 @@ class Context:
"""Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
This method can be invoked from a thread different from the one executing the
interruptable procedure.
interruptible procedure.
"""
Z3_interrupt(self.ref())
@ -365,6 +365,12 @@ class AstRef(Z3PPObject):
_z3_assert(isinstance(target, Context), "argument must be a Z3 context")
return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def hash(self):
"""Return a hashcode for the `self`.
@ -596,7 +602,7 @@ def _sort(ctx, a):
return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
def DeclareSort(name, ctx=None):
"""Create a new uninterpred sort named `name`.
"""Create a new uninterpreted sort named `name`.
If `ctx=None`, then the new sort is declared in the global Z3Py context.
@ -718,7 +724,7 @@ class FuncDeclRef(AstRef):
The arguments must be Z3 expressions. This method assumes that
the sorts of the elements in `args` match the sorts of the
domain. Limited coersion is supported. For example, if
domain. Limited coercion is supported. For example, if
args[0] is a Python integer, and the function expects a Z3
integer, then the argument is automatically converted into a
Z3 integer.
@ -3568,6 +3574,14 @@ def BV2Int(a, is_signed=False):
## investigate problem with bv2int
return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
def Int2BV(a, num_bits):
"""Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
modulo of a by 2^num_bits
"""
ctx = a.ctx
return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
def BitVecSort(sz, ctx=None):
"""Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
@ -5040,6 +5054,12 @@ class Goal(Z3PPObject):
_z3_assert(isinstance(target, Context), "target must be a context")
return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def simplify(self, *arguments, **keywords):
"""Return a new simplified goal.
@ -5132,9 +5152,18 @@ class AstVector(Z3PPObject):
>>> A[1]
y
"""
if i >= self.__len__():
raise IndexError
return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
if isinstance(i, int):
if i < 0:
i += self.__len__()
if i >= self.__len__():
raise IndexError
return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
elif isinstance(i, slice):
return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))]
def __setitem__(self, i, v):
"""Update AST at position `i`.
@ -5213,6 +5242,12 @@ class AstVector(Z3PPObject):
"""
return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def __repr__(self):
return obj_to_string(self)
@ -5550,6 +5585,17 @@ class FuncInterp(Z3PPObject):
raise IndexError
return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
def translate(self, other_ctx):
"""Copy model 'self' to context 'other_ctx'.
"""
return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def as_list(self):
"""Return the function interpretation as a Python list.
>>> f = Function('f', IntSort(), IntSort())
@ -5579,9 +5625,6 @@ class ModelRef(Z3PPObject):
self.ctx = ctx
Z3_model_inc_ref(self.ctx.ref(), self.model)
def __deepcopy__(self, memo={}):
return ModelRef(self.m, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_model_dec_ref(self.ctx.ref(), self.model)
@ -5835,6 +5878,20 @@ class ModelRef(Z3PPObject):
r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
return r
def translate(self, target):
"""Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
"""
if __debug__:
_z3_assert(isinstance(target, Context), "argument must be a Z3 context")
model = Z3_model_translate(self.ctx.ref(), self.model, target.ref())
return Model(model, target)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def is_as_array(n):
"""Return true if n is a Z3 expression of the form (_ as-array f)."""
return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
@ -6037,9 +6094,6 @@ class Solver(Z3PPObject):
self.solver = solver
Z3_solver_inc_ref(self.ctx.ref(), self.solver)
def __deepcopy__(self, memo={}):
return Solver(self.solver, self.ctx)
def __del__(self):
if self.solver is not None and self.ctx.ref() is not None:
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
@ -6324,6 +6378,20 @@ class Solver(Z3PPObject):
sz = len(consequences)
consequences = [ consequences[i] for i in range(sz) ]
return CheckSatResult(r), consequences
def from_file(self, filename):
"""Parse assertions from a file"""
try:
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def from_string(self, s):
"""Parse assertions from a string"""
try:
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def proof(self):
"""Return a proof for the last `check()`. Proof construction must be enabled."""
@ -6399,6 +6467,12 @@ class Solver(Z3PPObject):
solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
return Solver(solver, target)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def sexpr(self):
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
@ -6668,11 +6742,17 @@ class Fixedpoint(Z3PPObject):
def parse_string(self, s):
"""Parse rules and queries from a string"""
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
try:
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def parse_file(self, f):
"""Parse rules and queries from a file"""
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
try:
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
@ -6995,15 +7075,21 @@ class Optimize(Z3PPObject):
def upper_values(self, obj):
if not isinstance(obj, OptimizeObjective):
raise Z3Exception("Expecting objective handle returned by maximize/minimize")
return obj.upper_values()
return obj.upper_values()
def from_file(self, filename):
"""Parse assertions and objectives from a file"""
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
try:
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def from_string(self, s):
"""Parse assertions and objectives from a string"""
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
try:
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def assertions(self):
"""Return an AST vector containing all added constraints."""
@ -8071,6 +8157,12 @@ def _dict2darray(decls, ctx):
i = i + 1
return sz, _names, _decls
def _handle_parse_error(ex, ctx):
msg = Z3_get_parser_error(ctx.ref())
if msg != "":
raise Z3Exception(msg)
raise ex
def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
"""Parse a string in SMT 2.0 format using the given sorts and decls.
@ -8089,7 +8181,10 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
ctx = _get_ctx(ctx)
ssz, snames, ssorts = _dict2sarray(sorts, ctx)
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
try:
return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
except Z3Exception as e:
_handle_parse_error(e, ctx)
def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
"""Parse a file in SMT 2.0 format using the given sorts and decls.
@ -8099,7 +8194,10 @@ 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)
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
try:
return _to_expr_ref(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.
@ -9145,7 +9243,7 @@ def fpMul(rm, a, b, ctx=None):
return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
def fpDiv(rm, a, b, ctx=None):
"""Create a Z3 floating-point divison expression.
"""Create a Z3 floating-point division expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
@ -9172,7 +9270,7 @@ def fpRem(a, b, ctx=None):
return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
def fpMin(a, b, ctx=None):
"""Create a Z3 floating-point minimium expression.
"""Create a Z3 floating-point minimum expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()

185
src/api/z3_api.h
View file

@ -270,7 +270,7 @@ typedef enum
- Z3_OP_ARRAY_MAP Array map operator.
It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
- Z3_OP_SET_UNION Set union between two Booelan arrays (two arrays whose range type is Boolean). The function is binary.
- Z3_OP_SET_UNION Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
- Z3_OP_SET_INTERSECT Set intersection between two Boolean arrays. The function is binary.
@ -406,7 +406,7 @@ typedef enum
- Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow.
Signed multiplication underflows if the operands have opposite signs and the result of multiplication
does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow.
does not fit within the available bits. Z3_mk_bvmul_no_underflow.
- Z3_OP_BSDIV_I: Binary signed division.
It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
@ -485,7 +485,7 @@ typedef enum
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
}
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are supressed to save space.
That is, reflexivity proofs are suppressed to save space.
- Z3_OP_PR_QUANT_INTRO: Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
@ -832,7 +832,7 @@ typedef enum
- Z3_OP_RA_FILTER: Filter (restrict) a relation with respect to a predicate.
The first argument is a relation.
The second argument is a predicate with free de-Brujin indices
The second argument is a predicate with free de-Bruijn indices
corresponding to the columns of the relation.
So the first column in the relation has index 0.
@ -969,7 +969,7 @@ typedef enum
- Z3_OP_FPA_TO_FP: Floating-point conversion (various)
- Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigend bit-vector
- Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigned bit-vector
- Z3_OP_FPA_TO_UBV: Floating-point conversion to unsigned bit-vector
@ -984,7 +984,7 @@ typedef enum
of non-relevant terms in theory_fpa)
- Z3_OP_FPA_BV2RM: Conversion of a 3-bit bit-vector term to a
floating-point rouding-mode term
floating-point rounding-mode term
The conversion uses the following values:
0 = 000 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@ -1314,13 +1314,11 @@ typedef enum {
- Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
- Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
- Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
- Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.
*/
typedef enum {
Z3_PRINT_SMTLIB_FULL,
Z3_PRINT_LOW_LEVEL,
Z3_PRINT_SMTLIB_COMPLIANT,
Z3_PRINT_SMTLIB2_COMPLIANT
} Z3_ast_print_mode;
@ -1333,7 +1331,7 @@ typedef enum {
- Z3_IOB: Index out of bounds.
- Z3_INVALID_ARG: Invalid argument was provided.
- Z3_PARSER_ERROR: An error occurred when parsing a string or file.
- Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
- Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
- Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
- Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
@ -1924,7 +1922,7 @@ extern "C" {
\param c logical context
\param name name of the enumeration sort.
\param n number of elemenets in enumeration sort.
\param n number of elements in enumeration sort.
\param enum_names names of the enumerated elements.
\param enum_consts constants corresponding to the enumerated elements.
\param enum_testers predicates testing if terms of the enumeration sort correspond to an enumeration.
@ -3188,7 +3186,7 @@ extern "C" {
\param c logical context.
\param num numerator of rational.
\param den denomerator of rational.
\param den denominator of rational.
\pre den != 0
@ -3203,7 +3201,7 @@ extern "C" {
/**
\brief Create a numeral of an int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine integer.
This function can be used to create numerals that fit in a machine integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3215,7 +3213,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine unsinged integer.
This function can be used to create numerals that fit in a machine unsigned integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3227,7 +3225,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine __int64 integer.
This function can be used to create numerals that fit in a machine __int64 integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3239,7 +3237,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine __uint64 integer.
This function can be used to create numerals that fit in a machine __uint64 integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3495,8 +3493,8 @@ extern "C" {
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
/**
\brief Create a regular expression loop. The supplied regular expression \c r is repated
between \c lo and \c hi times. The \c lo should be below \c hi with one exection: when
\brief Create a regular expression loop. The supplied regular expression \c r is repeated
between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when
supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least
\c lo number of times, and with an unbounded upper bound.
@ -4250,7 +4248,7 @@ extern "C" {
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
/**
\brief Return the expresson value associated with an expression parameter.
\brief Return the expression value associated with an expression parameter.
\pre Z3_get_decl_parameter_kind(c, d, idx) == Z3_PARAMETER_AST
@ -4259,7 +4257,7 @@ extern "C" {
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
/**
\brief Return the expresson value associated with an expression parameter.
\brief Return the expression value associated with an expression parameter.
\pre Z3_get_decl_parameter_kind(c, d, idx) == Z3_PARAMETER_FUNC_DECL
@ -4301,7 +4299,7 @@ extern "C" {
/**
\brief Return the i-th argument of the given application.
\pre i < Z3_get_num_args(c, a)
\pre i < Z3_get_app_num_args(c, a)
def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT)))
*/
@ -4329,7 +4327,7 @@ extern "C" {
/**
\brief Return a hash code for the given AST.
The hash code is structural. You can use Z3_get_ast_id interchangably with
The hash code is structural. You can use Z3_get_ast_id interchangeably with
this function.
def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
@ -4558,7 +4556,7 @@ extern "C" {
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
/**
\brief Return index of de-Brujin bound variable.
\brief Return index of de-Bruijn bound variable.
\pre Z3_get_ast_kind(a) == Z3_VAR_AST
@ -4661,7 +4659,7 @@ extern "C" {
Provides an interface to the AST simplifier used by Z3.
It returns an AST object which is equal to the argument.
The returned AST is simplified using algebraic simplificaiton rules,
The returned AST is simplified using algebraic simplification rules,
such as constant propagation (propagating true/false over logical connectives).
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
@ -4863,9 +4861,9 @@ extern "C" {
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
/**
\brief Return the number of uninterpreted sorts that \c m assigs an interpretation to.
\brief Return the number of uninterpreted sorts that \c m assigns an interpretation to.
Z3 also provides an intepretation for uninterpreted sorts used in a formua.
Z3 also provides an interpretation for uninterpreted sorts used in a formula.
The interpretation for a sort \c s is a finite set of distinct values. We say this finite set is
the "universe" of \c s.
@ -4898,6 +4896,13 @@ extern "C" {
*/
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
/**
\brief translate model from context c to context \c dst.
def_API('Z3_model_translate', MODEL, (_in(CONTEXT), _in(MODEL), _in(CONTEXT)))
*/
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
/**
\brief The \ccode{(_ as-array f)} AST node is a construct for assigning interpretations for arrays in Z3.
It is the array such that forall indices \c i we have that \ccode{(select (_ as-array f) i)} is equal to \ccode{(f i)}.
@ -4966,7 +4971,7 @@ extern "C" {
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
/**
\brief Return a "point" of the given function intepretation. It represents the
\brief Return a "point" of the given function interpretation. It represents the
value of \c f in a particular point.
\pre i < Z3_func_interp_get_num_entries(c, f)
@ -5008,7 +5013,7 @@ extern "C" {
\brief add a function entry to a function interpretation.
\param c logical context
\param fi a function interpregation to be updated.
\param fi a function interpretation to be updated.
\param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
\param value value of the function when the parameters match args.
@ -5116,7 +5121,7 @@ extern "C" {
To print shared common subexpressions only once,
use the Z3_PRINT_LOW_LEVEL mode.
To print in way that conforms to SMT-LIB standards and uses let
expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
expressions to share common sub-expressions use Z3_PRINT_SMTLIB2_COMPLIANT.
\sa Z3_ast_to_string
\sa Z3_pattern_to_string
@ -5228,115 +5233,13 @@ extern "C" {
Z3_symbol const decl_names[],
Z3_func_decl const decls[]);
/**
\brief Parse the given string using the SMT-LIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays \c sort_names and \c decl_names don't need to match the names
of the sorts and declarations in the arrays \c sorts and \c decls. This is an useful feature
since we can use arbitrary names to reference sorts and declarations defined using the C API.
The formulas, assumptions and declarations defined in \c str can be extracted using the functions:
#Z3_get_smtlib_num_formulas, #Z3_get_smtlib_formula, #Z3_get_smtlib_num_assumptions, #Z3_get_smtlib_assumption,
#Z3_get_smtlib_num_decls, and #Z3_get_smtlib_decl.
def_API('Z3_parse_smtlib_string', VOID, (_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)))
*/
void Z3_API Z3_parse_smtlib_string(Z3_context c,
Z3_string str,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
unsigned num_decls,
Z3_symbol const decl_names[],
Z3_func_decl const decls[]
);
/**
\brief Similar to #Z3_parse_smtlib_string, but reads the benchmark from a file.
def_API('Z3_parse_smtlib_file', VOID, (_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)))
*/
void Z3_API Z3_parse_smtlib_file(Z3_context c,
Z3_string file_name,
unsigned num_sorts,
Z3_symbol const sort_names[],
Z3_sort const sorts[],
unsigned num_decls,
Z3_symbol const decl_names[],
Z3_func_decl const decls[]
);
/**
\brief Return the number of SMTLIB formulas parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
def_API('Z3_get_smtlib_num_formulas', UINT, (_in(CONTEXT), ))
*/
unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c);
/**
\brief Return the i-th formula parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
\pre i < Z3_get_smtlib_num_formulas(c)
def_API('Z3_get_smtlib_formula', AST, (_in(CONTEXT), _in(UINT)))
*/
Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i);
/**
\brief Return the number of SMTLIB assumptions parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
def_API('Z3_get_smtlib_num_assumptions', UINT, (_in(CONTEXT), ))
*/
unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c);
/**
\brief Return the i-th assumption parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
\pre i < Z3_get_smtlib_num_assumptions(c)
def_API('Z3_get_smtlib_assumption', AST, (_in(CONTEXT), _in(UINT)))
*/
Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i);
/**
\brief Return the number of declarations parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
def_API('Z3_get_smtlib_num_decls', UINT, (_in(CONTEXT), ))
*/
unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c);
/**
\brief Return the i-th declaration parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
\pre i < Z3_get_smtlib_num_decls(c)
def_API('Z3_get_smtlib_decl', FUNC_DECL, (_in(CONTEXT), _in(UINT)))
*/
Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i);
/**
\brief Return the number of sorts parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
def_API('Z3_get_smtlib_num_sorts', UINT, (_in(CONTEXT), ))
*/
unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c);
/**
\brief Return the i-th sort parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
\pre i < Z3_get_smtlib_num_sorts(c)
def_API('Z3_get_smtlib_sort', SORT, (_in(CONTEXT), _in(UINT)))
*/
Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i);
/**
\brief Retrieve that last error message information generated from parsing.
def_API('Z3_get_smtlib_error', STRING, (_in(CONTEXT), ))
def_API('Z3_get_parser_error', STRING, (_in(CONTEXT), ))
*/
Z3_string Z3_API Z3_get_smtlib_error(Z3_context c);
Z3_string Z3_API Z3_get_parser_error(Z3_context c);
/*@}*/
/** @name Error Handling */
@ -5563,7 +5466,7 @@ extern "C" {
Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
/**
\brief Copy a goal \c g from the context \c source to a the context \c target.
\brief Copy a goal \c g from the context \c source to the context \c target.
def_API('Z3_goal_translate', GOAL, (_in(CONTEXT), _in(GOAL), _in(CONTEXT)))
*/
@ -6029,7 +5932,7 @@ extern "C" {
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
/**
\brief Copy a solver \c s from the context \c source to a the context \c target.
\brief Copy a solver \c s from the context \c source to the context \c target.
def_API('Z3_solver_translate', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(CONTEXT)))
*/
@ -6142,6 +6045,20 @@ extern "C" {
*/
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
/**
\brief load solver assertions from a file.
def_API('Z3_solver_from_file', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
*/
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
/**
\brief load solver assertions from a string.
def_API('Z3_solver_from_string', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
*/
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
/**
\brief Check whether the assertions in a given solver are consistent or not.

4
src/ast/arith_decl_plugin.h
View file

@ -370,7 +370,7 @@ public:
app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); }
app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
@ -378,7 +378,7 @@ public:
app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); }
app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }

56
src/ast/ast.cpp
View file

@ -1289,7 +1289,7 @@ decl_kind user_sort_plugin::register_name(symbol s) {
decl_plugin * user_sort_plugin::mk_fresh() {
user_sort_plugin * p = alloc(user_sort_plugin);
for (symbol const& s : m_sort_names)
for (symbol const& s : m_sort_names)
p->register_name(s);
return p;
}
@ -1415,7 +1415,7 @@ ast_manager::~ast_manager() {
p->finalize();
}
for (decl_plugin* p : m_plugins) {
if (p)
if (p)
dealloc(p);
}
m_plugins.reset();
@ -1454,13 +1454,13 @@ ast_manager::~ast_manager() {
mark_array_ref(mark, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
mark_array_ref(mark, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
break;
}
}
}
}
for (ast * n : m_ast_table) {
if (!mark.is_marked(n)) {
roots.push_back(n);
}
}
}
SASSERT(!roots.empty());
for (unsigned i = 0; i < roots.size(); ++i) {
ast* a = roots[i];
@ -1492,11 +1492,8 @@ void ast_manager::compact_memory() {
unsigned capacity = m_ast_table.capacity();
if (capacity > 4*m_ast_table.size()) {
ast_table new_ast_table;
ast_table::iterator it = m_ast_table.begin();
ast_table::iterator end = m_ast_table.end();
for (; it != end; ++it) {
new_ast_table.insert(*it);
}
for (ast* curr : m_ast_table)
new_ast_table.insert(curr);
m_ast_table.swap(new_ast_table);
IF_VERBOSE(10, verbose_stream() << "(ast-table :prev-capacity " << capacity
<< " :capacity " << m_ast_table.capacity() << " :size " << m_ast_table.size() << ")\n";);
@ -1510,10 +1507,7 @@ void ast_manager::compress_ids() {
ptr_vector<ast> asts;
m_expr_id_gen.cleanup();
m_decl_id_gen.cleanup(c_first_decl_id);
ast_table::iterator it = m_ast_table.begin();
ast_table::iterator end = m_ast_table.end();
for (; it != end; ++it) {
ast * n = *it;
for (ast * n : m_ast_table) {
if (is_decl(n))
n->m_id = m_decl_id_gen.mk();
else
@ -1521,10 +1515,8 @@ void ast_manager::compress_ids() {
asts.push_back(n);
}
m_ast_table.finalize();
ptr_vector<ast>::iterator it2 = asts.begin();
ptr_vector<ast>::iterator end2 = asts.end();
for (; it2 != end2; ++it2)
m_ast_table.insert(*it2);
for (ast* a : asts)
m_ast_table.insert(a);
}
void ast_manager::raise_exception(char const * msg) {
@ -1570,20 +1562,15 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
}
void ast_manager::set_next_expr_id(unsigned id) {
while (true) {
id = m_expr_id_gen.set_next_id(id);
ast_table::iterator it = m_ast_table.begin();
ast_table::iterator end = m_ast_table.end();
for (; it != end; ++it) {
ast * curr = *it;
if (curr->get_id() == id)
break;
try_again:
id = m_expr_id_gen.set_next_id(id);
for (ast * curr : m_ast_table) {
if (curr->get_id() == id) {
// id is in use, move to the next one.
++id;
goto try_again;
}
if (it == end)
return;
// id is in use, move to the next one.
id++;
}
}
}
unsigned ast_manager::get_node_size(ast const * n) { return ::get_node_size(n); }
@ -1683,7 +1670,7 @@ ast * ast_manager::register_node_core(ast * n) {
bool contains = m_ast_table.contains(n);
CASSERT("nondet_bug", contains || slow_not_contains(n));
#endif
ast * r = m_ast_table.insert_if_not_there(n);
SASSERT(r->m_hash == h);
if (r != n) {
@ -2358,8 +2345,9 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort *
unsigned num_patterns, expr * const * patterns,
unsigned num_no_patterns, expr * const * no_patterns) {
SASSERT(body);
SASSERT(num_patterns == 0 || num_no_patterns == 0);
SASSERT(num_decls > 0);
if (num_patterns != 0 && num_no_patterns != 0)
throw ast_exception("simultaneous patterns and no-patterns not supported");
DEBUG_CODE({
for (unsigned i = 0; i < num_patterns; ++i) {
TRACE("ast", tout << i << " " << mk_pp(patterns[i], *this) << "\n";);
@ -2763,7 +2751,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
}
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) {
if (num_proofs == 0)
if (num_proofs == 0)
return nullptr;
if (num_proofs == 1)
return proofs[0];

22
src/ast/ast.h
View file

@ -53,6 +53,12 @@ Revision History:
#pragma warning(disable : 4355)
#endif
#ifdef _MSC_VER
# define Z3_NORETURN __declspec(noreturn)
#else
# define Z3_NORETURN [[noreturn]]
#endif
class ast;
class ast_manager;
@ -330,7 +336,7 @@ std::ostream& operator<<(std::ostream& out, sort_size const & ss);
// -----------------------------------
/**
\brief Extra information that may be attached to intepreted sorts.
\brief Extra information that may be attached to interpreted sorts.
*/
class sort_info : public decl_info {
sort_size m_num_elements;
@ -932,7 +938,7 @@ struct builtin_name {
};
/**
\brief Each family of intepreted function declarations and sorts must provide a plugin
\brief Each family of interpreted function declarations and sorts must provide a plugin
to build sorts and decls of the family.
*/
class decl_plugin {
@ -1059,7 +1065,7 @@ protected:
ptr_vector<func_decl> m_eq_decls; // cached eqs
ptr_vector<func_decl> m_ite_decls; // cached ites
ptr_vector<func_decl> m_oeq_decls; // cached obsevational eqs
ptr_vector<func_decl> m_oeq_decls; // cached observational eqs
sort * m_proof_sort;
func_decl * m_undef_decl;
func_decl * m_true_pr_decl;
@ -1161,7 +1167,7 @@ public:
virtual expr * get_some_value(sort * s);
};
typedef app proof; /* a proof is just an applicaton */
typedef app proof; /* a proof is just an application */
// -----------------------------------
//
@ -1220,7 +1226,7 @@ enum pattern_op_kind {
/**
\brief Patterns are used to group expressions. These expressions are using during E-matching for
heurisitic quantifier instantiation.
heuristic quantifier instantiation.
*/
class pattern_decl_plugin : public decl_plugin {
public:
@ -1245,13 +1251,13 @@ enum model_value_op_kind {
/**
\brief Values are used during model construction. All values are
assumed to be different. Users should not use them, since they may
introduce unsoundess if the sort of a value is finite.
introduce unsoundness if the sort of a value is finite.
Moreover, values should never be internalized in a logical context.
However, values can be used during evaluation (i.e., simplification).
\remark Model values can be viewed as the partion ids in Z3 1.x.
\remark Model values can be viewed as the partition ids in Z3 1.x.
*/
class model_value_decl_plugin : public decl_plugin {
public:
@ -1515,7 +1521,7 @@ public:
void compress_ids();
// Equivalent to throw ast_exception(msg)
void raise_exception(char const * msg);
Z3_NORETURN void raise_exception(char const * msg);
bool is_format_manager() const { return m_format_manager == 0; }

115
src/ast/ast_smt_pp.cpp
View file

@ -340,8 +340,7 @@ class smt_printer {
}
void pp_arg(expr *arg, app *parent)
{
void pp_arg(expr *arg, app *parent) {
pp_marked_expr(arg);
}
@ -417,7 +416,7 @@ class smt_printer {
else if (m_simplify_implies && m_manager.is_implies(decl) && m_manager.is_implies(n->get_arg(1))) {
expr *curr = n;
expr *arg;
m_out << "(implies (and";
m_out << "(=> (and";
while (m_manager.is_implies(curr)) {
arg = to_app(curr)->get_arg(0);
@ -476,9 +475,8 @@ class smt_printer {
}
}
void print_no_lets(expr *e)
{
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, true, m_indent, m_num_var_names, m_var_names);
void print_no_lets(expr *e) {
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
p(e);
}
@ -511,7 +509,7 @@ class smt_printer {
m_out << "(! ";
}
{
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
p(q->get_expr());
}
@ -704,7 +702,7 @@ class smt_printer {
public:
smt_printer(std::ostream& out, ast_manager& m, ptr_vector<quantifier>& ql, smt_renaming& rn,
symbol logic, bool no_lets, bool is_smt2, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) :
symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) :
m_out(out),
m_manager(m),
m_qlists(ql),
@ -894,25 +892,17 @@ ast_smt_pp::ast_smt_pp(ast_manager& m):
m_simplify_implies(true)
{}
void ast_smt_pp::display_expr(std::ostream& strm, expr* n) {
ptr_vector<quantifier> ql;
smt_renaming rn;
smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0);
p(n);
}
void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent, unsigned num_var_names, char const* const* var_names) {
ptr_vector<quantifier> ql;
smt_renaming rn;
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
p(n);
}
void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) {
ptr_vector<quantifier> ql;
smt_renaming rn;
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
if (is_expr(a)) {
p(to_expr(a));
}
@ -1021,92 +1011,3 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
p(n);
}
}
void ast_smt_pp::display(std::ostream& strm, expr* n) {
ptr_vector<quantifier> ql;
decl_collector decls(m_manager);
smt_renaming rn;
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
decls.visit(m_assumptions[i].get());
}
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
decls.visit(m_assumptions_star[i].get());
}
decls.visit(n);
strm << "(benchmark ";
if (m_benchmark_name != symbol::null) {
strm << m_benchmark_name << "\n";
}
else {
strm << "unnamed\n";
}
if (m_source_info != symbol::null && m_source_info != symbol("")) {
strm << ":source { " << m_source_info << " }\n";
}
strm << ":status " << m_status << "\n";
if (m_category != symbol::null && m_category != symbol("")) {
strm << ":category { " << m_category << " }\n";
}
if (m_logic != symbol::null && m_logic != symbol("")) {
strm << ":logic " << m_logic << "\n";
}
if (m_attributes.size() > 0) {
strm << m_attributes.c_str();
}
ast_mark sort_mark;
for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
sort* s = decls.get_sorts()[i];
if (!(*m_is_declared)(s)) {
smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0);
p.pp_sort_decl(sort_mark, s);
}
}
for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
func_decl* d = decls.get_func_decls()[i];
if (!(*m_is_declared)(d)) {
strm << ":extrafuns (";
smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0);
p(d);
strm << ")\n";
}
}
for (unsigned i = 0; i < decls.get_num_preds(); ++i) {
func_decl* d = decls.get_pred_decls()[i];
if (!(*m_is_declared)(d)) {
strm << ":extrapreds (";
smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0);
p.visit_pred(d);
strm << ")\n";
}
}
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
expr * e = m_assumptions[i].get();
strm << ":assumption\n";
smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0);
p(e);
strm << "\n";
}
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
strm << ":assumption-core\n";
smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0);
p(m_assumptions_star[i].get());
strm << "\n";
}
{
strm << ":formula\n";
smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0);
p(n);
strm << "\n";
}
strm << ")\n";
}

2
src/ast/ast_smt_pp.h
View file

@ -75,9 +75,7 @@ public:
void set_is_declared(is_declared* id) { m_is_declared = id; }
void display(std::ostream& strm, expr* n);
void display_smt2(std::ostream& strm, expr* n);
void display_expr(std::ostream& strm, expr* n);
void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);

4
src/ast/proofs/proof_checker.cpp
View file

@ -502,7 +502,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false;
}
case PR_HYPOTHESIS: {
// TBD all branches with hyptheses must be closed by a later lemma.
// TBD all branches with hypotheses must be closed by a later lemma.
if (match_proof(p) &&
match_fact(p, fml)) {
return true;
@ -1284,7 +1284,7 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
pp.add_assumption(antecedents[i]);
expr_ref n(m);
n = m.mk_not(consequent);
pp.display(out, n);
pp.display_smt2(out, n);
out.close();
m_proof_lemma_id++;
}

1
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -1193,7 +1193,6 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
return false;
}
SASSERT(out_bits.empty());
ptr_buffer<expr, 128> na_bits;
na_bits.append(sz, a_bits);
ptr_buffer<expr, 128> nb_bits;

14
src/ast/static_features.cpp
View file

@ -111,16 +111,6 @@ void static_features::flush_cache() {
m_expr2formula_depth.reset();
}
#if 0
bool static_features::is_non_linear(expr * e) const {
if (!is_arith_expr(e))
return false;
if (is_numeral(e))
return true;
if (m_autil.is_add(e))
return true; // the non
}
#endif
bool static_features::is_diff_term(expr const * e, rational & r) const {
// lhs can be 'x' or '(+ k x)'
@ -301,10 +291,12 @@ void static_features::update_core(expr * e) {
m_num_interpreted_constants++;
}
if (fid == m_afid) {
// std::cout << mk_pp(e, m_manager) << "\n";
switch (to_app(e)->get_decl_kind()) {
case OP_MUL:
if (!is_numeral(to_app(e)->get_arg(0)))
if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) {
m_num_non_linear++;
}
break;
case OP_DIV:
case OP_IDIV:

7
src/cmd_context/cmd_context.cpp
View file

@ -339,6 +339,13 @@ void ast_object_ref::finalize(cmd_context & ctx) {
ctx.m().dec_ref(m_ast);
}
void stream_ref::set(std::ostream& out) {
reset();
m_owner = false;
m_name = "caller-owned";
m_stream = &out;
}
void stream_ref::set(char const * name) {
if (!name) {
throw cmd_exception("invalid stream name");

2
src/cmd_context/cmd_context.h
View file

@ -128,6 +128,7 @@ public:
stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
~stream_ref() { reset(); }
void set(char const * name);
void set(std::ostream& strm);
void reset();
std::ostream & operator*() { return *m_stream; }
char const * name() const { return m_name.c_str(); }
@ -404,6 +405,7 @@ public:
void reset_object_refs();
void reset_user_tactics();
void set_regular_stream(char const * name) { m_regular.set(name); }
void set_regular_stream(std::ostream& out) { m_regular.set(out); }
void set_diagnostic_stream(char const * name);
virtual std::ostream & regular_stream() { return *m_regular; }
virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }

2
src/cmd_context/pdecl.cpp
View file

@ -852,7 +852,7 @@ pdecl_manager::pdecl_manager(ast_manager & m):
pdecl_manager::~pdecl_manager() {
dec_ref(m_list);
reset_sort_info();
SASSERT(m_sort2psort.empty());
SASSERT(m_sort2psort.empty());
SASSERT(m_table.empty());
}

8
src/interp/iz3proof_itp.cpp
View file

@ -55,7 +55,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* The summation rule. The term sum(p,c,i) takes a proof p of an
inequality i', an integer coefficient c and an inequality i, and
yieds a proof of i' + ci. */
yields a proof of i' + ci. */
symb sum;
/* Proof rotation. The proof term rotate(q,p) takes a
@ -75,7 +75,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
symb leq2eq;
/* Equality to inequality. eq2leq(p, q) takes a proof p of x=y, and
a proof q ~(x <= y) and and yields a proof of false. */
a proof q ~(x <= y) and yields a proof of false. */
symb eq2leq;
/* Proof term cong(p,q) takes a proof p of x=y and a proof
@ -97,7 +97,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
/* This oprerator represents a concatenation of rewrites. The term
a=b;c=d represents an A rewrite from a to b, followed by a B
rewrite fron b to c, followed by an A rewrite from c to d.
rewrite from b to c, followed by an A rewrite from c to d.
*/
symb concat;
@ -1542,7 +1542,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
return my_implies(arg(rew,1),arg(rew,2));
}
// make rewrite rew conditon on rewrite cond
// make rewrite rew condition on rewrite cond
ast rewrite_conditional(const ast &cond, const ast &rew){
ast cf = rewrite_to_formula(cond);
return make(sym(rew),arg(rew,0),my_and(arg(rew,1),cf),arg(rew,2));

2
src/interp/iz3translate_direct.cpp
View file

@ -9,7 +9,7 @@
Translate a Z3 proof into the interpolating proof calculus.
Translation is direct, without transformations on the target proof
representaiton.
representation.
Author:

93
src/math/polynomial/polynomial.cpp
View file

@ -150,7 +150,6 @@ namespace polynomial {
return r;
}
/**
\brief Monomials (power products)
*/
@ -192,7 +191,7 @@ namespace polynomial {
};
static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz * sizeof(power); }
monomial(unsigned id, unsigned sz, power const * pws, unsigned h):
m_ref_count(0),
m_id(id),
@ -257,9 +256,7 @@ namespace polynomial {
if (m_size < SMALL_MONOMIAL) {
// use linear search for small monomials
// search backwards since we usually ask for the degree of "big" variables
unsigned i = last;
while (i > 0) {
--i;
for (unsigned i = last; i-- > 0; ) {
if (get_var(i) == x)
return i;
}
@ -798,9 +795,8 @@ namespace polynomial {
dec_ref(m_unit);
CTRACE("polynomial", !m_monomials.empty(),
tout << "monomials leaked\n";
monomial_table::iterator it = m_monomials.begin(); monomial_table::iterator end = m_monomials.end();
for (; it != end; ++it) {
(*it)->display(tout); tout << "\n";
for (auto * m : m_monomials) {
m->display(tout); tout << "\n";
});
SASSERT(m_monomials.empty());
if (m_own_allocator)
@ -1510,6 +1506,8 @@ namespace polynomial {
unsigned id() const { return m_id; }
unsigned size() const { return m_size; }
monomial * m(unsigned idx) const { SASSERT(idx < size()); return m_ms[idx]; }
monomial *const* begin() const { return m_ms; }
monomial *const* end() const { return m_ms + size(); }
numeral const & a(unsigned idx) const { SASSERT(idx < size()); return m_as[idx]; }
numeral & a(unsigned idx) { SASSERT(idx < size()); return m_as[idx]; }
numeral const * as() const { return m_as; }
@ -1773,11 +1771,9 @@ namespace polynomial {
}
bool manager::is_linear(polynomial const * p) {
unsigned sz = p->size();
for (unsigned i = 0; i < sz; i++) {
if (!is_linear(p->m(0)))
for (monomial* m : *p)
if (!is_linear(m))
return false;
}
return true;
}
@ -2396,6 +2392,7 @@ namespace polynomial {
return mm().is_valid(x);
}
void add_del_eh(del_eh * eh) {
eh->m_next = m_del_eh;
m_del_eh = eh;
@ -6101,6 +6098,33 @@ namespace polynomial {
});
}
lbool sign(monomial* m, numeral const& c, svector<lbool> const& sign_of_vars) {
unsigned sz = size(m);
lbool sign1 = m_manager.is_pos(c) ? l_true : l_false;
for (unsigned i = 0; i < sz; ++i) {
var v = get_var(m, i);
unsigned d = degree(m, i);
lbool sign2 = sign_of_vars.get(v, l_undef);
if (sign2 == l_undef)
return l_undef;
else if (1 == (d % 2) && sign2 == l_false) {
sign1 = sign1 == l_true ? l_false : l_true;
}
}
return sign1;
}
lbool sign(polynomial const * p, svector<lbool> const& sign_of_vars) {
unsigned sz = size(p);
if (sz == 0) return l_undef;
lbool sign1 = sign(p->m(0), p->a(0), sign_of_vars);
for (unsigned i = 1; sign1 != l_undef && i < sz; ++i) {
if (sign(p->m(i), p->a(i), sign_of_vars) != sign1)
return l_undef;
}
return sign1;
}
bool is_pos(polynomial const * p) {
bool found_unit = false;
unsigned sz = p->size();
@ -6372,6 +6396,31 @@ namespace polynomial {
R.add(new_a, mk_monomial(new_m));
}
return R.mk();
}
void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) {
unsigned md = degree(r, x);
if (md == 0) {
result = const_cast<polynomial*>(r);
return;
}
result = 0;
polynomial_ref p1(pm()), q1(pm());
polynomial_ref_buffer ps(pm());
unsigned sz = r->size();
for (unsigned i = 0; i < sz; i++) {
monomial * m0 = r->m(i);
unsigned dm = m0->degree_of(x);
SASSERT(md >= dm);
monomial_ref m1(div_x(m0, x), pm());
pw(p, dm, p1);
pw(q, md - dm, q1);
p1 = mul(r->a(i), m1, p1 * q1);
if (result)
result = add(result, p1);
else
result = p1;
}
}
@ -6918,6 +6967,18 @@ namespace polynomial {
return m_imp->m().set_zp(p);
}
bool manager::is_var(polynomial const* p, var& v) {
return p->size() == 1 && is_var(p->m(0), v) && m_imp->m().is_one(p->a(0));
}
bool manager::is_var(monomial const* m, var& v) {
return m->size() == 1 && m->degree(0) == 1 && (v = m->get_var(0), true);
}
bool manager::is_var_num(polynomial const* p, var& v, scoped_numeral& n) {
return p->size() == 2 && m_imp->m().is_one(p->a(0)) && is_var(p->m(0), v) && is_unit(p->m(1)) && (n = p->a(1), true);
}
small_object_allocator & manager::allocator() const {
return m_imp->mm().allocator();
}
@ -7271,6 +7332,10 @@ namespace polynomial {
void manager::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) {
m_imp->psc_chain(p, q, x, S);
}
lbool manager::sign(polynomial const * p, svector<lbool> const& sign_of_vars) {
return m_imp->sign(p, sign_of_vars);
}
bool manager::is_pos(polynomial const * p) {
return m_imp->is_pos(p);
@ -7307,6 +7372,10 @@ namespace polynomial {
polynomial * manager::substitute(polynomial const * p, unsigned xs_sz, var const * xs, numeral const * vs) {
return m_imp->substitute(p, xs_sz, xs, vs);
}
void manager::substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) {
m_imp->substitute(r, x, p, q, result);
}
void manager::factor(polynomial const * p, factors & r, factor_params const & params) {
m_imp->factor(p, r, params);

35
src/math/polynomial/polynomial.h
View file

@ -29,6 +29,7 @@ Notes:
#include "util/params.h"
#include "util/mpbqi.h"
#include "util/rlimit.h"
#include "util/lbool.h"
class small_object_allocator;
@ -98,7 +99,7 @@ namespace polynomial {
};
struct display_var_proc {
virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
virtual std::ostream& operator()(std::ostream & out, var x) const { return out << "x" << x; }
};
class polynomial;
@ -306,12 +307,27 @@ namespace polynomial {
\brief Return true if m is linear (i.e., it is of the form 1 or x).
*/
static bool is_linear(monomial const * m);
/**
\brief Return true if all monomials in p are linear.
*/
static bool is_linear(polynomial const * p);
/**
\brief Return true if the monomial is a variable.
*/
static bool is_var(monomial const* p, var& v);
/**
\brief Return true if the polynomial is a variable.
*/
bool is_var(polynomial const* p, var& v);
/**
\brief Return true if the polynomial is of the form x + k
*/
bool is_var_num(polynomial const* p, var& v, scoped_numeral& n);
/**
\brief Return the degree of variable x in p.
*/
@ -860,7 +876,13 @@ namespace polynomial {
\brief Return true if p is a square, and store its square root in r.
*/
bool sqrt(polynomial const * p, polynomial_ref & r);
/**
\brief obtain the sign of the polynomial given sign of variables.
*/
lbool sign(polynomial const* p, svector<lbool> const& sign_of_vars);
/**
\brief Return true if p is always positive for any assignment of its variables.
@ -936,6 +958,13 @@ namespace polynomial {
return substitute(p, 1, &x, &v);
}
/**
\brief Apply substiution [x -> p/q] in r.
That is, given r \in Z[x, y_1, .., y_m] return
polynomial q^k * r(p/q, y_1, .., y_m), where k is the maximal degree of x in r.
*/
void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result);
/**
\brief Factorize the given polynomial p and store its factors in r.
*/

2
src/math/simplex/simplex_def.h
View file

@ -634,7 +634,7 @@ namespace simplex {
//
// max { c*x | A*x = 0 and l <= x <= u }
//
// start with feasible assigment
// start with feasible assignment
// A*x0 = 0 and l <= x0 <= u
//
// Identify pivot: i, j: such that x_i is base,

2
src/muz/rel/dl_compiler.h
View file

@ -60,7 +60,7 @@ namespace datalog {
ACK_UNBOUND_VAR(var_index) - encodes that the column contains a variable that
is unbound (by the corresponding rule body),
var_index is the de-Brujin index (var->get_idx())
var_index is the de-Bruijn index (var->get_idx())
of the variable associated with the column.
ACK_CONSTANT(constant) - encodes that the column contains the constant.

2
src/muz/rel/dl_relation_manager.h
View file

@ -609,7 +609,7 @@ namespace datalog {
std::string to_nice_string(const relation_element & el) const;
/**
This one may give a nicer representation of \c el than the
\c to_nice_string(const relation_element & el) function, by unsing the information about the sort
\c to_nice_string(const relation_element & el) function, by using the information about the sort
of the element.
*/
std::string to_nice_string(const relation_sort & s, const relation_element & el) const;

2
src/nlsat/nlsat_clause.h
View file

@ -44,6 +44,8 @@ namespace nlsat {
bool is_learned() const { return m_learned; }
literal * begin() { return m_lits; }
literal * end() { return m_lits + m_size; }
literal const * begin() const { return m_lits; }
literal const * end() const { return m_lits + m_size; }
literal const * c_ptr() const { return m_lits; }
void inc_activity() { m_activity++; }
void set_activity(unsigned v) { m_activity = v; }

4
src/nlsat/nlsat_interval_set.cpp
View file

@ -672,14 +672,14 @@ namespace nlsat {
return new_set;
}
void interval_set_manager::peek_in_complement(interval_set const * s, anum & w, bool randomize) {
void interval_set_manager::peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) {
SASSERT(!is_full(s));
if (s == 0) {
if (randomize) {
int num = m_rand() % 2 == 0 ? 1 : -1;
#define MAX_RANDOM_DEN_K 4
int den_k = (m_rand() % MAX_RANDOM_DEN_K);
int den = 1 << den_k;
int den = is_int ? 1 : (1 << den_k);
scoped_mpq _w(m_am.qm());
m_am.qm().set(_w, num, den);
m_am.set(w, _w);

2
src/nlsat/nlsat_interval_set.h
View file

@ -108,7 +108,7 @@ namespace nlsat {
\pre !is_full(s)
*/
void peek_in_complement(interval_set const * s, anum & w, bool randomize);
void peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize);
};
typedef obj_ref<interval_set, interval_set_manager> interval_set_ref;

1
src/nlsat/nlsat_params.pyg
View file

@ -10,6 +10,7 @@ def_module_params('nlsat',
('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."),
('shuffle_vars', BOOL, False, "use a random variable order."),
('inline_vars', BOOL, False, "inline variables that can be isolated from equations"),
('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution.")
))

721
src/nlsat/nlsat_solver.cpp
View file

File diff suppressed because it is too large Load diff

2
src/nlsat/nlsat_solver.h
View file

@ -35,7 +35,7 @@ namespace nlsat {
struct imp;
imp * m_imp;
public:
solver(reslimit& rlim, params_ref const & p);
solver(reslimit& rlim, params_ref const & p, bool incremental);
~solver();
/**

7
src/nlsat/nlsat_types.h
View file

@ -47,6 +47,8 @@ namespace nlsat {
typedef polynomial::var_vector var_vector;
typedef polynomial::manager pmanager;
typedef polynomial::polynomial poly;
typedef polynomial::monomial monomial;
typedef polynomial::numeral numeral;
const var null_var = polynomial::null_var;
const var true_bool_var = 0;
@ -148,10 +150,7 @@ namespace nlsat {
typedef algebraic_numbers::anum anum;
typedef algebraic_numbers::manager anum_manager;
class solver_exception : public default_exception {
public:
solver_exception(char const * msg):default_exception(msg) {}
};
typedef default_exception solver_exception;
class assignment;

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

@ -32,11 +32,11 @@ class nlsat_tactic : public tactic {
ast_manager & m;
expr_ref_vector m_var2expr;
expr_display_var_proc(ast_manager & _m):m(_m), m_var2expr(_m) {}
virtual void operator()(std::ostream & out, nlsat::var x) const {
virtual std::ostream& operator()(std::ostream & out, nlsat::var x) const {
if (x < m_var2expr.size())
out << mk_ismt2_pp(m_var2expr.get(x), m);
return out << mk_ismt2_pp(m_var2expr.get(x), m);
else
out << "x!" << x;
return out << "x!" << x;
}
};
@ -51,7 +51,7 @@ class nlsat_tactic : public tactic {
m(_m),
m_params(p),
m_display_var(_m),
m_solver(m.limit(), p) {
m_solver(m.limit(), p, false) {
}
void updt_params(params_ref const & p) {

4
src/nlsat/tactic/qfnra_nlsat_tactic.cpp
View file

@ -48,11 +48,15 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
purify_p),
mk_propagate_values_tactic(m, p),
mk_solve_eqs_tactic(m, p),
using_params(mk_purify_arith_tactic(m, p),
purify_p),
mk_elim_uncnstr_tactic(m, p),
mk_elim_term_ite_tactic(m, p)),
and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
factor,
mk_solve_eqs_tactic(m, p),
using_params(mk_purify_arith_tactic(m, p),
purify_p),
using_params(mk_simplify_tactic(m, p),
main_p),
mk_tseitin_cnf_core_tactic(m, p),

1
src/opt/CMakeLists.txt
View file

@ -6,6 +6,7 @@ z3_add_component(opt
opt_cmds.cpp
opt_context.cpp
opt_pareto.cpp
opt_parse.cpp
optsmt.cpp
opt_solver.cpp
pb_sls.cpp

22
src/opt/opt_context.cpp
View file

@ -345,12 +345,24 @@ namespace opt {
fix_model(mdl);
}
bool context::contains_quantifiers() const {
for (expr* f : m_hard_constraints) {
if (has_quantifiers(f)) return true;
}
return false;
}
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
if (scoped) get_solver().push();
lbool result = m_optsmt.lex(index, is_max);
if (result == l_true) m_optsmt.get_model(m_model, m_labels);
if (scoped) get_solver().pop(1);
if (result == l_true && committed) m_optsmt.commit_assignment(index);
if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
throw default_exception("unbounded objectives on quantified constraints is not supported");
result = l_undef;
}
return result;
}
@ -646,8 +658,7 @@ namespace opt {
expr_fast_mark1 visited;
is_bv proc(m);
try {
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective & obj = m_objectives[i];
for (objective& obj : m_objectives) {
if (obj.m_type != O_MAXSMT) return false;
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < ms.size(); ++j) {
@ -658,8 +669,8 @@ namespace opt {
for (unsigned i = 0; i < sz; i++) {
quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
}
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
for (expr* f : m_hard_constraints) {
quick_for_each_expr(proc, visited, f);
}
}
catch (is_bv::found) {
@ -1224,6 +1235,9 @@ namespace opt {
}
void context::display_assignment(std::ostream& out) {
if (m_scoped_state.m_objectives.size() != m_objectives.size()) {
throw default_exception("check-sat has not been called with latest objectives");
}
out << "(objectives\n";
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_scoped_state.m_objectives[i];

3
src/opt/opt_context.h
View file

@ -233,13 +233,14 @@ namespace opt {
private:
lbool execute(objective const& obj, bool committed, bool scoped);
lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
lbool execute_lex();
lbool execute_box();
lbool execute_pareto();
lbool adjust_unknown(lbool r);
bool scoped_lex();
bool contains_quantifiers() const;
expr_ref to_expr(inf_eps const& n);
void to_exprs(inf_eps const& n, expr_ref_vector& es);

317
src/opt/opt_parse.cpp Normal file
View file

@ -0,0 +1,317 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
opt_parse.cpp
Abstract:
Parse utilities for optimization.
Author:
Nikolaj Bjorner (nbjorner) 2017-11-19
Revision History:
--*/
#include "opt/opt_context.h"
#include "opt/opt_parse.h"
class opt_stream_buffer {
std::istream & m_stream;
int m_val;
unsigned m_line;
public:
opt_stream_buffer(std::istream & s):
m_stream(s),
m_line(0) {
m_val = m_stream.get();
}
int operator *() const { return m_val;}
void operator ++() { m_val = m_stream.get(); }
int ch() const { return m_val; }
void next() { m_val = m_stream.get(); }
bool eof() const { return ch() == EOF; }
unsigned line() const { return m_line; }
void skip_whitespace();
void skip_space();
void skip_line();
bool parse_token(char const* token);
int parse_int();
unsigned parse_unsigned();
};
void opt_stream_buffer::skip_whitespace() {
while ((ch() >= 9 && ch() <= 13) || ch() == 32) {
if (ch() == 10) ++m_line;
next();
}
}
void opt_stream_buffer::skip_space() {
while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) {
next();
}
}
void opt_stream_buffer::skip_line() {
while(true) {
if (eof()) {
return;
}
if (ch() == '\n') {
++m_line;
next();
return;
}
next();
}
}
bool opt_stream_buffer::parse_token(char const* token) {
skip_whitespace();
char const* t = token;
while (ch() == *t) {
next();
++t;
}
return 0 == *t;
}
unsigned opt_stream_buffer::parse_unsigned() {
skip_space();
if (ch() == '\n') {
return UINT_MAX;
}
unsigned val = 0;
while (ch() >= '0' && ch() <= '9') {
val = val*10 + (ch() - '0');
next();
}
return val;
}
int opt_stream_buffer::parse_int() {
int val = 0;
bool neg = false;
skip_whitespace();
if (ch() == '-') {
neg = true;
next();
}
else if (ch() == '+') {
next();
}
if (ch() < '0' || ch() > '9') {
std::cerr << "(error line " << line() << " \"unexpected char: " << ((char)ch()) << "\" )\n";
exit(3);
}
while (ch() >= '0' && ch() <= '9') {
val = val*10 + (ch() - '0');
next();
}
return neg ? -val : val;
}
class wcnf {
opt::context& opt;
ast_manager& m;
opt_stream_buffer& in;
unsigned_vector& m_handles;
app_ref read_clause(unsigned& weight) {
int parsed_lit;
int var;
weight = in.parse_unsigned();
app_ref result(m), p(m);
expr_ref_vector ors(m);
while (true) {
parsed_lit = in.parse_int();
if (parsed_lit == 0)
break;
var = abs(parsed_lit);
p = m.mk_const(symbol(var), m.mk_bool_sort());
if (parsed_lit < 0) p = m.mk_not(p);
ors.push_back(p);
}
result = to_app(mk_or(m, ors.size(), ors.c_ptr()));
return result;
}
void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
in.parse_token("wcnf");
num_vars = in.parse_unsigned();
num_clauses = in.parse_unsigned();
max_weight = in.parse_unsigned();
}
public:
wcnf(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h): opt(opt), m(opt.get_manager()), in(in), m_handles(h) {
opt.set_clausal(true);
}
void parse() {
unsigned num_vars = 0, num_clauses = 0, max_weight = 0;
while (true) {
in.skip_whitespace();
if (in.eof()) {
break;
}
else if (*in == 'c') {
in.skip_line();
}
else if (*in == 'p') {
++in;
parse_spec(num_vars, num_clauses, max_weight);
}
else {
unsigned weight = 0;
app_ref cls = read_clause(weight);
if (weight >= max_weight) {
opt.add_hard_constraint(cls);
}
else {
unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
if (m_handles.empty()) {
m_handles.push_back(id);
}
}
}
}
}
};
class opb {
opt::context& opt;
ast_manager& m;
opt_stream_buffer& in;
unsigned_vector& m_handles;
arith_util arith;
app_ref parse_id() {
bool negated = in.parse_token("~");
if (!in.parse_token("x")) {
std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\" expected \"x\")\n";
exit(3);
}
app_ref p(m);
int id = in.parse_int();
p = m.mk_const(symbol(id), m.mk_bool_sort());
if (negated) p = m.mk_not(p);
in.skip_whitespace();
return p;
}
app_ref parse_ids() {
app_ref result = parse_id();
while (*in == '~' || *in == 'x') {
result = m.mk_and(result, parse_id());
}
return result;
}
rational parse_coeff_r() {
in.skip_whitespace();
svector<char> num;
bool pos = true;
if (*in == '-') pos = false, ++in;
if (*in == '+') ++in;
if (!pos) num.push_back('-');
in.skip_whitespace();
while ('0' <= *in && *in <='9') num.push_back(*in), ++in;
num.push_back(0);
return rational(num.c_ptr());
}
app_ref parse_coeff() {
return app_ref(arith.mk_numeral(parse_coeff_r(), true), m);
}
app_ref parse_term() {
app_ref c = parse_coeff();
app_ref e = parse_ids();
return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m);
}
void parse_objective(bool is_min) {
app_ref t = parse_term();
while (!in.parse_token(";") && !in.eof()) {
if (is_min) {
t = arith.mk_add(t, parse_term());
}
else {
t = arith.mk_sub(t, parse_term());
}
}
m_handles.push_back(opt.add_objective(t, false));
}
void parse_constraint() {
app_ref t = parse_term();
while (!in.eof()) {
if (in.parse_token(">=")) {
t = arith.mk_ge(t, parse_coeff());
in.parse_token(";");
break;
}
if (in.parse_token("=")) {
t = m.mk_eq(t, parse_coeff());
in.parse_token(";");
break;
}
if (in.parse_token("<=")) {
t = arith.mk_le(t, parse_coeff());
in.parse_token(";");
break;
}
t = arith.mk_add(t, parse_term());
}
opt.add_hard_constraint(t);
}
public:
opb(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h):
opt(opt), m(opt.get_manager()),
in(in), m_handles(h), arith(m) {}
void parse() {
while (true) {
in.skip_whitespace();
if (in.eof()) {
break;
}
else if (*in == '*') {
in.skip_line();
}
else if (in.parse_token("min:")) {
parse_objective(true);
}
else if (in.parse_token("max:")) {
parse_objective(false);
}
else {
parse_constraint();
}
}
}
};
void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h) {
opt_stream_buffer _is(is);
wcnf w(opt, _is, h);
w.parse();
}
void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) {
opt_stream_buffer _is(is);
opb opb(opt, _is, h);
opb.parse();
}

28
src/opt/opt_parse.h Normal file
View file

@ -0,0 +1,28 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
opt_parse.h
Abstract:
Parse utilities for optimization.
Author:
Nikolaj Bjorner (nbjorner) 2017-11-19
Revision History:
--*/
#ifndef OPT_PARSE_H_
#define OPT_PARSE_H_
void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h);
void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h);
#endif /* OPT_PARSE_H_ */

8
src/opt/optsmt.cpp
View file

@ -161,6 +161,14 @@ namespace opt {
return l_true;
}
bool optsmt::is_unbounded(unsigned obj_index, bool is_maximize) {
if (is_maximize) {
return !m_upper[obj_index].is_finite();
}
else {
return !m_lower[obj_index].is_finite();
}
}
lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
arith_util arith(m);

2
src/opt/optsmt.h
View file

@ -49,6 +49,8 @@ namespace opt {
lbool lex(unsigned obj_index, bool is_maximize);
bool is_unbounded(unsigned obj_index, bool is_maximize);
unsigned add(app* t);
void updt_params(params_ref& p);

8
src/parsers/smt/CMakeLists.txt
View file

@ -1,8 +0,0 @@
z3_add_component(smtparser
SOURCES
smtlib.cpp
smtlib_solver.cpp
smtparser.cpp
COMPONENT_DEPENDENCIES
portfolio
)

258
src/parsers/smt/smtlib.cpp
View file

@ -1,258 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
#include "parsers/smt/smtlib.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt2_pp.h"
#ifdef _WINDOWS
#ifdef ARRAYSIZE
#undef ARRAYSIZE
#endif
#include <windows.h>
#include <strsafe.h>
#endif
#include <iostream>
using namespace smtlib;
// --------------------------------------------------------------------------
// symtable
symtable::~symtable() {
reset();
}
void symtable::reset() {
svector<ptr_vector<func_decl>*> range;
m_ids.get_range(range);
for (unsigned i = 0; i < range.size(); ++i) {
ptr_vector<func_decl> const & v = *range[i];
for (unsigned j = 0; j < v.size(); ++j) {
m_manager.dec_ref(v[j]);
}
dealloc(range[i]);
}
m_ids.reset();
ptr_vector<sort> sorts;
m_sorts1.get_range(sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
m_manager.dec_ref(sorts[i]);
}
m_sorts1.reset();
ptr_vector<sort_builder> sort_builders;
m_sorts.get_range(sort_builders);
for (unsigned i = 0; i < sort_builders.size(); ++i) {
dealloc(sort_builders[i]);
}
m_sorts.reset();
}
void symtable::insert(symbol s, func_decl * d) {
ptr_vector<func_decl>* decls = 0;
m_manager.inc_ref(d);
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
decls = alloc(ptr_vector<func_decl>);
decls->push_back(d);
m_ids.insert(s, decls);
}
else {
SASSERT(decls);
if ((*decls)[0] != d) {
decls->push_back(d);
}
else {
m_manager.dec_ref(d);
}
}
}
bool symtable::find1(symbol s, func_decl*& d) {
ptr_vector<func_decl>* decls = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls && !decls->empty());
d = (*decls)[0];
return true;
}
bool symtable::find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d) {
ptr_vector<func_decl>* decls = 0;
d = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls);
for (unsigned i = 0; i < decls->size(); ++i) {
func_decl* decl = (*decls)[i];
if (decl->is_associative() && decl->get_arity() > 0) {
for (unsigned j = 0; j < dom.size(); ++j) {
if (dom[j] != decl->get_domain(0)) {
goto try_next;
}
}
d = decl;
return true;
}
if (decl->get_arity() != dom.size()) {
goto try_next;
}
for (unsigned j = 0; j < decl->get_arity(); ++j) {
if (decl->get_domain(j) != dom[j]) {
goto try_next;
}
}
d = decl;
return true;
try_next:
if (decl->get_family_id() == m_manager.get_basic_family_id() && decl->get_decl_kind() == OP_DISTINCT) {
// we skip type checking for 'distinct'
d = decl;
return true;
}
}
return false;
}
// Store in result the func_decl that are not attached to any family id.
// That is, the uninterpreted constants and function declarations.
void symtable::get_func_decls(ptr_vector<func_decl> & result) const {
svector<ptr_vector<func_decl>*> tmp;
m_ids.get_range(tmp);
svector<ptr_vector<func_decl>*>::const_iterator it = tmp.begin();
svector<ptr_vector<func_decl>*>::const_iterator end = tmp.end();
for (; it != end; ++it) {
ptr_vector<func_decl> * curr = *it;
if (curr) {
ptr_vector<func_decl>::const_iterator it2 = curr->begin();
ptr_vector<func_decl>::const_iterator end2 = curr->end();
for (; it2 != end2; ++it2) {
func_decl * d = *it2;
if (d && d->get_family_id() == null_family_id) {
result.push_back(d);
}
}
}
}
}
void symtable::insert(symbol s, sort_builder* sb) {
m_sorts.insert(s, sb);
}
bool symtable::lookup(symbol s, sort_builder*& sb) {
return m_sorts.find(s, sb);
}
void symtable::push_sort(symbol name, sort* srt) {
m_sorts.begin_scope();
sort_builder* sb = alloc(basic_sort_builder,srt);
m_sorts.insert(name, sb);
m_sorts_trail.push_back(sb);
}
void symtable::pop_sorts(unsigned num_sorts) {
while (num_sorts > 0) {
dealloc(m_sorts_trail.back());
m_sorts_trail.pop_back();
m_sorts.end_scope();
}
}
void symtable::get_sorts(ptr_vector<sort>& result) const {
vector<sort*,false> tmp;
m_sorts1.get_range(tmp);
for (unsigned i = 0; i < tmp.size(); ++i) {
if (tmp[i]->get_family_id() == null_family_id) {
result.push_back(tmp[i]);
}
}
}
// --------------------------------------------------------------------------
// theory
func_decl * theory::declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj) {
func_decl * decl = m_ast_manager.mk_func_decl(id, domain.size(), domain.c_ptr(), range,
is_assoc, is_comm, is_inj);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
sort * theory::declare_sort(symbol const & id) {
sort * decl = m_ast_manager.mk_uninterpreted_sort(id);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
bool theory::get_func_decl(symbol id, func_decl * & decl) {
return m_symtable.find1(id, decl);
}
bool theory::get_sort(symbol id, sort* & s) {
return m_symtable.find(id, s);
}
bool theory::get_const(symbol id, expr * & term) {
func_decl* decl = 0;
if (!get_func_decl(id,decl)) {
return false;
}
if (decl->get_arity() != 0) {
return false;
}
term = m_ast_manager.mk_const(decl);
m_asts.push_back(term);
return true;
}
void benchmark::display_as_smt2(std::ostream & out) const {
if (m_logic != symbol::null)
out << "(set-logic " << m_logic << ")\n";
out << "(set-info :smt-lib-version 2.0)\n";
out << "(set-info :status ";
switch (m_status) {
case SAT: out << "sat"; break;
case UNSAT: out << "unsat"; break;
default: out << "unknown"; break;
}
out << ")\n";
#if 0
ast_manager & m = m_ast_manager;
ptr_vector<func_decl> decls;
m_symtable.get_func_decls(decls);
ptr_vector<func_decl>::const_iterator it = decls.begin();
ptr_vector<func_decl>::const_iterator end = decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
out << "(declare-fun " << f->get_name() << " (";
for (unsigned i = 0; i < f->get_arity(); i++) {
if (i > 0) out << " ";
out << mk_ismt2_pp(f->get_domain(i), m);
}
out << ") " << mk_ismt2_pp(f->get_range(), m);
out << ")\n";
}
#endif
}

232
src/parsers/smt/smtlib.h
View file

@ -1,232 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib.h
Abstract:
SMT library utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-29
Revision History:
--*/
#ifndef SMTLIB_H_
#define SMTLIB_H_
#include "ast/ast.h"
#include "util/symbol_table.h"
#include "util/map.h"
#include "ast/arith_decl_plugin.h"
namespace smtlib {
class sort_builder {
public:
virtual ~sort_builder() {}
virtual bool apply(unsigned num_params, parameter const* params, sort_ref& result) = 0;
virtual char const* error_message() { return ""; }
};
class basic_sort_builder : public sort_builder {
sort* m_sort;
public:
basic_sort_builder(sort* s) : m_sort(s) {}
virtual bool apply(unsigned np, parameter const*, sort_ref& result) {
result = m_sort;
return m_sort && np != 0;
}
};
class symtable {
ast_manager& m_manager;
symbol_table<sort*> m_sorts1;
symbol_table<sort_builder*> m_sorts;
ptr_vector<sort_builder> m_sorts_trail;
symbol_table<ptr_vector<func_decl>* > m_ids;
public:
symtable(ast_manager& m): m_manager(m) {}
~symtable();
void reset();
void insert(symbol s, func_decl * d);
bool find(symbol s, ptr_vector<func_decl> * & decls) {
return m_ids.find(s, decls);
}
bool find1(symbol s, func_decl * & d);
bool find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d);
void insert(symbol s, sort * d) {
sort * d2;
if (m_sorts1.find(s, d2)) {
m_manager.dec_ref(d2);
}
m_manager.inc_ref(d);
m_sorts1.insert(s, d);
}
bool find(symbol s, sort * & d) {
return m_sorts1.find(s, d);
}
void insert(symbol s, sort_builder* sb);
bool lookup(symbol s, sort_builder*& sb);
void push_sort(symbol s, sort*);
void pop_sorts(unsigned num_sorts);
void get_func_decls(ptr_vector<func_decl> & result) const;
void get_sorts(ptr_vector<sort>& result) const;
};
class theory {
public:
typedef ptr_vector<expr>::const_iterator expr_iterator;
theory(ast_manager & ast_manager, symbol const& name):
m_name(name),
m_ast_manager(ast_manager),
m_symtable(ast_manager),
m_asts(ast_manager)
{}
virtual ~theory() {}
symtable * get_symtable() { return &m_symtable; }
void insert(sort * s) { m_symtable.insert(s->get_name(), s); }
void insert(func_decl * c) { m_symtable.insert(c->get_name(), c); }
func_decl * declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj);
sort * declare_sort(symbol const & id);
void add_axiom(expr * axiom) {
m_asts.push_back(axiom);
m_axioms.push_back(axiom);
}
expr_iterator begin_axioms() const {
return m_axioms.begin();
}
unsigned get_num_axioms() const {
return m_axioms.size();
}
expr * const * get_axioms() const {
return m_axioms.c_ptr();
}
expr_iterator end_axioms() const {
return m_axioms.end();
}
void add_assumption(expr * axiom) {
m_asts.push_back(axiom);
m_assumptions.push_back(axiom);
}
unsigned get_num_assumptions() const {
return m_assumptions.size();
}
expr * const * get_assumptions() const {
return m_assumptions.c_ptr();
}
bool get_func_decl(symbol, func_decl*&);
bool get_sort(symbol, sort*&);
bool get_const(symbol, expr*&);
void set_name(symbol const& name) { m_name = name; }
symbol const get_name() const { return m_name; }
protected:
symbol m_name;
ast_manager& m_ast_manager;
ptr_vector<expr> m_axioms;
ptr_vector<expr> m_assumptions;
symtable m_symtable;
ast_ref_vector m_asts;
private:
theory& operator=(theory const&);
theory(theory const&);
};
class benchmark : public theory {
public:
enum status {
UNKNOWN,
SAT,
UNSAT
};
benchmark(ast_manager & ast_manager, symbol const & name) :
theory(ast_manager, name),
m_status(UNKNOWN) {}
virtual ~benchmark() {}
status get_status() const { return m_status; }
void set_status(status status) { m_status = status; }
symbol get_logic() const {
if (m_logic == symbol::null) {
return symbol("ALL");
}
return m_logic;
}
void set_logic(symbol const & s) { m_logic = s; }
unsigned get_num_formulas() const {
return m_formulas.size();
}
expr_iterator begin_formulas() const {
return m_formulas.begin();
}
expr_iterator end_formulas() const {
return m_formulas.end();
}
void add_formula(expr * formula) {
m_asts.push_back(formula);
m_formulas.push_back(formula);
}
void display_as_smt2(std::ostream & out) const;
private:
status m_status;
symbol m_logic;
ptr_vector<expr> m_formulas;
};
};
#endif

119
src/parsers/smt/smtlib_solver.cpp
View file

@ -1,119 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.cpp
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#include "parsers/smt/smtparser.h"
#include "parsers/smt/smtlib_solver.h"
#include "util/warning.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "model/model.h"
#include "model/model_v2_pp.h"
#include "solver/solver.h"
#include "tactic/portfolio/smt_strategic_solver.h"
#include "cmd_context/cmd_context.h"
#include "model/model_params.hpp"
#include "parsers/util/parser_params.hpp"
namespace smtlib {
solver::solver():
m_ast_manager(m_params.m_proof ? PGM_ENABLED : PGM_DISABLED,
m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
m_ctx(0),
m_error_code(0) {
parser_params ps;
m_parser = parser::create(m_ast_manager, ps.ignore_user_patterns());
m_parser->initialize_smtlib();
}
solver::~solver() {
if (m_ctx)
dealloc(m_ctx);
}
bool solver::solve_smt(char const * benchmark_file) {
IF_VERBOSE(100, verbose_stream() << "parsing...\n";);
if (!m_parser->parse_file(benchmark_file)) {
if (benchmark_file) {
warning_msg("could not parse file '%s'.", benchmark_file);
}
else {
warning_msg("could not parse input stream.");
}
m_error_code = ERR_PARSER;
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
bool solver::solve_smt_string(char const * benchmark_string) {
if (!m_parser->parse_string(benchmark_string)) {
warning_msg("could not parse string '%s'.", benchmark_string);
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
void solver::display_statistics() {
if (m_ctx)
m_ctx->display_statistics();
}
void solver::solve_benchmark(benchmark & benchmark) {
if (benchmark.get_num_formulas() == 0) {
// Hack: it seems SMT-LIB allow benchmarks without any :formula
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver_factory(mk_smt_strategic_solver_factory());
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
for (; fit != fend; ++fit)
solve_formula(benchmark, *fit);
}
void solver::solve_formula(benchmark const & benchmark, expr * f) {
IF_VERBOSE(100, verbose_stream() << "starting...\n";);
m_ctx->reset();
for (unsigned i = 0; i < benchmark.get_num_axioms(); i++)
m_ctx->assert_expr(benchmark.get_axioms()[i]);
m_ctx->assert_expr(f);
m_ctx->check_sat(benchmark.get_num_assumptions(), benchmark.get_assumptions());
check_sat_result * r = m_ctx->get_check_sat_result();
if (r != 0) {
proof * pr = r->get_proof();
if (pr != 0 && m_params.m_proof)
std::cout << mk_ll_pp(pr, m_ast_manager, false, false);
model_ref md;
if (r->status() != l_false) r->get_model(md);
if (md.get() != 0 && m_params.m_model) {
model_params p;
model_v2_pp(std::cout, *(md.get()), p.partial());
}
}
else {
m_error_code = ERR_UNKNOWN_RESULT;
}
}
};

48
src/parsers/smt/smtlib_solver.h
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.h
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#ifndef SMTLIB_SOLVER_H_
#define SMTLIB_SOLVER_H_
#include "parsers/smt/smtparser.h"
#include "cmd_context/context_params.h"
#include "util/lbool.h"
class cmd_context;
namespace smtlib {
class solver {
context_params m_params;
ast_manager m_ast_manager;
cmd_context * m_ctx;
scoped_ptr<parser> m_parser;
unsigned m_error_code;
public:
solver();
~solver();
bool solve_smt(char const * benchmark_file);
bool solve_smt_string(char const * benchmark_string);
void display_statistics();
unsigned get_error_code() const { return m_error_code; }
private:
void solve_benchmark(benchmark & benchmark);
void solve_formula(benchmark const & benchmark, expr * f);
};
};
#endif

2760
src/parsers/smt/smtparser.cpp
View file

File diff suppressed because it is too large Load diff

48
src/parsers/smt/smtparser.h
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtparser.h
Abstract:
SMT parsing utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-25
Revision History:
--*/
#ifndef SMT_PARSER_H_
#define SMT_PARSER_H_
#include<iostream>
#include "ast/ast.h"
#include "util/vector.h"
#include "parsers/smt/smtlib.h"
namespace smtlib {
class parser {
public:
static parser * create(ast_manager & ast_manager, bool ignore_user_patterns = false);
virtual ~parser() {}
virtual void add_builtin_op(char const *, family_id fid, decl_kind kind) = 0;
virtual void add_builtin_type(char const *, family_id fid, decl_kind kind) = 0;
virtual void initialize_smtlib() = 0;
virtual void set_error_stream(std::ostream& strm) = 0;
virtual bool parse_file(char const * path) = 0;
virtual bool parse_string(char const * string) = 0;
virtual benchmark * get_benchmark() = 0;
};
};
#endif

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

@ -867,7 +867,7 @@ namespace smt2 {
throw parser_exception("invalid datatype declaration, too many data-type bodies defined");
}
symbol dt_name = m_dt_names[i];
parse_datatype_dec(new_ct_decls);
parse_datatype_dec(nullptr, new_ct_decls);
d = pm().mk_pdatatype_decl(m_dt_name2arity.find(dt_name), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr());
}
else {
@ -942,7 +942,7 @@ namespace smt2 {
pdatatype_decl_ref d(pm());
pconstructor_decl_ref_buffer new_ct_decls(pm());
parse_datatype_dec(new_ct_decls);
parse_datatype_dec(&dt_name, new_ct_decls);
d = pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr());
check_missing(d, line, pos);
@ -956,12 +956,16 @@ namespace smt2 {
// datatype_dec ::= ( constructor_dec+ ) | ( par ( symbol+ ) ( constructor_dec+ ) )
void parse_datatype_dec(pconstructor_decl_ref_buffer & ct_decls) {
void parse_datatype_dec(symbol* dt_name, pconstructor_decl_ref_buffer & ct_decls) {
check_lparen_next("invalid datatype declaration, '(' expected");
if (curr_id() == m_par) {
next();
parse_sort_decl_params();
check_lparen_next("invalid constructor declaration after par, '(' expected");
unsigned sz = m_sort_id2param_idx.size();
if (sz > 0 && dt_name) {
m_ctx.insert(pm().mk_psort_dt_decl(sz, *dt_name));
}
parse_constructor_decls(ct_decls);
check_rparen_next("invalid datatype declaration, ')' expected");
}

170
src/qe/nlqsat.cpp
View file

@ -782,7 +782,7 @@ namespace qe {
m(m),
m_mode(mode),
m_params(p),
m_solver(m.limit(), p),
m_solver(m.limit(), p, true),
m_nftactic(0),
m_rmodel(m_solver.am()),
m_rmodel0(m_solver.am()),
@ -886,174 +886,6 @@ namespace qe {
tactic * translate(ast_manager & m) {
return alloc(nlqsat, m, m_mode, m_params);
}
#if 0
/**
Algorithm:
I := true
while there is M, such that M |= ~B & I:
find P, such that M => P => exists y . ~B & I
; forall y B => ~P
C := core of P with respect to A
; A => ~ C => ~ P
I := I & ~C
Alternative Algorithm:
R := false
while there is M, such that M |= A & ~R:
find I, such that M => I => forall y . B
R := R | I
*/
lbool interpolate(expr* a, expr* b, expr_ref& result) {
SASSERT(m_mode == interp_t);
reset();
app_ref enableA(m), enableB(m);
expr_ref A(m), B(m), fml(m);
expr_ref_vector fmls(m), answer(m);
// varsB are private to B.
nlsat::var_vector vars;
uint_set fvars;
private_vars(a, b, vars, fvars);
enableA = m.mk_const(symbol("#A"), m.mk_bool_sort());
enableB = m.mk_not(enableA);
A = m.mk_implies(enableA, a);
B = m.mk_implies(enableB, m.mk_not(b));
fml = m.mk_and(A, B);
hoist(fml);
nlsat::literal _enableB = nlsat::literal(m_a2b.to_var(enableB), false);
nlsat::literal _enableA = ~_enableB;
while (true) {
m_mode = qsat_t;
// enable B
m_assumptions.reset();
m_assumptions.push_back(_enableB);
lbool is_sat = check_sat();
switch (is_sat) {
case l_undef:
return l_undef;
case l_true:
break;
case l_false:
result = mk_and(answer);
return l_true;
}
// disable B, enable A
m_assumptions.reset();
m_assumptions.push_back(_enableA);
// add blocking clause to solver.
nlsat::scoped_literal_vector core(m_solver);
m_mode = elim_t;
mbp(vars, fvars, core);
// minimize core.
nlsat::literal_vector _core(core.size(), core.c_ptr());
_core.push_back(_enableA);
is_sat = m_solver.check(_core); // TBD: only for quantifier-free A. Generalize output of elim_t to be a core.
switch (is_sat) {
case l_undef:
return l_undef;
case l_true:
UNREACHABLE();
case l_false:
core.reset();
core.append(_core.size(), _core.c_ptr());
break;
}
negate_clause(core);
// keep polarity of enableA, such that clause is only
// used when checking satisfiability of B.
for (unsigned i = 0; i < core.size(); ++i) {
if (core[i].var() == _enableA.var()) core.set(i, ~core[i]);
}
add_clause(core); // Invariant is added as assumption for B.
answer.push_back(clause2fml(core)); // TBD: remove answer literal.
}
}
/**
\brief extract variables that are private to a (not used in b).
vars cover the real variables, and fvars cover the Boolean variables.
TBD: We want fvars to be the complement such that returned core contains
Shared boolean variables, but not the ones private to B.
*/
void private_vars(expr* a, expr* b, nlsat::var_vector& vars, uint_set& fvars) {
app_ref_vector varsA(m), varsB(m);
obj_hashtable<expr> varsAS;
pred_abs abs(m);
abs.get_free_vars(a, varsA);
abs.get_free_vars(b, varsB);
insert_set(varsAS, varsA);
for (unsigned i = 0; i < varsB.size(); ++i) {
if (varsAS.contains(varsB[i].get())) {
varsB[i] = varsB.back();
varsB.pop_back();
--i;
}
}
for (unsigned j = 0; j < varsB.size(); ++j) {
app* v = varsB[j].get();
if (m_a2b.is_var(v)) {
fvars.insert(m_a2b.to_var(v));
}
else if (m_t2x.is_var(v)) {
vars.push_back(m_t2x.to_var(v));
}
}
}
lbool maximize(app* _x, expr* _fml, scoped_anum& result, bool& unbounded) {
expr_ref fml(_fml, m);
reset();
hoist(fml);
nlsat::literal_vector lits;
lbool is_sat = l_true;
nlsat::var x = m_t2x.to_var(_x);
m_mode = qsat_t;
while (is_sat == l_true) {
is_sat = check_sat();
if (is_sat == l_true) {
// m_asms is minimized set of literals that satisfy formula.
nlsat::explain& ex = m_solver.get_explain();
polynomial::manager& pm = m_solver.pm();
anum_manager& am = m_solver.am();
ex.maximize(x, m_asms.size(), m_asms.c_ptr(), result, unbounded);
if (unbounded) {
break;
}
// TBD: assert the new bound on x using the result.
bool is_even = false;
polynomial::polynomial_ref pr(pm);
pr = pm.mk_polynomial(x);
rational r;
am.get_upper(result, r);
// result is algebraic numeral, but polynomials are not defined over extension field.
polynomial::polynomial* p = pr;
nlsat::bool_var b = m_solver.mk_ineq_atom(nlsat::atom::GT, 1, &p, &is_even);
nlsat::literal bound(b, false);
m_solver.mk_clause(1, &bound);
}
}
return is_sat;
}
#endif
};
};

2
src/qe/qe_lite.cpp
View file

@ -974,7 +974,7 @@ namespace ar {
// ------------------------------------------------------------
// fm_tactic adapted to eliminate designated de-Brujin indices.
// fm_tactic adapted to eliminate designated de-Bruijn indices.
namespace fm {
typedef ptr_vector<app> clauses;

25
src/shell/main.cpp
View file

@ -35,9 +35,10 @@ Revision History:
#include "util/error_codes.h"
#include "util/gparams.h"
#include "util/env_params.h"
#include "util/file_path.h"
#include "shell/lp_frontend.h"
typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
std::string g_aux_input_file;
char const * g_input_file = 0;
@ -169,9 +170,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
std::cout << "\n";
exit(0);
}
else if (strcmp(opt_name, "smt") == 0) {
g_input_kind = IN_SMTLIB;
}
else if (strcmp(opt_name, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
@ -289,19 +287,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
}
}
char const * get_extension(char const * file_name) {
if (file_name == 0)
return 0;
char const * last_dot = 0;
for (;;) {
char const * tmp = strchr(file_name, '.');
if (tmp == 0) {
return last_dot;
}
last_dot = tmp + 1;
file_name = last_dot;
}
}
int STD_CALL main(int argc, char ** argv) {
try{
@ -340,9 +325,6 @@ int STD_CALL main(int argc, char ** argv) {
else if (strcmp(ext, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
else if (strcmp(ext, "smt") == 0) {
g_input_kind = IN_SMTLIB;
}
else if (strcmp(ext, "mps") == 0 || strcmp(ext, "sif") == 0 ||
strcmp(ext, "MPS") == 0 || strcmp(ext, "SIF") == 0) {
g_input_kind = IN_MPS;
@ -350,9 +332,6 @@ int STD_CALL main(int argc, char ** argv) {
}
}
switch (g_input_kind) {
case IN_SMTLIB:
return_value = read_smtlib_file(g_input_file);
break;
case IN_SMTLIB_2:
memory::exit_when_out_of_memory(true, "(error \"out of memory\")");
return_value = read_smtlib2_commands(g_input_file);

264
src/shell/opt_frontend.cpp
View file

@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/gparams.h"
#include "util/timeout.h"
#include "ast/reg_decl_plugins.h"
#include "opt/opt_parse.h"
extern bool g_display_statistics;
static bool g_first_interrupt = true;
@ -20,262 +21,6 @@ static opt::context* g_opt = 0;
static double g_start_time = 0;
static unsigned_vector g_handles;
class opt_stream_buffer {
std::istream & m_stream;
int m_val;
unsigned m_line;
public:
opt_stream_buffer(std::istream & s):
m_stream(s),
m_line(0) {
m_val = m_stream.get();
}
int operator *() const { return m_val;}
void operator ++() { m_val = m_stream.get(); }
int ch() const { return m_val; }
void next() { m_val = m_stream.get(); }
bool eof() const { return ch() == EOF; }
unsigned line() const { return m_line; }
void skip_whitespace() {
while ((ch() >= 9 && ch() <= 13) || ch() == 32) {
if (ch() == 10) ++m_line;
next();
}
}
void skip_space() {
while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) {
next();
}
}
void skip_line() {
while(true) {
if (eof()) {
return;
}
if (ch() == '\n') {
++m_line;
next();
return;
}
next();
}
}
bool parse_token(char const* token) {
skip_whitespace();
char const* t = token;
while (ch() == *t) {
next();
++t;
}
return 0 == *t;
}
int parse_int() {
int val = 0;
bool neg = false;
skip_whitespace();
if (ch() == '-') {
neg = true;
next();
}
else if (ch() == '+') {
next();
}
if (ch() < '0' || ch() > '9') {
std::cerr << "(error line " << line() << " \"unexpected char: " << ((char)ch()) << "\" )\n";
exit(3);
}
while (ch() >= '0' && ch() <= '9') {
val = val*10 + (ch() - '0');
next();
}
return neg ? -val : val;
}
unsigned parse_unsigned() {
skip_space();
if (ch() == '\n') {
return UINT_MAX;
}
unsigned val = 0;
while (ch() >= '0' && ch() <= '9') {
val = val*10 + (ch() - '0');
next();
}
return val;
}
};
class wcnf {
opt::context& opt;
ast_manager& m;
opt_stream_buffer& in;
app_ref read_clause(unsigned& weight) {
int parsed_lit;
int var;
weight = in.parse_unsigned();
app_ref result(m), p(m);
expr_ref_vector ors(m);
while (true) {
parsed_lit = in.parse_int();
if (parsed_lit == 0)
break;
var = abs(parsed_lit);
p = m.mk_const(symbol(var), m.mk_bool_sort());
if (parsed_lit < 0) p = m.mk_not(p);
ors.push_back(p);
}
result = to_app(mk_or(m, ors.size(), ors.c_ptr()));
return result;
}
void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
in.parse_token("wcnf");
num_vars = in.parse_unsigned();
num_clauses = in.parse_unsigned();
max_weight = in.parse_unsigned();
}
public:
wcnf(opt::context& opt, opt_stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) {
opt.set_clausal(true);
}
void parse() {
unsigned num_vars = 0, num_clauses = 0, max_weight = 0;
while (true) {
in.skip_whitespace();
if (in.eof()) {
break;
}
else if (*in == 'c') {
in.skip_line();
}
else if (*in == 'p') {
++in;
parse_spec(num_vars, num_clauses, max_weight);
}
else {
unsigned weight = 0;
app_ref cls = read_clause(weight);
if (weight >= max_weight) {
opt.add_hard_constraint(cls);
}
else {
unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
if (g_handles.empty()) {
g_handles.push_back(id);
}
}
}
}
}
};
class opb {
opt::context& opt;
ast_manager& m;
opt_stream_buffer& in;
arith_util arith;
app_ref parse_id() {
bool negated = in.parse_token("~");
if (!in.parse_token("x")) {
std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\")\n";
exit(3);
}
app_ref p(m);
int id = in.parse_int();
p = m.mk_const(symbol(id), m.mk_bool_sort());
if (negated) p = m.mk_not(p);
in.skip_whitespace();
return p;
}
app_ref parse_ids() {
app_ref result = parse_id();
while (*in == '~' || *in == 'x') {
result = m.mk_and(result, parse_id());
}
return result;
}
rational parse_coeff_r() {
in.skip_whitespace();
svector<char> num;
bool pos = true;
if (*in == '-') pos = false, ++in;
if (*in == '+') ++in;
if (!pos) num.push_back('-');
in.skip_whitespace();
while ('0' <= *in && *in <='9') num.push_back(*in), ++in;
num.push_back(0);
return rational(num.c_ptr());
}
app_ref parse_coeff() {
return app_ref(arith.mk_numeral(parse_coeff_r(), true), m);
}
app_ref parse_term() {
app_ref c = parse_coeff();
app_ref e = parse_ids();
return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m);
}
void parse_objective() {
app_ref t = parse_term();
while (!in.parse_token(";") && !in.eof()) {
t = arith.mk_add(t, parse_term());
}
g_handles.push_back(opt.add_objective(t, false));
}
void parse_constraint() {
app_ref t = parse_term();
while (!in.eof()) {
if (in.parse_token(">=")) {
t = arith.mk_ge(t, parse_coeff());
in.parse_token(";");
break;
}
if (in.parse_token("=")) {
t = m.mk_eq(t, parse_coeff());
in.parse_token(";");
break;
}
t = arith.mk_add(t, parse_term());
}
opt.add_hard_constraint(t);
}
public:
opb(opt::context& opt, opt_stream_buffer& in):
opt(opt), m(opt.get_manager()),
in(in), arith(m) {}
void parse() {
while (true) {
in.skip_whitespace();
if (in.eof()) {
break;
}
else if (*in == '*') {
in.skip_line();
}
else if (in.parse_token("min:")) {
parse_objective();
}
else {
parse_constraint();
}
}
}
};
static void display_results() {
@ -335,14 +80,11 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
g_opt = &opt;
params_ref p = gparams::get_module("opt");
opt.updt_params(p);
opt_stream_buffer _in(in);
if (is_wcnf) {
wcnf wcnf(opt, _in);
wcnf.parse();
parse_wcnf(opt, in, g_handles);
}
else {
opb opb(opt, _in);
opb.parse();
parse_opb(opt, in, g_handles);
}
try {
lbool r = opt.optimize();

38
src/shell/smtlib_frontend.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include<iostream>
#include<time.h>
#include<signal.h>
#include "parsers/smt/smtlib_solver.h"
#include "util/timeout.h"
#include "parsers/smt2/smt2parser.h"
#include "muz/fp/dl_cmds.h"
@ -35,20 +34,14 @@ Revision History:
extern bool g_display_statistics;
static clock_t g_start_time;
static smtlib::solver* g_solver = 0;
static cmd_context * g_cmd_context = 0;
static void display_statistics() {
clock_t end_time = clock();
if ((g_solver || g_cmd_context) && g_display_statistics) {
if (g_cmd_context && g_display_statistics) {
std::cout.flush();
std::cerr.flush();
if (g_solver) {
g_solver->display_statistics();
memory::display_max_usage(std::cout);
std::cout << "time: " << ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC) << " secs\n";
}
else if (g_cmd_context) {
if (g_cmd_context) {
g_cmd_context->set_regular_stream("stdout");
g_cmd_context->display_statistics(true, ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
}
@ -72,33 +65,6 @@ static void STD_CALL on_ctrl_c(int) {
raise(SIGINT);
}
unsigned read_smtlib_file(char const * benchmark_file) {
g_start_time = clock();
register_on_timeout_proc(on_timeout);
signal(SIGINT, on_ctrl_c);
smtlib::solver solver;
g_solver = &solver;
bool ok = true;
ok = solver.solve_smt(benchmark_file);
if (!ok) {
if (benchmark_file) {
std::cerr << "ERROR: solving '" << benchmark_file << "'.\n";
}
else {
std::cerr << "ERROR: solving input stream.\n";
}
}
#pragma omp critical (g_display_stats)
{
display_statistics();
register_on_timeout_proc(0);
g_solver = 0;
}
return solver.get_error_code();
}
unsigned read_smtlib2_commands(char const * file_name) {
g_start_time = clock();

1
src/smt/asserted_formulas.cpp
View file

@ -131,6 +131,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
p.set_bool("gcd_rounding", true);
p.set_bool("expand_select_store", true);
p.set_bool("bv_sort_ac", true);
p.set_bool("som", true);
m_rewriter.updt_params(p);
flush_cache();
}

4
src/smt/mam.cpp
View file

@ -188,7 +188,7 @@ namespace smt {
1) Variables: (f ... X ...)
2) Ground terms: (f ... t ...)
3) depth 2 joint: (f ... (g ... X ...) ...)
Joint2 stores the declartion g, and the position of variable X, and its idx.
Joint2 stores the declaration g, and the position of variable X, and its idx.
\remark Z3 has no support for depth 3 joints (f ... (g ... (h ... X ...) ...) ....)
*/
@ -211,7 +211,7 @@ namespace smt {
approx_set m_lbl_set; // singleton set containing m_label
/*
The following field is an array of tagged pointers.
Each positon contains:
Each position contains:
1- null (no joint), NULL_TAG
2- a boxed integer (i.e., register that contains the variable bind) VAR_TAG
3- an enode pointer (ground term) GROUND_TERM_TAG

2
src/smt/params/smt_params_helper.pyg
View file

@ -74,7 +74,7 @@ def_module_params(module_name='smt',
('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
('str.use_binary_search', BOOL, True, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),

59
src/smt/smt_context.cpp
View file

@ -3202,10 +3202,8 @@ namespace smt {
});
validate_unsat_core();
// theory validation of unsat core
ptr_vector<theory>::iterator th_it = m_theory_set.begin();
ptr_vector<theory>::iterator th_end = m_theory_set.end();
for (; th_it != th_end; ++th_it) {
lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core);
for (theory* th : m_theory_set) {
lbool theory_result = th->validate_unsat_core(m_unsat_core);
if (theory_result == l_undef) {
return l_undef;
}
@ -3296,10 +3294,8 @@ namespace smt {
#ifndef _EXTERNAL_RELEASE
if (m_fparams.m_display_installed_theories) {
std::cout << "(theories";
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
std::cout << " " << (*it)->get_name();
for (theory* th : m_theory_set) {
std::cout << " " << th->get_name();
}
std::cout << ")" << std::endl;
}
@ -3316,17 +3312,13 @@ namespace smt {
m_fparams.m_relevancy_lemma = false;
// setup all the theories
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->setup();
for (theory* th : m_theory_set)
th->setup();
}
void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
for (theory* th : m_theory_set) {
th->add_theory_assumptions(theory_assumptions);
}
}
@ -3342,18 +3334,7 @@ namespace smt {
if (!check_preamble(reset_cancel))
return l_undef;
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";);
TRACE("unsat_core_bug", for (unsigned i = 0; i < num_assumptions; i++) { tout << mk_pp(assumptions[i], m_manager) << "\n";});
pop_to_base_lvl();
TRACE("before_search", display(tout););
SASSERT(at_base_level());
@ -3363,6 +3344,18 @@ namespace smt {
}
else {
setup_context(false);
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("unsat_core_bug", tout << all_assumptions << "\n";);
internalize_assertions();
TRACE("after_internalize_assertions", display(tout););
if (m_asserted_formulas.inconsistent()) {
@ -3551,10 +3544,9 @@ namespace smt {
pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level());
}
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end && !inconsistent(); ++it)
(*it)->restart_eh();
for (theory* th : m_theory_set) {
if (!inconsistent()) th->restart_eh();
}
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
if (!inconsistent()) {
m_qmanager->restart_eh();
@ -4070,10 +4062,7 @@ namespace smt {
bool include = false;
if (at_lbls) {
// include if there is a label with the '@' sign.
buffer<symbol>::const_iterator it = lbls.begin();
buffer<symbol>::const_iterator end = lbls.end();
for (; it != end; ++it) {
symbol const & s = *it;
for (symbol const& s : lbls) {
if (s.contains('@')) {
include = true;
break;

12
src/smt/smt_internalizer.cpp
View file

@ -369,7 +369,7 @@ namespace smt {
else {
TRACE("internalize_bug", tout << "creating enode for #" << n->get_id() << "\n";);
mk_enode(to_app(n),
true, /* supress arguments, we not not use CC for this kind of enode */
true, /* suppress arguments, we not not use CC for this kind of enode */
true, /* bool enode must be merged with true/false, since it is not in the context of a gate */
false /* CC is not enabled */ );
set_enode_flag(v, false);
@ -453,7 +453,7 @@ namespace smt {
// must be associated with an enode.
if (!e_internalized(n)) {
mk_enode(to_app(n),
true, /* supress arguments, we not not use CC for this kind of enode */
true, /* suppress arguments, we not not use CC for this kind of enode */
true /* bool enode must be merged with true/false, since it is not in the context of a gate */,
false /* CC is not enabled */);
}
@ -739,7 +739,7 @@ namespace smt {
app_ref eq1(mk_eq_atom(n, t), m_manager);
app_ref eq2(mk_eq_atom(n, e), m_manager);
mk_enode(n,
true /* supress arguments, I don't want to apply CC on ite terms */,
true /* suppress arguments, I don't want to apply CC on ite terms */,
false /* it is a term, so it should not be merged with true/false */,
false /* CC is not enabled */);
internalize(c, true);
@ -797,7 +797,7 @@ namespace smt {
}
enode * e = mk_enode(n,
false, /* do not supress args */
false, /* do not suppress args */
false, /* it is a term, so it should not be merged with true/false */
true);
apply_sort_cnstr(n, e);
@ -1506,7 +1506,7 @@ namespace smt {
relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
// if one child is assigned to false, the the and-parent must be notified
// if one child is assigned to false, the and-parent must be notified
literal l = get_literal(n->get_arg(i));
add_rel_watch(~l, eh);
}
@ -1518,7 +1518,7 @@ namespace smt {
relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
// if one child is assigned to true, the the or-parent must be notified
// if one child is assigned to true, the or-parent must be notified
literal l = get_literal(n->get_arg(i));
add_rel_watch(l, eh);
}

33
src/smt/smt_model_finder.cpp
View file

@ -537,7 +537,7 @@ namespace smt {
}
}
// For each instantiation_set, reemove entries that do not evaluate to values.
// For each instantiation_set, remove entries that do not evaluate to values.
void cleanup_instantiation_sets() {
ptr_vector<expr> to_delete;
for (node * curr : m_nodes) {
@ -735,7 +735,7 @@ namespace smt {
}
}
// TBD: add support for the else of bitvectors.
// Idea: get the term t with the minimal interpreation and use t - 1.
// Idea: get the term t with the minimal interpretation and use t - 1.
}
n->set_else((*(elems.begin())).m_key);
}
@ -955,7 +955,7 @@ namespace smt {
if (elems.empty()) {
// The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts
// (e.g., (Array S S) where S is uninterpreted). The problem is that these sorts do not have a fixed interpretation.
// Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value.
// Moreover, a model assigns an arbitrary interpretation to these sorts using "model_values" a model value.
// If these module values "leak" inside the logical context, they may affect satisfiability.
//
sort * ns = n->get_sort();
@ -1007,7 +1007,7 @@ namespace smt {
This may happen because the evaluator uses model_completion.
In the beginning of fix_model() we collected all f with
partial interpretations. During the process of computing the
projections we used the evalutator with model_completion,
projections we used the evaluator with model_completion,
and it may have fixed the "else" case of some partial interpretations.
This is ok, because in the "limit" the "else" of the interpretation
is irrelevant after the projections are applied.
@ -1570,7 +1570,7 @@ namespace smt {
ast_manager & m = ctx->get_manager();
sort * s = q->get_decl_sort(num_vars - m_var_i - 1);
if (m.is_uninterp(s)) {
// For uninterpreted sorst, we add all terms in the context.
// For uninterpreted sorts, we add all terms in the context.
// See Section 4.1 in the paper "Complete Quantifier Instantiation"
node * S_q_i = slv.get_uvar(q, m_var_i);
ptr_vector<enode>::const_iterator it = ctx->begin_enodes();
@ -1741,7 +1741,7 @@ namespace smt {
if (has_quantifiers(q->get_expr())) {
static bool displayed_flat_msg = false;
if (!displayed_flat_msg) {
// [Leo]: This warning message is not usefult.
// [Leo]: This warning message is not useful.
// warning_msg("For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.");
displayed_flat_msg = true;
}
@ -2104,7 +2104,7 @@ namespace smt {
}
/**
\brief Process unintrepreted applications.
\brief Process uninterpreted applications.
*/
void process_u_app(app * t) {
unsigned num_args = t->get_num_args();
@ -2130,7 +2130,7 @@ namespace smt {
/**
\brief A term \c t is said to be a auf_select if
it is of ther form
it is of the form
(select a i) Where:
@ -2151,7 +2151,7 @@ namespace smt {
}
/**
\brief Process intrepreted applications.
\brief Process interpreted applications.
*/
void process_i_app(app * t) {
if (is_auf_select(t)) {
@ -2272,10 +2272,9 @@ namespace smt {
process_literal(atom, pol == NEG);
}
void process_or(app * n, polarity p) {
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++)
visit_formula(n->get_arg(i), p);
void process_and_or(app * n, polarity p) {
for (expr* arg : *n)
visit_formula(arg, p);
}
void process_ite(app * n, polarity p) {
@ -2306,13 +2305,13 @@ namespace smt {
if (is_app(curr)) {
if (to_app(curr)->get_family_id() == m_manager.get_basic_family_id() && m_manager.is_bool(curr)) {
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
case OP_AND:
case OP_IMPLIES:
case OP_XOR:
UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs
break;
case OP_OR:
process_or(to_app(curr), pol);
case OP_AND:
process_and_or(to_app(curr), pol);
break;
case OP_NOT:
visit_formula(to_app(curr)->get_arg(0), neg(pol));
@ -2513,7 +2512,7 @@ namespace smt {
SASSERT(f_else != 0);
// Remark: I can ignore the conditions of m because
// I know the (partial) interpretation of f satisfied the ground part.
// MBQI will force extra instantiations if the the (partial) interpretation of f
// MBQI will force extra instantiations if the (partial) interpretation of f
// does not satisfy the quantifier.
// In all other cases the "else" of f will satisfy the quantifier.
set_else_interp(f, f_else);
@ -2938,7 +2937,7 @@ namespace smt {
}
/**
\brief Use m_fs to set the interpreation of the function symbols that were used to satisfy the
\brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the
quantifiers in m_satisfied.
*/
void set_interp() {

2
src/smt/smt_quantifier.h
View file

@ -152,7 +152,7 @@ namespace smt {
virtual bool mbqi_enabled(quantifier *q) const {return true;}
/**
\brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
\brief Give a change to the plugin to adjust the interpretation of uninterpreted functions.
It can basically change the "else" of each uninterpreted function.
*/
virtual void adjust_model(proto_model * m) = 0;

2
src/smt/smt_setup.cpp
View file

@ -968,7 +968,7 @@ namespace smt {
if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
if (!st.m_has_real)
setup_QF_UFLIA(st);
else if (!st.m_has_int)
else if (!st.m_has_int && st.m_num_non_linear == 0)
setup_QF_UFLRA();
else
setup_unknown();

2
src/smt/theory_arith.h
View file

@ -660,7 +660,7 @@ namespace smt {
satisfy their respective constraints. However, when they
do that the may create inconsistencies in the other
modules. I use m_liberal_final_check to avoid infinite
loops where the modules keep changing the assigment and no
loops where the modules keep changing the assignment and no
progress is made. If m_liberal_final_check is set to false,
these modules will avoid mutating the assignment to satisfy
constraints.

1
src/smt/theory_arith_nl.h
View file

@ -711,6 +711,7 @@ namespace smt {
if (ctx.is_relevant(get_enode(*it)) && !check_monomial_assignment(*it, computed_epsilon)) {
TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(*it), get_manager()) << "\n";
display_var(tout, *it););
return false;
}
}

2
src/smt/theory_arith_pp.h
View file

@ -526,7 +526,7 @@ namespace smt {
}
}
}
pp.display(out, m.mk_true());
pp.display_smt2(out, m.mk_true());
}
template<typename Ext>

2
src/smt/theory_lra.cpp
View file

@ -1916,7 +1916,7 @@ namespace smt {
lp::var_index vi = m_theory_var2var_index[v];
SASSERT(m_solver->is_term(vi));
lp::lar_term const& term = m_solver->get_term(vi);
for (auto const coeff : term.m_coeffs) {
for (auto const& coeff : term.m_coeffs) {
lp::var_index wi = coeff.first;
lp::constraint_index ci;
rational value;

53
src/smt/theory_seq.cpp
View file

@ -397,15 +397,13 @@ bool theory_seq::branch_binary_variable(eq const& e) {
expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
ys.push_back(Y1);
expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m);
expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
literal_vector lits;
lits.push_back(~lit);
expr_ref ysY1(mk_concat(ys));
expr_ref xsE(mk_concat(xs));
expr_ref Y1Y2(mk_concat(Y1, Y2));
dependency* dep = e.dep();
propagate_eq(dep, lits, x, ysY1, true);
propagate_eq(dep, lits, y, Y1Y2, true);
propagate_eq(dep, lits, Y2, xsE, true);
propagate_eq(dep, ~lit, x, ysY1);
propagate_eq(dep, ~lit, y, Y1Y2);
propagate_eq(dep, ~lit, Y2, xsE);
}
else {
ctx.mark_as_relevant(lit);
@ -471,9 +469,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false);
if (l_true == ctx.get_assignment(lit)) {
expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
literal_vector lits;
lits.push_back(lit);
propagate_eq(dep, lits, X, R, true);
propagate_eq(dep, lit, X, R);
TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
}
else {
@ -506,11 +502,10 @@ bool theory_seq::branch_variable_mb() {
for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j];
if (l1 != l2) {
TRACE("seq", tout << "lengths are not compatible\n";);
expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
expr_ref l = mk_concat(e.ls());
expr_ref r = mk_concat(e.rs());
expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
literal_vector lits;
propagate_eq(e.dep(), lits, lnl, lnr, false);
propagate_eq(e.dep(), lnl, lnr, false);
change = true;
continue;
}
@ -626,8 +621,8 @@ bool theory_seq::split_lengths(dependency* dep,
SASSERT(is_var(Y));
expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m);
expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
expr_ref bY1 = mk_concat(b, Y1);
expr_ref Y1Y2 = mk_concat(Y1, Y2);
propagate_eq(dep, lits, X, bY1, true);
propagate_eq(dep, lits, Y, Y1Y2, true);
}
@ -1317,6 +1312,18 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
enforce_length_coherence(n1, n2);
}
void theory_seq::propagate_eq(dependency* dep, expr* e1, expr* e2, bool add_eq) {
literal_vector lits;
propagate_eq(dep, lits, e1, e2, add_eq);
}
void theory_seq::propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2, bool add_to_eqs) {
literal_vector lits;
lits.push_back(lit);
propagate_eq(dep, lits, e1, e2, add_to_eqs);
}
void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
@ -1662,19 +1669,18 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
}
SASSERT(0 < l1 && l1 < ls.size());
SASSERT(0 < r1 && r1 < rs.size());
expr_ref l(m_util.str.mk_concat(l1, ls1), m);
expr_ref r(m_util.str.mk_concat(r1, rs1), m);
expr_ref l = mk_concat(l1, ls1);
expr_ref r = mk_concat(r1, rs1);
expr_ref lenl(m_util.str.mk_length(l), m);
expr_ref lenr(m_util.str.mk_length(r), m);
literal lit = mk_eq(lenl, lenr, false);
if (ctx.get_assignment(lit) == l_true) {
literal_vector lits;
expr_ref_vector lhs(m), rhs(m);
lhs.append(l2, ls2);
rhs.append(r2, rs2);
deps = mk_join(deps, lit);
m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
propagate_eq(deps, lits, l, r, true);
propagate_eq(deps, l, r, true);
TRACE("seq", tout << "propagate eq\nlhs: " << lhs << "\nrhs: " << rhs << "\n";);
return true;
}
@ -3212,9 +3218,10 @@ void theory_seq::add_indexof_axiom(expr* i) {
literal t_eq_empty = mk_eq_empty(t);
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
// ~contains(t,s) => indexof(t,s,offset) = -1
// ~contains(t,s) <=> indexof(t,s,offset) = -1
add_axiom(cnt, i_eq_m1);
// add_axiom(~cnt, ~i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
@ -3227,6 +3234,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(~s_eq_empty, i_eq_0);
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
add_axiom(~cnt, mk_literal(m_autil.mk_ge(i, zero)));
tightest_prefix(s, x);
}
else {
@ -3661,7 +3669,6 @@ void theory_seq::add_extract_axiom(expr* e) {
literal ls_le_i = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
literal li_ge_ls = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_zero = mk_simplified_literal(m_autil.mk_le(l, zero));
literal ls_le_0 = mk_simplified_literal(m_autil.mk_le(ls, zero));
add_axiom(~i_ge_0, ~ls_le_i, mk_seq_eq(xey, s));

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