mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-29 07:13:37 +00:00
Code Activity

Subterms Theory (#8115)

Browse source 
* somewhaat failed attempt at declaring subterm predicate

I can't really figure out how to link the smt parser to the rest of the
machinenery, so I will stop here and try from the other side. I'll start
implmenting the logic and see if it brings me back to the parser.

* initial logic implmentation

Very primitive, but I don't like have that much work uncommitted.

* parser implementation

* more theory

* Working base

* subterm reflexivity

* a few optimization

Skip adding obvious equalities or disequality

* removed some optimisations

* better handling of backtracking

* stupid segfault

Add m_subterm to the trail

* Update src/smt/theory_datatype.h

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/ast/rewriter/datatype_rewriter.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* review

* forgot to update `iterate_subterm`'s signature

* fix iterator segfault

* Remove duplicate include statement

Removed duplicate include of 'theory_datatype.h'.

* Replace 'optional' with 'std::option' in datatype_decl_plugin.h

* Add is_subterm_predicate matcher to datatype_decl_plugin

* Change std::option to std::optional for m_subterm

* Update pdecl.h

* Change has_subterm to use has_value method

* Update pdecl.cpp

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
This commit is contained in:
Simon Jeanteur 2026-01-13 19:53:17 +01:00 • committed by Nikolaj Bjorner
parent a6c1d32074
commit 9ca6580e38
9 changed files with 563 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -105,6 +105,7 @@ namespace smt2 {
symbol m_declare_type_var;
symbol m_declare_datatypes;
symbol m_declare_datatype;
symbol m_subterm_keyword;
symbol m_par;
symbol m_push;
symbol m_pop;
@ -955,7 +956,7 @@ namespace smt2 {
next();
}
// ( declare-datatype symbol datatype_dec)
// ( declare-datatype symbol datatype_dec [:subterm <subterm>])
void parse_declare_datatype() {
SASSERT(curr_is_identifier());
SASSERT(curr_id() == m_declare_datatype);
@ -974,8 +975,15 @@ namespace smt2 {
pdatatype_decl_ref d(pm());
pconstructor_decl_ref_buffer new_ct_decls(pm());
parse_datatype_dec(&dt_name, new_ct_decls);
symbol subterm_name = parse_subterm_decl();
d = pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.data());
if (subterm_name != symbol::null) {
d->set_subterm(subterm_name);
}
check_missing(d, line, pos);
check_duplicate(d, line, pos);
@ -985,6 +993,18 @@ namespace smt2 {
next();
}
// [:subterm <subterm>]
symbol parse_subterm_decl() {
symbol predicate_name = symbol::null;
if ((curr_is_identifier() || curr() == scanner::KEYWORD_TOKEN) && curr_id() == m_subterm_keyword) {
next(); // consume :subterm keyword
check_identifier("expected name for subterm predicate");
predicate_name = curr_id();
next();
}
return predicate_name;
}
// datatype_dec ::= ( constructor_dec+ ) | ( par ( symbol+ ) ( constructor_dec+ ) )
@ -3092,6 +3112,7 @@ namespace smt2 {
m_declare_type_var("declare-type-var"),
m_declare_datatypes("declare-datatypes"),
m_declare_datatype("declare-datatype"),
m_subterm_keyword(":subterm"),
m_par("par"),
m_push("push"),
m_pop("pop"),