* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663).
* add prd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing text
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix#7647
* fix#7647 - with respect to scope level
* initial stab at randomizer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Create prd.yml
* missing text
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update prd.yml
* allows setting simplifier factory independently of whether solver has been allocated.
Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command
```
(set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify))
```
This command can be invoked any time prior to push or adding assertions.
The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior.
* remove experiment from pr
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).
The WIP SMTLIB3 format is assumed to be supporting the following declaration
```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).
The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.
This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers
Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
This commit overhauls the proof format (in development) for the new core.
NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.
It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):
- assume - for input clauses
- learn - when a clause is learned (or redundant clause is added)
- del - when a clause is deleted.
The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.
Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.
Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```
Run z3 on a file with above content.
Then run z3 on f.proof
```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```
Adding new API object to maintain state between calls to parser.
The state is incremental: all declarations of sorts and functions are valid in the next parse. The parser produces an ast-vector of assertions that are parsed in the current calls.
The following is a unit test:
```
from z3 import *
pc = ParserContext()
A = DeclareSort('A')
pc.add_sort(A)
print(pc.from_string("(declare-const x A) (declare-const y A) (assert (= x y))"))
print(pc.from_string("(declare-const z A) (assert (= x z))"))
print(parse_smt2_string("(declare-const x Int) (declare-const y Int) (assert (= x y))"))
s = Solver()
s.from_string("(declare-sort A)")
s.from_string("(declare-const x A)")
s.from_string("(declare-const y A)")
s.from_string("(assert (= x y))")
print(s.assertions())
s.from_string("(declare-const z A)")
print(s.assertions())
s.from_string("(assert (= x z))")
print(s.assertions())
```
It produces results of the form
```
[x == y]
[x == z]
[x == y]
[x == y]
[x == y]
[x == y, x == z]
```
Thus, the set of assertions returned by a parse call is just the set of assertions added.
The solver maintains state between parser calls so that declarations made in a previous call are still available when declaring the constant 'z'.
The same holds for the parser_context_from_string function: function and sort declarations either added externally or declared using SMTLIB2 command line format as strings are valid for later calls.
