mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

Annotate spec as "constraint" - work in progress

Browse source
This commit is contained in:
Petra Hozzova 2023-08-09 17:36:40 -07:00
parent a7e2b64545
commit 3fc8f7e5d0
4 changed files with 24 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/synth_decl_plugin.cpp
View file

@ -43,6 +43,9 @@ namespace synth {
case OP_DECLARE_GRAMMAR: case OP_DECLARE_GRAMMAR:
name = "uncomputable"; name = "uncomputable";
break; break;
case OP_DECLARE_SPECIFICATION:
name = "constraint";
break;
default: default:
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
@ -54,6 +57,7 @@ namespace synth {
if (logic == symbol::null) { if (logic == symbol::null) {
op_names.push_back(builtin_name("synthesiz3", OP_DECLARE_OUTPUT)); op_names.push_back(builtin_name("synthesiz3", OP_DECLARE_OUTPUT));
op_names.push_back(builtin_name("uncomputable", OP_DECLARE_GRAMMAR)); op_names.push_back(builtin_name("uncomputable", OP_DECLARE_GRAMMAR));
op_names.push_back(builtin_name("constraint", OP_DECLARE_SPECIFICATION));
} }
} }

2
src/ast/synth_decl_plugin.h
View file

@ -24,6 +24,7 @@ namespace synth {
enum op_kind { enum op_kind {
OP_DECLARE_OUTPUT, OP_DECLARE_OUTPUT,
OP_DECLARE_GRAMMAR, OP_DECLARE_GRAMMAR,
OP_DECLARE_SPECIFICATION,
LAST_OP LAST_OP
}; };
@ -51,6 +52,7 @@ namespace synth {
bool is_synthesiz3(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); } 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_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); }
}; };
} }

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

@ -85,6 +85,16 @@ namespace synth {
} }
} }
void solver::add_specification(app* e) {
// 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));
internalize(arg);
m_spec.insert(arg);
ctx.push(insert_obj_trail(m_spec, arg));
// TODO: assert arg <=> e
}
// recognize synthesis objectives here. // recognize synthesis objectives here.
sat::literal solver::internalize(expr* e, bool sign, bool root) { sat::literal solver::internalize(expr* e, bool sign, bool root) {
internalize(e); internalize(e);
@ -101,10 +111,13 @@ namespace synth {
sat::literal lit(bv, false); sat::literal lit(bv, false);
ctx.attach_lit(lit, e); ctx.attach_lit(lit, e);
synth::util util(m); synth::util util(m);
app* a = to_app(e);
if (util.is_synthesiz3(e)) if (util.is_synthesiz3(e))
add_synth_objective(to_app(e)); add_synth_objective(a);
if (util.is_grammar(e)) if (util.is_grammar(e))
add_uncomputable(to_app(e)); add_uncomputable(a);
if (util.is_specification(e))
add_specification(a);
} }
// display current state (eg. current set of realizers) // display current state (eg. current set of realizers)

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

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