mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

updates with constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-09 18:32:45 -07:00
parent 942571d5a4
commit 7db0df22e8
3 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/synth_decl_plugin.h
View file

@ -50,9 +50,12 @@ namespace synth {
public:
util(ast_manager& m): m(m), m_fid(m.get_family_id("synth")) {}
bool is_synthesiz3(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); }
bool is_grammar(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); }
bool is_specification(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_SPECIFICATION); }
bool is_synthesiz3(expr* e) const { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); }
bool is_grammar(expr* e) const { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); }
bool is_specification(expr const* e) const { return is_app_of(e, m_fid, OP_DECLARE_SPECIFICATION); }
bool is_specification(func_decl const* f) const { return is_decl_of(f, m_fid, OP_DECLARE_SPECIFICATION); }
MATCH_UNARY(is_specification);
};
}

9
src/sat/smt/synth_solver.cpp
View file

@ -85,10 +85,8 @@ namespace synth {
}
}
void solver::add_specification(app* e) {
void solver::add_specification(app* e, expr* arg) {
// This assumes that each (assert (constraint (...)) is asserting exactly one app
SASSERT((e->get_num_args() == 1) && (is_app(e->get_arg(0))));
app* arg = to_app(e->get_arg(0));
sat::literal lit = ctx.mk_literal(arg);
sat::bool_var bv = ctx.get_si().add_bool_var(e);
sat::literal lit_e(bv, false);
@ -115,12 +113,13 @@ namespace synth {
ctx.attach_lit(lit, e);
synth::util util(m);
app* a = to_app(e);
expr* arg = nullptr;
if (util.is_synthesiz3(e))
add_synth_objective(a);
if (util.is_grammar(e))
add_uncomputable(a);
if (util.is_specification(e))
add_specification(a);
if (util.is_specification(e, arg))
add_specification(a, arg);
}
// display current state (eg. current set of realizers)

4
src/sat/smt/synth_solver.h
View file

@ -42,7 +42,7 @@ namespace synth {
sat::literal synthesize(app* e);
void add_uncomputable(app* e);
void add_synth_objective(app* e);
void add_specification(app* e);
void add_specification(app* e, expr* arg);
bool contains_uncomputable(expr* e);
void on_merge_eh(euf::enode* root, euf::enode* other);
@ -59,7 +59,7 @@ namespace synth {
typedef obj_hashtable<func_decl> func_decl_set;
func_decl_set m_uncomputable;
typedef obj_hashtable<app> app_set;
app_set m_spec;
obj_hashtable<expr> m_spec;
};