mirror of
https://github.com/Z3Prover/z3
synced 2026-01-21 01:24:43 +00:00
deaced1711
* 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> |
||
|---|---|---|
| .. | ||
| extra_cmds | ||
| basic_cmds.cpp | ||
| basic_cmds.h | ||
| CMakeLists.txt | ||
| cmd_context.cpp | ||
| cmd_context.h | ||
| cmd_context_to_goal.cpp | ||
| cmd_context_to_goal.h | ||
| cmd_util.cpp | ||
| cmd_util.h | ||
| echo_tactic.cpp | ||
| echo_tactic.h | ||
| eval_cmd.cpp | ||
| eval_cmd.h | ||
| parametric_cmd.cpp | ||
| parametric_cmd.h | ||
| pdecl.cpp | ||
| pdecl.h | ||
| README | ||
| simplifier_cmds.cpp | ||
| simplifier_cmds.h | ||
| simplify_cmd.cpp | ||
| simplify_cmd.h | ||
| tactic_cmds.cpp | ||
| tactic_cmds.h | ||
| tactic_manager.cpp | ||
| tactic_manager.h | ||
Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0. It is also provides the solver abstraction to plugin solvers in this kind of front-end.