mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

include special functionality in parsers for solvers and opt for additional file formats

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-03 20:00:24 +01:00
parent 187998ae4d
commit 5ee30a3cd9
12 changed files with 324 additions and 303 deletions
Download patch file Download diff file Expand all files Collapse all files

42
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,27 @@ 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));
ctx->set_ignore_check(true);
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
ctx->set_ignore_check(true);
try {
if (!parse_smt2_commands(*ctx.get(), s)) {
mk_c(c)->m_parser_error_buffer = errstrm.str();
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
@ -303,6 +316,7 @@ extern "C" {
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) {
@ -310,6 +324,8 @@ extern "C" {
}
}
void Z3_API Z3_optimize_from_string(
Z3_context c,
Z3_optimize d,
@ -318,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;
}
@ -334,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;
}
@ -347,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);

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

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

@ -1536,6 +1536,35 @@ namespace z3 {
m_vector = s.m_vector;
return *this;
}
bool contains(T const& x) const {
for (auto 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; }
};
@ -1911,6 +1940,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(); }
@ -1923,6 +1957,10 @@ namespace z3 {
void add(expr const & e, char const * p) {
add(e, ctx().bool_const(p));
}
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);
@ -2003,6 +2041,7 @@ namespace z3 {
return *this;
}
void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
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); }

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

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

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

@ -6324,6 +6324,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."""

14
src/api/z3_api.h
View file

@ -6038,6 +6038,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.