mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-02 13:27:01 +00:00
Code Activity

init search before returning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-11 13:08:05 -07:00
parent b266af3e08
commit af6ebbcd92
16 changed files with 90 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/api_solver.cpp
View file

@ -479,12 +479,14 @@ extern "C" {
Z3_ast Z3_API Z3_solver_lookahead(Z3_context c,
Z3_solver s,
Z3_ast_vector assumptions,
Z3_ast_vector candidates) {
Z3_TRY;
LOG_Z3_solver_lookahead(c, s, candidates);
LOG_Z3_solver_lookahead(c, s, assumptions, candidates);
ast_manager& m = mk_c(c)->m();
expr_ref_vector _candidates(m);
expr_ref_vector _candidates(m), _assumptions(m);
ast_ref_vector const& __candidates = to_ast_vector_ref(candidates);
ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
for (auto & e : __candidates) {
if (!is_expr(e)) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
@ -492,6 +494,13 @@ extern "C" {
}
_candidates.push_back(to_expr(e));
}
for (auto & e : __assumptions) {
if (!is_expr(e)) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return 0;
}
_assumptions.push_back(to_expr(e));
}
expr_ref result(m);
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
@ -504,7 +513,7 @@ extern "C" {
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
result = to_solver_ref(s)->lookahead(_candidates);
result = to_solver_ref(s)->lookahead(_assumptions, _candidates);
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);

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

@ -255,11 +255,13 @@ namespace Microsoft.Z3
/// <summary>
/// Select a lookahead literal from the set of supplied candidates.
/// </summary>
public BoolExpr Lookahead(IEnumerable<BoolExpr> candidates)
public BoolExpr Lookahead(IEnumerable<BoolExpr> assumptions, IEnumerable<BoolExpr> candidates)
{
ASTVector cands = new ASTVector(Context);
foreach (var c in candidates) cands.Push(c);
return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, cands.NativeObject));
ASTVector assums = new ASTVector(Context);
foreach (var c in assumptions) assums.Push(c);
return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, assums.NativeObject, cands.NativeObject));
}
/// <summary>

4
src/api/z3_api.h
View file

@ -6028,10 +6028,10 @@ extern "C" {
\brief select a literal from the list of candidate propositional variables to split on.
If the candidate list is empty, then the solver chooses a formula based on its internal state.
def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR)))
def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR)))
*/
Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector candidates);
Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector candidates);
/**