Subterms Theory #8115

puyral · 2026-01-06T23:09:40Z

This pull request introduces a subterm theory for datatypes, developed as part of the 199.029 SMT Solving Internals course at TU Wien.

The implementation seems functional to my testing, though there are known limitations and areas for improvement:

Mutually recursive datatypes are not supported. I did not want to introduce the complexity of polymorphism for my first time modifying z3.
Conflict propagation currently generates trivial equalities (e.g., equalities already decided in the current model or easily discardable by inspecting constructors). Attempts to optimize this led to unexpected issues, so the changes were reverted. The overhead is expected to be minimal, as these literal would quickly get back to the theory solver, where effectively the same code will be executed.
Model generation is not yet implemented.

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.

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

Skip adding obvious equalities or disequality

Add m_subterm to the trail

puyral · 2026-01-06T23:34:30Z

@microsoft-github-policy-service agree

NikolajBjorner · 2026-01-07T02:36:28Z

src/smt/theory_datatype.cpp

+
+        TRACE(datatype, tout << "propagate_not_is_subterm: " << enode_pp(n, ctx) << "\n";);
+
+        datatype_util util(get_manager());


NikolajBjorner · 2026-01-07T02:38:24Z

src/smt/theory_datatype.cpp

+                        TRACE(datatype, tout << "adding recursive case: " << mk_pp(arg1->get_expr(), m) << " ⊑ "
+                                             << mk_pp(s->get_expr(), m) << "\n";);
+                        app_ref sub_app(m.mk_app(sub_decl, arg1->get_expr(), s->get_expr()), m);
+                        ctx.internalize(sub_app, false);


it is probably mk_literal(sub_app) from base class in smt_theory.h instead of internalize + get_bool_var.

NikolajBjorner · 2026-01-07T02:50:50Z

I am not sure what you mean by that model generation isn't implemented. Subterm relationship is an interpreted function.
Maybe the simplifier can be completed by always returning true/false for ground data-type terms. But, assuming the datatype theory solver reaches a saturated state, then each uninterpreted datatype constant is given an interpretation without requiring to access the subterm predicate.

Copilot

Pull request overview

This PR introduces a subterm theory for datatypes as part of the SMT Solving Internals course at TU Wien. The implementation adds support for subterm predicates (⊑) that can express subterm relationships within datatype terms, with reflexivity axioms automatically generated and propagation logic integrated with the existing datatype theory solver.

Key Changes

Added subterm predicates as a new datatype operator (OP_DT_SUBTERM) with syntax support through :subterm keyword in SMT-LIB2 parser
Implemented propagation logic for subterm constraints including handling of true/false assignments and interaction with constructor information
Created a custom iterator pattern (subterm_iterator) for traversing subterms of datatype expressions

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 8 comments.

Show a summary per file

File	Description
src/smt/theory_datatype.h	Adds m_subterms tracking to var_data, declares subterm propagation methods, and introduces subterm_iterator class
src/smt/theory_datatype.cpp	Implements reflexivity axioms, propagation logic for subterm predicates, and subterm iterator functionality
src/parsers/smt2/smt2parser.cpp	Adds parsing support for `:subterm` keyword in datatype declarations
src/cmd_context/pdecl.h	Adds psubterm_decl class and optional m_subterm member to pdatatype_decl
src/cmd_context/pdecl.cpp	Implements display method and instantiation logic for subterm declarations
src/cmd_context/cmd_context.cpp	Registers subterm predicate function declarations in the command context
src/ast/datatype_decl_plugin.h	Declares subterm class, OP_DT_SUBTERM operator, and utility methods for subterm predicates
src/ast/datatype_decl_plugin.cpp	Implements subterm instantiation, mk_subterm factory method, and get_datatype_subterm lookup
src/ast/rewriter/datatype_rewriter.cpp	Adds case for OP_DT_SUBTERM (currently returns BR_FAILED, no rewriting)

Copilot · 2026-01-09T03:59:32Z

src/smt/theory_datatype.cpp

+            add_subterm_predicate(a, e);
+            add_subterm_predicate(b, e);
+
+            // propagating potentially adds a lot of litteral, avoid it if we can


Typo in comment: "litteral" should be "literals".

Suggested change

// propagating potentially adds a lot of litteral, avoid it if we can

// propagating potentially adds a lot of literals, avoid it if we can

Copilot · 2026-01-09T03:59:32Z

src/smt/theory_datatype.cpp

+    }
+
+    void theory_datatype::propagate_subterm(enode *n, bool is_true) {
+        force_push(); // I am faily sure I need that here


Typo in comment: "faily" should be "fairly".

Suggested change

force_push(); // I am faily sure I need that here

force_push(); // I am fairly sure I need that here

Copilot · 2026-01-09T03:59:32Z

src/ast/rewriter/datatype_rewriter.cpp

        return BR_DONE;        
    }
+    case OP_DT_SUBTERM:
+        // Re rewrite yet for subterms


Typo in comment: "Re rewrite yet" should be "No rewrite yet".

Suggested change

// Re rewrite yet for subterms

// No rewrite yet for subterms

Copilot · 2026-01-09T03:59:33Z

src/smt/theory_datatype.cpp

+     *
+     * With `predicate:='a ⊑ b'` this should be called with `v:='a'` and `v:='b'`.
+     * 
+     * This doesn't handle potential propagation. The responsability for it


Typo in comment: "responsability" should be "responsibility".

Suggested change

* This doesn't handle potential propagation. The responsability for it

* This doesn't handle potential propagation. The responsibility for it

Copilot · 2026-01-09T03:59:33Z

src/smt/theory_datatype.h

+        subterm_iterator(const subterm_iterator&) = delete;
+
+        subterm_iterator begin() {
+            return std::move(*this);
+        }
+        subterm_iterator end() {


The iterator pattern has a bug. When used in a range-based for loop (line 723), begin() moves from the iterator object, leaving it in a moved-from state. Then end() is called on the same moved-from object. While this might work in practice because end() only checks m_current, it's undefined behavior to use a moved-from object. The proper pattern would be to either: (1) have begin() and end() return separate iterator objects, not move from this; or (2) make this a proper range type with separate iterator and sentinel types.

Suggested change

subterm_iterator(const subterm_iterator&) = delete;

subterm_iterator begin() {

return std::move(*this);

}

subterm_iterator end() {

subterm_iterator(const subterm_iterator& other)

: m_todo(other.m_todo),

m_marked(other.m_marked),

m_manager(other.m_manager),

m_current(other.m_current) {

}

subterm_iterator begin() const {

return *this;

}

subterm_iterator end() const {

Copilot · 2026-01-09T03:59:33Z

src/smt/theory_datatype.cpp

+#include "theory_datatype.h"



Redundant include: theory_datatype.h is already included on line 25, so the duplicate include on line 29 should be removed.

Suggested change

#include "theory_datatype.h"

Copilot · 2026-01-09T03:59:33Z

src/cmd_context/pdecl.h

+    friend class pdecl_manager;
+    friend class pdatatype_decl;
+    symbol                     m_name;
+    ptype    m_type;


The psubterm_decl class declares a member variable m_type on line 237, but it is never initialized or used. This appears to be a copy-paste artifact from paccessor_decl. Either this member should be removed, or if it's intended for future use, it should be initialized in the constructor.

Suggested change

ptype m_type;

Copilot · 2026-01-09T03:59:34Z

src/smt/theory_datatype.cpp

+    void theory_datatype::assert_subterm_axioms(enode * n) {
+        sort * s = n->get_sort();
+        if (m_util.is_datatype(s)) {
+            func_decl * sub_decl = m_util.get_datatype_subterm(s);
+            if (sub_decl) {
+                TRACE(datatype, tout << "asserting reflexivity for #" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << "\n";);
+                app_ref reflex(m.mk_app(sub_decl, n->get_expr(), n->get_expr()), m);
+                ctx.internalize(reflex, false);
+                literal l(ctx.get_bool_var(reflex));
+                ctx.mark_as_relevant(l);
+                ctx.mk_th_axiom(get_id(), 1, &l);
+            }
+        }
+    }


The subterm theory feature lacks test coverage. Given that the repository has comprehensive test coverage for datatype functionality (see src/test/parametric_datatype.cpp, src/test/simplifier.cpp with test_datatypes(), etc.), the new subterm predicates should have corresponding tests to verify correct behavior, including basic reflexivity, transitivity checks, propagation with constructors, and conflict detection.

puyral and others added 10 commits January 6, 2026 23:42

somewhaat failed attempt at declaring subterm predicate

7761ffd

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

0ffd342

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

parser implementation

9ce5a93

more theory

8494ec7

Working base

be0a81b

subterm reflexivity

882b79b

a few optimization

0a5a0d6

Skip adding obvious equalities or disequality

removed some optimisations

778ae44

better handling of backtracking

93cbd35

stupid segfault

49a4004

Add m_subterm to the trail

NikolajBjorner reviewed Jan 7, 2026

View reviewed changes

NikolajBjorner marked this pull request as ready for review January 7, 2026 02:47

Copilot AI mentioned this pull request Jan 9, 2026

[WIP] Update pull request based on code review remarks #8127

Closed

NikolajBjorner requested a review from Copilot January 9, 2026 03:53

Copilot started reviewing on behalf of NikolajBjorner January 9, 2026 03:54 View session

Copilot AI reviewed Jan 9, 2026

View reviewed changes


		TRACE(datatype, tout << "propagate_not_is_subterm: " << enode_pp(n, ctx) << "\n";);

		datatype_util util(get_manager());

	// propagating potentially adds a lot of litteral, avoid it if we can
	// propagating potentially adds a lot of literals, avoid it if we can

	force_push(); // I am faily sure I need that here
	force_push(); // I am fairly sure I need that here

	// Re rewrite yet for subterms
	// No rewrite yet for subterms

	* This doesn't handle potential propagation. The responsability for it
	* This doesn't handle potential propagation. The responsibility for it

-        subterm_iterator(const subterm_iterator&) = delete;
-        subterm_iterator begin() {
-            return std::move(*this);
-        }
-        subterm_iterator end() {
+        subterm_iterator(const subterm_iterator& other)
+            : m_todo(other.m_todo),
+              m_marked(other.m_marked),
+              m_manager(other.m_manager),
+              m_current(other.m_current) {
+        }
+        subterm_iterator begin() const {
+            return *this;
+        }
+        subterm_iterator end() const {

Subterms Theory #8115

Are you sure you want to change the base?

Subterms Theory #8115

Conversation

puyral commented Jan 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

puyral commented Jan 6, 2026

Uh oh!

NikolajBjorner Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

NikolajBjorner Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

NikolajBjorner commented Jan 7, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Key Changes

Reviewed changes

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jan 9, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

puyral commented Jan 6, 2026 •

edited

Loading