Merge branch 'master' into jfleisher/nightlyversion

.github/workflows/coverage.yml

@@ -56,9 +56,10 @@ jobs:
         ./test-z3 -a
         cd -
 
+# Disabled:       ${{github.workspace}}/build/examples/c_example_build_dir/c_example
+
     - name: Run examples
       run: |
-        ${{github.workspace}}/build/examples/c_example_build_dir/c_example
         ${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example
         ${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help
         ${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt

.github/workflows/docker-image.yml

@@ -41,7 +41,7 @@ jobs:
             type=edge
             type=sha,prefix=ubuntu-20.04-bare-z3-sha-
       - name: Build and push Bare Z3 Docker Image
-        uses: docker/build-push-action@v3.1.1
+        uses: docker/build-push-action@v3.2.0
         with:  
           context: .
           push: true

.github/workflows/msvc-static-build.yml

@@ -0,0 +1,23 @@
+name: MSVC Static Build
+  
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read # to fetch code (actions/checkout)
+
+jobs:
+  build:
+    runs-on: windows-2019
+    env:
+      BUILD_TYPE: Release
+    steps:
+    - name: Checkout Repo
+      uses: actions/checkout@v3
+  
+    - name: Build
+      run: |
+        cmake -B build -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DZ3_BUILD_LIBZ3_SHARED=OFF -DZ3_BUILD_LIBZ3_MSVC_STATIC=ON
+        cmake --build build --config ${{ env.BUILD_TYPE }} --parallel
+        

.github/workflows/wasm-release.yml

@@ -12,6 +12,9 @@ defaults:
 env:
   EM_VERSION: 3.1.15
 
+permissions:
+  contents: read # to fetch code (actions/checkout)
+
 jobs:
   publish:
     name: Publish

.github/workflows/wasm.yml

@@ -12,6 +12,9 @@ defaults:
 env:
   EM_VERSION: 3.1.15
 
+permissions:
+  contents: read # to fetch code (actions/checkout)
+
 jobs:
   check:
     name: Check

.gitignore

@@ -81,6 +81,8 @@ src/api/js/node_modules/
 src/api/js/build/
 src/api/js/**/*.__GENERATED__.*
 debug/*
+examples/python/z3
+examples/python/libz3.dll
 
 out/**
 *.bak
@@ -93,3 +95,4 @@ CMakeSettings.json
 *.swp
 .DS_Store
 dbg/**
+*.wsp

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.11.1.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version
@@ -304,6 +304,7 @@ endif()
 # Option to control what type of library we build
 ################################################################################
 option(Z3_BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON)
+option(Z3_BUILD_LIBZ3_MSVC_STATIC "Build libz3 as a statically-linked runtime library"                   OFF)
 
 
 ################################################################################

Parameters.md

@@ -1,605 +0,0 @@
-## Module pi
-
-Description: pattern inference (heuristics) for universal formulas (without annotation)
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-arith | unsigned int  |  0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms | 1
-arith_weight | unsigned int  |  default weight for quantifiers where the only available pattern has nested arithmetic terms | 5
-block_loop_patterns | bool  |  block looping patterns during pattern inference | true
-max_multi_patterns | unsigned int  |  when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern | 0
-non_nested_arith_weight | unsigned int  |  default weight for quantifiers where the only available pattern has non nested arithmetic terms | 10
-pull_quantifiers | bool  |  pull nested quantifiers, if no pattern was found | true
-use_database | bool  |  use pattern database | false
-warnings | bool  |  enable/disable warning messages in the pattern inference module | false
-
-## Module tactic
-
-Description: tactic parameters
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-blast_term_ite.max_inflation | unsigned int  |  multiplicative factor of initial term size. | 4294967295
-blast_term_ite.max_steps | unsigned int  |  maximal number of steps allowed for tactic. | 4294967295
-default_tactic | symbol  |  overwrite default tactic in strategic solver | 
-propagate_values.max_rounds | unsigned int  |  maximal number of rounds to propagate values. | 4
-solve_eqs.context_solve | bool  |  solve equalities within disjunctions. | true
-solve_eqs.ite_solver | bool  |  use if-then-else solvers. | true
-solve_eqs.max_occs | unsigned int  |  maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295
-solve_eqs.theory_solver | bool  |  use theory solvers. | true
-
-## Module pp
-
-Description: pretty printer
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-bounded | bool  |  ignore characters exceeding max width | false
-bv_literals | bool  |  use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing | true
-bv_neg | bool  |  use bvneg when displaying Bit-Vector literals where the most significant bit is 1 | false
-decimal | bool  |  pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise | false
-decimal_precision | unsigned int  |  maximum number of decimal places to be used when pp.decimal=true | 10
-fixed_indent | bool  |  use a fixed indentation for applications | false
-flat_assoc | bool  |  flat associative operators (when pretty printing SMT2 terms/formulas) | true
-fp_real_literals | bool  |  use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing | false
-max_depth | unsigned int  |  max. term depth (when pretty printing SMT2 terms/formulas) | 5
-max_indent | unsigned int  |  max. indentation in pretty printer | 4294967295
-max_num_lines | unsigned int  |  max. number of lines to be displayed in pretty printer | 4294967295
-max_ribbon | unsigned int  |  max. ribbon (width - indentation) in pretty printer | 80
-max_width | unsigned int  |  max. width in pretty printer | 80
-min_alias_size | unsigned int  |  min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas) | 10
-pretty_proof | bool  |  use slower, but prettier, printer for proofs | false
-simplify_implies | bool  |  simplify nested implications for pretty printing | true
-single_line | bool  |  ignore line breaks when true | false
-
-## Module sat
-
-Description: propositional SAT solver
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-abce | bool  |  eliminate blocked clauses using asymmetric literals | false
-acce | bool  |  eliminate covered clauses using asymmetric added literals | false
-anf | bool  |  enable ANF based simplification in-processing | false
-anf.delay | unsigned int  |  delay ANF simplification by in-processing round | 2
-anf.exlin | bool  |  enable extended linear simplification | false
-asymm_branch | bool  |  asymmetric branching | true
-asymm_branch.all | bool  |  asymmetric branching on all literals per clause | false
-asymm_branch.delay | unsigned int  |  number of simplification rounds to wait until invoking asymmetric branch simplification | 1
-asymm_branch.limit | unsigned int  |  approx. maximum number of literals visited during asymmetric branching | 100000000
-asymm_branch.rounds | unsigned int  |  maximal number of rounds to run asymmetric branch simplifications if progress is made | 2
-asymm_branch.sampled | bool  |  use sampling based asymmetric branching based on binary implication graph | true
-ate | bool  |  asymmetric tautology elimination | true
-backtrack.conflicts | unsigned int  |  number of conflicts before enabling chronological backtracking | 4000
-backtrack.scopes | unsigned int  |  number of scopes to enable chronological backtracking | 100
-bca | bool  |  blocked clause addition - add blocked binary clauses | false
-bce | bool  |  eliminate blocked clauses | false
-bce_at | unsigned int  |  eliminate blocked clauses only once at the given simplification round | 2
-bce_delay | unsigned int  |  delay eliminate blocked clauses until simplification round | 2
-binspr | bool  |  enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models | false
-blocked_clause_limit | unsigned int  |  maximum number of literals visited during blocked clause elimination | 100000000
-branching.anti_exploration | bool  |  apply anti-exploration heuristic for branch selection | false
-branching.heuristic | symbol  |  branching heuristic vsids, chb | vsids
-burst_search | unsigned int  |  number of conflicts before first global simplification | 100
-cardinality.encoding | symbol  |  encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit | grouped
-cardinality.solver | bool  |  use cardinality solver | true
-cce | bool  |  eliminate covered clauses | false
-core.minimize | bool  |  minimize computed core | false
-core.minimize_partial | bool  |  apply partial (cheap) core minimization | false
-cut | bool  |  enable AIG based simplification in-processing | false
-cut.aig | bool  |  extract aigs (and ites) from cluases for cut simplification | false
-cut.delay | unsigned int  |  delay cut simplification by in-processing round | 2
-cut.dont_cares | bool  |  integrate dont cares with cuts | true
-cut.force | bool  |  force redoing cut-enumeration until a fixed-point | false
-cut.lut | bool  |  extract luts from clauses for cut simplification | false
-cut.npn3 | bool  |  extract 3 input functions from clauses for cut simplification | false
-cut.redundancies | bool  |  integrate redundancy checking of cuts | true
-cut.xor | bool  |  extract xors from clauses for cut simplification | false
-ddfw.init_clause_weight | unsigned int  |  initial clause weight for DDFW local search | 8
-ddfw.reinit_base | unsigned int  |  increment basis for geometric backoff scheme of re-initialization of weights | 10000
-ddfw.restart_base | unsigned int  |  number of flips used a starting point for hessitant restart backoff | 100000
-ddfw.threads | unsigned int  |  number of ddfw threads to run in parallel with sat solver | 0
-ddfw.use_reward_pct | unsigned int  |  percentage to pick highest reward variable when it has reward 0 | 15
-ddfw_search | bool  |  use ddfw local search instead of CDCL | false
-dimacs.core | bool  |  extract core from DIMACS benchmarks | false
-drat.activity | bool  |  dump variable activities | false
-drat.binary | bool  |  use Binary DRAT output format | false
-drat.check_sat | bool  |  build up internal trace, check satisfying model | false
-drat.check_unsat | bool  |  build up internal proof and check | false
-drat.file | symbol  |  file to dump DRAT proofs | 
-drup.trim | bool  |  build and trim drup proof | false
-dyn_sub_res | bool  |  dynamic subsumption resolution for minimizing learned clauses | true
-elim_vars | bool  |  enable variable elimination using resolution during simplification | true
-elim_vars_bdd | bool  |  enable variable elimination using BDD recompilation during simplification | true
-elim_vars_bdd_delay | unsigned int  |  delay elimination of variables using BDDs until after simplification round | 3
-enable_pre_simplify | bool  |  enable pre simplifications before the bounded search | false
-euf | bool  |  enable euf solver (this feature is preliminary and not ready for general consumption) | false
-force_cleanup | bool  |  force cleanup to remove tautologies and simplify clauses | false
-gc | symbol  |  garbage collection strategy: psm, glue, glue_psm, dyn_psm | glue_psm
-gc.burst | bool  |  perform eager garbage collection during initialization | false
-gc.defrag | bool  |  defragment clauses when garbage collecting | true
-gc.increment | unsigned int  |  increment to the garbage collection threshold | 500
-gc.initial | unsigned int  |  learned clauses garbage collection frequency | 20000
-gc.k | unsigned int  |  learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm) | 7
-gc.small_lbd | unsigned int  |  learned clauses with small LBD are never deleted (only used in dyn_psm) | 3
-inprocess.max | unsigned int  |  maximal number of inprocessing passes | 4294967295
-inprocess.out | symbol  |  file to dump result of the first inprocessing step and exit | 
-local_search | bool  |  use local search instead of CDCL | false
-local_search_dbg_flips | bool  |  write debug information for number of flips | false
-local_search_mode | symbol  |  local search algorithm, either default wsat or qsat | wsat
-local_search_threads | unsigned int  |  number of local search threads to find satisfiable solution | 0
-lookahead.cube.cutoff | symbol  |  cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat | depth
-lookahead.cube.depth | unsigned int  |  cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth. | 1
-lookahead.cube.fraction | double  |  adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat | 0.4
-lookahead.cube.freevars | double  |  cube free variable fraction. Used when lookahead.cube.cutoff is freevars | 0.8
-lookahead.cube.psat.clause_base | double  |  clause base for PSAT cutoff | 2
-lookahead.cube.psat.trigger | double  |  trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5
-lookahead.cube.psat.var_exp | double  |  free variable exponent for PSAT cutoff | 1
-lookahead.delta_fraction | double  |  number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0
-lookahead.double | bool  |  enable doubld lookahead | true
-lookahead.global_autarky | bool  |  prefer to branch on variables that occur in clauses that are reduced | false
-lookahead.preselect | bool  |  use pre-selection of subset of variables for branching | false
-lookahead.reward | symbol  |  select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu
-lookahead.use_learned | bool  |  use learned clauses when selecting lookahead literal | false
-lookahead_scores | bool  |  extract lookahead scores. A utility that can only be used from the DIMACS front-end | false
-lookahead_simplify | bool  |  use lookahead solver during simplification | false
-lookahead_simplify.bca | bool  |  add learned binary clauses as part of lookahead simplification | true
-max_conflicts | unsigned int  |  maximum number of conflicts | 4294967295
-max_memory | unsigned int  |  maximum amount of memory in megabytes | 4294967295
-minimize_lemmas | bool  |  minimize learned clauses | true
-override_incremental | bool  |  override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused | false
-pb.lemma_format | symbol  |  generate either cardinality or pb lemmas | cardinality
-pb.min_arity | unsigned int  |  minimal arity to compile pb/cardinality constraints to CNF | 9
-pb.resolve | symbol  |  resolution strategy for boolean algebra solver: cardinality, rounding | cardinality
-pb.solver | symbol  |  method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver) | solver
-phase | symbol  |  phase selection strategy: always_false, always_true, basic_caching, random, caching | caching
-phase.sticky | bool  |  use sticky phase caching | true
-prob_search | bool  |  use probsat local search instead of CDCL | false
-probing | bool  |  apply failed literal detection during simplification | true
-probing_binary | bool  |  probe binary clauses | true
-probing_cache | bool  |  add binary literals as lemmas | true
-probing_cache_limit | unsigned int  |  cache binaries unless overall memory usage exceeds cache limit | 1024
-probing_limit | unsigned int  |  limit to the number of probe calls | 5000000
-propagate.prefetch | bool  |  prefetch watch lists for assigned literals | true
-random_freq | double  |  frequency of random case splits | 0.01
-random_seed | unsigned int  |  random seed | 0
-reorder.activity_scale | unsigned int  |  scaling factor for activity update | 100
-reorder.base | unsigned int  |  number of conflicts per random reorder  | 4294967295
-reorder.itau | double  |  inverse temperature for softmax | 4.0
-rephase.base | unsigned int  |  number of conflicts per rephase  | 1000
-resolution.cls_cutoff1 | unsigned int  |  limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination | 100000000
-resolution.cls_cutoff2 | unsigned int  |  limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination | 700000000
-resolution.limit | unsigned int  |  approx. maximum number of literals visited during variable elimination | 500000000
-resolution.lit_cutoff_range1 | unsigned int  |  second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 700
-resolution.lit_cutoff_range2 | unsigned int  |  second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 400
-resolution.lit_cutoff_range3 | unsigned int  |  second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 300
-resolution.occ_cutoff | unsigned int  |  first cutoff (on number of positive/negative occurrences) for Boolean variable elimination | 10
-resolution.occ_cutoff_range1 | unsigned int  |  second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 8
-resolution.occ_cutoff_range2 | unsigned int  |  second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 5
-resolution.occ_cutoff_range3 | unsigned int  |  second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 3
-restart | symbol  |  restart strategy: static, luby, ema or geometric | ema
-restart.emafastglue | double  |  ema alpha factor for fast moving average | 0.03
-restart.emaslowglue | double  |  ema alpha factor for slow moving average | 1e-05
-restart.factor | double  |  restart increment factor for geometric strategy | 1.5
-restart.fast | bool  |  use fast restart approach only removing less active literals. | true
-restart.initial | unsigned int  |  initial restart (number of conflicts) | 2
-restart.margin | double  |  margin between fast and slow restart factors. For ema | 1.1
-restart.max | unsigned int  |  maximal number of restarts. | 4294967295
-retain_blocked_clauses | bool  |  retain blocked clauses as lemmas | true
-scc | bool  |  eliminate Boolean variables by computing strongly connected components | true
-scc.tr | bool  |  apply transitive reduction, eliminate redundant binary clauses | true
-search.sat.conflicts | unsigned int  |  period for solving for sat (in number of conflicts) | 400
-search.unsat.conflicts | unsigned int  |  period for solving for unsat (in number of conflicts) | 400
-simplify.delay | unsigned int  |  set initial delay of simplification by a conflict count | 0
-subsumption | bool  |  eliminate subsumed clauses | true
-subsumption.limit | unsigned int  |  approx. maximum number of literals visited during subsumption (and subsumption resolution) | 100000000
-threads | unsigned int  |  number of parallel threads to use | 1
-variable_decay | unsigned int  |  multiplier (divided by 100) for the VSIDS activity increment | 110
-
-## Module solver
-
-Description: solver parameters
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-axioms2files | bool  |  print negated theory axioms to separate files during search | false
-cancel_backup_file | symbol  |  file to save partial search state if search is canceled | 
-lemmas2console | bool  |  print lemmas during search | false
-smtlib2_log | symbol  |  file to save solver interaction | 
-timeout | unsigned int  |  timeout on the solver object; overwrites a global timeout | 4294967295
-
-## Module opt
-
-Description: optimization parameters
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-dump_benchmarks | bool  |  dump benchmarks for profiling | false
-dump_models | bool  |  display intermediary models to stdout | false
-elim_01 | bool  |  eliminate 01 variables | true
-enable_core_rotate | bool  |  enable core rotation to both sample cores and correction sets | false
-enable_lns | bool  |  enable LNS during weighted maxsat | false
-enable_sat | bool  |  enable the new SAT core for propositional constraints | true
-enable_sls | bool  |  enable SLS tuning during weighted maxsat | false
-incremental | bool  |  set incremental mode. It disables pre-processing and enables adding constraints in model event handler | false
-lns_conflicts | unsigned int  |  initial conflict count for LNS search | 1000
-maxlex.enable | bool  |  enable maxlex heuristic for lexicographic MaxSAT problems | true
-maxres.add_upper_bound_block | bool  |  restict upper bound with constraint | false
-maxres.hill_climb | bool  |  give preference for large weight cores | true
-maxres.max_core_size | unsigned int  |  break batch of generated cores if size reaches this number | 3
-maxres.max_correction_set_size | unsigned int  |  allow generating correction set constraints up to maximal size | 3
-maxres.max_num_cores | unsigned int  |  maximal number of cores per round | 200
-maxres.maximize_assignment | bool  |  find an MSS/MCS to improve current assignment | false
-maxres.pivot_on_correction_set | bool  |  reduce soft constraints if the current correction set is smaller than current core | true
-maxres.wmax | bool  |  use weighted theory solver to constrain upper bounds | false
-maxsat_engine | symbol  |  select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2' | maxres
-optsmt_engine | symbol  |  select optimization engine: 'basic', 'symba' | basic
-pb.compile_equality | bool  |  compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) | false
-pp.neat | bool  |  use neat (as opposed to less readable, but faster) pretty printer when displaying context | true
-pp.wcnf | bool  |  print maxsat benchmark into wcnf format | false
-priority | symbol  |  select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box' | lex
-rc2.totalizer | bool  |  use totalizer for rc2 encoding | true
-rlimit | unsigned int  |  resource limit (0 means no limit) | 0
-solution_prefix | symbol  |  path prefix to dump intermediary, but non-optimal, solutions | 
-timeout | unsigned int  |  timeout (in milliseconds) (UINT_MAX and 0 mean no timeout) | 4294967295
-
-## Module parallel
-
-Description: parameters for parallel solver
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-conquer.backtrack_frequency | unsigned int  |  frequency to apply core minimization during conquer | 10
-conquer.batch_size | unsigned int  |  number of cubes to batch together for fast conquer | 100
-conquer.delay | unsigned int  |  delay of cubes until applying conquer | 10
-conquer.restart.max | unsigned int  |  maximal number of restarts during conquer phase | 5
-enable | bool  |  enable parallel solver by default on selected tactics (for QF_BV) | false
-simplify.exp | double  |  restart and inprocess max is multiplied by simplify.exp ^ depth | 1
-simplify.inprocess.max | unsigned int  |  maximal number of inprocessing steps during simplification | 2
-simplify.max_conflicts | unsigned int  |  maximal number of conflicts during simplifcation phase | 4294967295
-simplify.restart.max | unsigned int  |  maximal number of restarts during simplification phase | 5000
-threads.max | unsigned int  |  caps maximal number of threads below the number of processors | 10000
-
-## Module nnf
-
-Description: negation normal form
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-ignore_labels | bool  |  remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false
-max_memory | unsigned int  |  maximum amount of memory in megabytes | 4294967295
-mode | symbol  |  NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem
-sk_hack | bool  |  hack for VCC | false
-
-## Module algebraic
-
-Description: real algebraic number package. Non-default parameter settings are not supported
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-factor | bool  |  use polynomial factorization to simplify polynomials representing algebraic numbers | true
-factor_max_prime | unsigned int  |  parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31
-factor_num_primes | unsigned int  |  parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1
-factor_search_size | unsigned int  |  parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space | 5000
-min_mag | unsigned int  |  Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16
-zero_accuracy | unsigned int  |  one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0
-
-## Module combined_solver
-
-Description: combines two solvers: non-incremental (solver1) and incremental (solver2)
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-ignore_solver1 | bool  |  if true, solver 2 is always used | false
-solver2_timeout | unsigned int  |  fallback to solver 1 after timeout even when in incremental model | 4294967295
-solver2_unknown | unsigned int  |  what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1 | 1
-
-## Module rcf
-
-Description: real closed fields
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-clean_denominators | bool  |  clean denominators before root isolation | true
-inf_precision | unsigned int  |  a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values | 24
-initial_precision | unsigned int  |  a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division | 24
-lazy_algebraic_normalization | bool  |  during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monic | true
-max_precision | unsigned int  |  during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision | 128
-use_prem | bool  |  use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences | true
-ERROR: unknown module 'rewriter, description: new formula simplification module used in the tactic framework'
-
-## Module ackermannization
-
-Description: solving UF via ackermannization
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-eager | bool  |  eagerly instantiate all congruence rules | true
-inc_sat_backend | bool  |  use incremental SAT | false
-sat_backend | bool  |  use SAT rather than SMT in qfufbv_ackr_tactic | false
-
-## Module nlsat
-
-Description: nonlinear solver
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-check_lemmas | bool  |  check lemmas on the fly using an independent nlsat solver | false
-factor | bool  |  factor polynomials produced during conflict resolution. | true
-inline_vars | bool  |  inline variables that can be isolated from equations (not supported in incremental mode) | false
-lazy | unsigned int  |  how lazy the solver is. | 0
-log_lemmas | bool  |  display lemmas as self-contained SMT formulas | false
-max_conflicts | unsigned int  |  maximum number of conflicts. | 4294967295
-max_memory | unsigned int  |  maximum amount of memory in megabytes | 4294967295
-minimize_conflicts | bool  |  minimize conflicts | false
-randomize | bool  |  randomize selection of a witness in nlsat. | true
-reorder | bool  |  reorder variables. | true
-seed | unsigned int  |  random seed. | 0
-shuffle_vars | bool  |  use a random variable order. | false
-simplify_conflicts | bool  |  simplify conflicts using equalities before resolving them in nlsat solver. | true
-
-
-## Module fp
-
-Description: fixedpoint parameters
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-bmc.linear_unrolling_depth | unsigned int  |  Maximal level to explore | 4294967295
-datalog.all_or_nothing_deltas | bool  |  compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not | false
-datalog.check_relation | symbol  |  name of default relation to check. operations on the default relation will be verified using SMT solving | null
-datalog.compile_with_widening | bool  |  widening will be used to compile recursive rules | false
-datalog.dbg_fpr_nonempty_relation_signature | bool  |  if true, finite_product_relation will attempt to avoid creating inner relation with empty signature by putting in half of the table columns, if it would have been empty otherwise | false
-datalog.default_relation | symbol  |  default relation implementation: external_relation, pentagon | pentagon
-datalog.default_table | symbol  |  default table implementation: sparse, hashtable, bitvector, interval | sparse
-datalog.default_table_checked | bool  |  if true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table | false
-datalog.default_table_checker | symbol  |  see default_table_checked | null
-datalog.explanations_on_relation_level | bool  |  if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect) | false
-datalog.generate_explanations | bool  |  produce explanations for produced facts when using the datalog engine | false
-datalog.initial_restart_timeout | unsigned int  |  length of saturation run before the first restart (in ms), zero means no restarts | 0
-datalog.magic_sets_for_queries | bool  |  magic set transformation will be used for queries | false
-datalog.output_profile | bool  |  determines whether profile information should be output when outputting Datalog rules or instructions | false
-datalog.print.tuples | bool  |  determines whether tuples for output predicates should be output | true
-datalog.profile_timeout_milliseconds | unsigned int  |  instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list | 0
-datalog.similarity_compressor | bool  |  rules that differ only in values of constants will be merged into a single rule | true
-datalog.similarity_compressor_threshold | unsigned int  |  if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged | 11
-datalog.subsumption | bool  |  if true, removes/filters predicates with total transitions | true
-datalog.timeout | unsigned int  |  Time limit used for saturation | 0
-datalog.unbound_compressor | bool  |  auxiliary relations will be introduced to avoid unbound variables in rule heads | true
-datalog.use_map_names | bool  |  use names from map files when displaying tuples | true
-engine | symbol  |  Select: auto-config, datalog, bmc, spacer | auto-config
-generate_proof_trace | bool  |  trace for 'sat' answer as proof object | false
-print_aig | symbol  |  Dump clauses in AIG text format (AAG) to the given file name | 
-print_answer | bool  |  print answer instance(s) to query | false
-print_boogie_certificate | bool  |  print certificate for reachability or non-reachability using a format understood by Boogie | false
-print_certificate | bool  |  print certificate for reachability or non-reachability | false
-print_fixedpoint_extensions | bool  |  use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules | true
-print_low_level_smt2 | bool  |  use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable) | false
-print_statistics | bool  |  print statistics | false
-print_with_variable_declarations | bool  |  use variable declarations when displaying rules (instead of attempting to use original names) | true
-spacer.arith.solver | unsigned int  |  arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 2
-spacer.blast_term_ite_inflation | unsigned int  |  Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative) | 3
-spacer.ctp | bool  |  Enable counterexample-to-pushing | true
-spacer.dump_benchmarks | bool  |  Dump SMT queries as benchmarks | false
-spacer.dump_threshold | double  |  Threshold in seconds on dumping benchmarks | 5.0
-spacer.elim_aux | bool  |  Eliminate auxiliary variables in reachability facts | true
-spacer.eq_prop | bool  |  Enable equality and bound propagation in arithmetic | true
-spacer.gpdr | bool  |  Use GPDR solving strategy for non-linear CHC | false
-spacer.gpdr.bfs | bool  |  Use BFS exploration strategy for expanding model search | true
-spacer.ground_pobs | bool  |  Ground pobs by using values from a model | true
-spacer.iuc | unsigned int  |  0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization | 1
-spacer.iuc.arith | unsigned int  |  0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin | 1
-spacer.iuc.debug_proof | bool  |  prints proof used by unsat-core-learner for debugging purposes (debugging) | false
-spacer.iuc.old_hyp_reducer | bool  |  use old hyp reducer instead of new implementation, for debugging only | false
-spacer.iuc.print_farkas_stats | bool  |  prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging) | false
-spacer.iuc.split_farkas_literals | bool  |  Split Farkas literals | false
-spacer.keep_proxy | bool  |  keep proxy variables (internal parameter) | true
-spacer.logic | symbol  |  SMT-LIB logic to configure internal SMT solvers | 
-spacer.max_level | unsigned int  |  Maximum level to explore | 4294967295
-spacer.max_num_contexts | unsigned int  |  maximal number of contexts to create | 500
-spacer.mbqi | bool  |  Enable mbqi | true
-spacer.min_level | unsigned int  |  Minimal level to explore | 0
-spacer.native_mbp | bool  |  Use native mbp of Z3 | true
-spacer.order_children | unsigned int  |  SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random) | 0
-spacer.p3.share_invariants | bool  |  Share invariants lemmas | false
-spacer.p3.share_lemmas | bool  |  Share frame lemmas | false
-spacer.print_json | symbol  |  Print pobs tree in JSON format to a given file | 
-spacer.propagate | bool  |  Enable propagate/pushing phase | true
-spacer.push_pob | bool  |  push blocked pobs to higher level | false
-spacer.push_pob_max_depth | unsigned int  |  Maximum depth at which push_pob is enabled | 4294967295
-spacer.q3 | bool  |  Allow quantified lemmas in frames | true
-spacer.q3.instantiate | bool  |  Instantiate quantified lemmas | true
-spacer.q3.qgen.normalize | bool  |  normalize cube before quantified generalization | true
-spacer.q3.use_qgen | bool  |  use quantified lemma generalizer | false
-spacer.random_seed | unsigned int  |  Random seed to be used by SMT solver | 0
-spacer.reach_dnf | bool  |  Restrict reachability facts to DNF | true
-spacer.reset_pob_queue | bool  |  SPACER: reset pob obligation queue when entering a new level | true
-spacer.restart_initial_threshold | unsigned int  |  Initial threshold for restarts | 10
-spacer.restarts | bool  |  Enable resetting obligation queue | false
-spacer.simplify_lemmas_post | bool  |  simplify derived lemmas after inductive propagation | false
-spacer.simplify_lemmas_pre | bool  |  simplify derived lemmas before inductive propagation | false
-spacer.simplify_pob | bool  |  simplify pobs by removing redundant constraints | false
-spacer.trace_file | symbol  |  Log file for progress events | 
-spacer.use_array_eq_generalizer | bool  |  SPACER: attempt to generalize lemmas with array equalities | true
-spacer.use_bg_invs | bool  |  Enable external background invariants | false
-spacer.use_derivations | bool  |  SPACER: using derivation mechanism to cache intermediate results for non-linear rules | true
-spacer.use_euf_gen | bool  |  Generalize lemmas and pobs using implied equalities | false
-spacer.use_inc_clause | bool  |  Use incremental clause to represent trans | true
-spacer.use_inductive_generalizer | bool  |  generalize lemmas using induction strengthening | true
-spacer.use_lemma_as_cti | bool  |  SPACER: use a lemma instead of a CTI in flexible_trace | false
-spacer.use_lim_num_gen | bool  |  Enable limit numbers generalizer to get smaller numbers | false
-spacer.validate_lemmas | bool  |  Validate each lemma after generalization | false
-spacer.weak_abs | bool  |  Weak abstraction | true
-tab.selection | symbol  |  selection method for tabular strategy: weight (default), first, var-use | weight
-validate | bool  |  validate result (by proof checking or model checking) | false
-xform.array_blast | bool  |  try to eliminate local array terms using Ackermannization -- some array terms may remain | false
-xform.array_blast_full | bool  |  eliminate all local array variables by QE | false
-xform.bit_blast | bool  |  bit-blast bit-vectors | false
-xform.coalesce_rules | bool  |  coalesce rules | false
-xform.coi | bool  |  use cone of influence simplification | true
-xform.compress_unbound | bool  |  compress tails with unbound variables | true
-xform.elim_term_ite | bool  |  Eliminate term-ite expressions | false
-xform.elim_term_ite.inflation | unsigned int  |  Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative) | 3
-xform.fix_unbound_vars | bool  |  fix unbound variables in tail | false
-xform.inline_eager | bool  |  try eager inlining of rules | true
-xform.inline_linear | bool  |  try linear inlining method | true
-xform.inline_linear_branch | bool  |  try linear inlining method with potential expansion | false
-xform.instantiate_arrays | bool  |  Transforms P(a) into P(i, a[i] a) | false
-xform.instantiate_arrays.enforce | bool  |  Transforms P(a) into P(i, a[i]), discards a from predicate | false
-xform.instantiate_arrays.nb_quantifier | unsigned int  |  Gives the number of quantifiers per array | 1
-xform.instantiate_arrays.slice_technique | symbol  |  <no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true | no-slicing
-xform.instantiate_quantifiers | bool  |  instantiate quantified Horn clauses using E-matching heuristic | false
-xform.magic | bool  |  perform symbolic magic set transformation | false
-xform.quantify_arrays | bool  |  create quantified Horn clauses from clauses with arrays | false
-xform.scale | bool  |  add scaling variable to linear real arithmetic clauses | false
-xform.slice | bool  |  simplify clause set using slicing | true
-xform.subsumption_checker | bool  |  Enable subsumption checker (no support for model conversion) | true
-xform.tail_simplifier_pve | bool  |  propagate_variable_equivalences | true
-xform.transform_arrays | bool  |  Rewrites arrays equalities and applies select over store | false
-xform.unfold_rules | unsigned int  |  unfold rules statically using iterative squaring | 0
-
-## Module smt
-
-Description: smt solver based on lazy smt
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-arith.auto_config_simplex | bool  |  force simplex solver in auto_config | false
-arith.bprop_on_pivoted_rows | bool  |  propagate bounds on rows changed by the pivot operation | true
-arith.branch_cut_ratio | unsigned int  |  branch/cut ratio for linear integer arithmetic | 2
-arith.dump_lemmas | bool  |  dump arithmetic theory lemmas to files | false
-arith.eager_eq_axioms | bool  |  eager equality axioms | true
-arith.enable_hnf | bool  |  enable hnf (Hermite Normal Form) cuts | true
-arith.greatest_error_pivot | bool  |  Pivoting strategy | false
-arith.ignore_int | bool  |  treat integer variables as real | false
-arith.int_eq_branch | bool  |  branching using derived integer equations | false
-arith.min | bool  |  minimize cost | false
-arith.nl | bool  |  (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2 | true
-arith.nl.branching | bool  |  branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2 | true
-arith.nl.delay | unsigned int  |  number of calls to final check before invoking bounded nlsat check | 500
-arith.nl.expp | bool  |  expensive patching | false
-arith.nl.gr_q | unsigned int  |  grobner's quota | 10
-arith.nl.grobner | bool  |  run grobner's basis heuristic | true
-arith.nl.grobner_cnfl_to_report | unsigned int  |  grobner's maximum number of conflicts to report | 1
-arith.nl.grobner_eqs_growth | unsigned int  |  grobner's number of equalities growth  | 10
-arith.nl.grobner_expr_degree_growth | unsigned int  |  grobner's maximum expr degree growth | 2
-arith.nl.grobner_expr_size_growth | unsigned int  |  grobner's maximum expr size growth | 2
-arith.nl.grobner_frequency | unsigned int  |  grobner's call frequency | 4
-arith.nl.grobner_max_simplified | unsigned int  |  grobner's maximum number of simplifications | 10000
-arith.nl.grobner_subs_fixed | unsigned int  |  0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 1
-arith.nl.horner | bool  |  run horner's heuristic | true
-arith.nl.horner_frequency | unsigned int  |  horner's call frequency | 4
-arith.nl.horner_row_length_limit | unsigned int  |  row is disregarded by the heuristic if its length is longer than the value | 10
-arith.nl.horner_subs_fixed | unsigned int  |  0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 2
-arith.nl.nra | bool  |  call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6 | true
-arith.nl.order | bool  |  run order lemmas | true
-arith.nl.rounds | unsigned int  |  threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2 | 1024
-arith.nl.tangents | bool  |  run tangent lemmas | true
-arith.print_ext_var_names | bool  |  print external variable names | false
-arith.print_stats | bool  |  print statistic | false
-arith.propagate_eqs | bool  |  propagate (cheap) equalities | true
-arith.propagation_mode | unsigned int  |  0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds | 1
-arith.random_initial_value | bool  |  use random initial values in the simplex-based procedure for linear arithmetic | false
-arith.rep_freq | unsigned int  |  the report frequency, in how many iterations print the cost and other info | 0
-arith.simplex_strategy | unsigned int  |  simplex strategy for the solver | 0
-arith.solver | unsigned int  |  arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 6
-array.extensional | bool  |  extensional array theory | true
-array.weak | bool  |  weak array theory | false
-auto_config | bool  |  automatically configure solver | true
-bv.delay | bool  |  delay internalize expensive bit-vector operations | true
-bv.enable_int2bv | bool  |  enable support for int2bv and bv2int operators | true
-bv.eq_axioms | bool  |  enable redundant equality axioms for bit-vectors | true
-bv.reflect | bool  |  create enode for every bit-vector term | true
-bv.watch_diseq | bool  |  use watch lists instead of eager axioms for bit-vectors | false
-candidate_models | bool  |  create candidate models even when quantifier or theory reasoning is incomplete | false
-case_split | unsigned int  |  0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity | 1
-clause_proof | bool  |  record a clausal proof | false
-core.extend_nonlocal_patterns | bool  |  extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body | false
-core.extend_patterns | bool  |  extend unsat core with literals that trigger (potential) quantifier instances | false
-core.extend_patterns.max_distance | unsigned int  |  limits the distance of a pattern-extended unsat core | 4294967295
-core.minimize | bool  |  minimize unsat core produced by SMT context | false
-core.validate | bool  |  [internal] validate unsat core produced by SMT context. This option is intended for debugging | false
-cube_depth | unsigned int  |  cube depth. | 1
-dack | unsigned int  |  0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1
-dack.eq | bool  |  enable dynamic ackermannization for transtivity of equalities | false
-dack.factor | double  |  number of instance per conflict | 0.1
-dack.gc | unsigned int  |  Dynamic ackermannization garbage collection frequency (per conflict) | 2000
-dack.gc_inv_decay | double  |  Dynamic ackermannization garbage collection decay | 0.8
-dack.threshold | unsigned int  |   number of times the congruence rule must be used before Leibniz's axiom is expanded | 10
-delay_units | bool  |  if true then z3 will not restart when a unit clause is learned | false
-delay_units_threshold | unsigned int  |  maximum number of learned unit clauses before restarting, ignored if delay_units is false | 32
-dt_lazy_splits | unsigned int  |  How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy | 1
-ematching | bool  |  E-Matching based quantifier instantiation | true
-induction | bool  |  enable generation of induction lemmas | false
-lemma_gc_strategy | unsigned int  |  lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none | 0
-logic | symbol  |  logic used to setup the SMT solver | 
-macro_finder | bool  |  try to find universally quantified formulas that can be viewed as macros | false
-max_conflicts | unsigned int  |  maximum number of conflicts before giving up. | 4294967295
-mbqi | bool  |  model based quantifier instantiation (MBQI) | true
-mbqi.force_template | unsigned int  |  some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template | 10
-mbqi.id | string  |  Only use model-based instantiation for quantifiers with id's beginning with string | 
-mbqi.max_cexs | unsigned int  |  initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation | 1
-mbqi.max_cexs_incr | unsigned int  |  increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI | 0
-mbqi.max_iterations | unsigned int  |  maximum number of rounds of MBQI | 1000
-mbqi.trace | bool  |  generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied | false
-pb.conflict_frequency | unsigned int  |  conflict frequency for Pseudo-Boolean theory | 1000
-pb.learn_complements | bool  |  learn complement literals for Pseudo-Boolean theory | true
-phase_caching_off | unsigned int  |  number of conflicts while phase caching is off | 100
-phase_caching_on | unsigned int  |  number of conflicts while phase caching is on | 400
-phase_selection | unsigned int  |  phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory | 3
-pull_nested_quantifiers | bool  |  pull nested quantifiers | false
-q.lift_ite | unsigned int  |  0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers | 0
-q.lite | bool  |  Use cheap quantifier elimination during pre-processing | false
-qi.cost | string  |  expression specifying what is the cost of a given quantifier instantiation | (+ weight generation)
-qi.eager_threshold | double  |  threshold for eager quantifier instantiation | 10.0
-qi.lazy_threshold | double  |  threshold for lazy quantifier instantiation | 20.0
-qi.max_instances | unsigned int  |  maximum number of quantifier instantiations | 4294967295
-qi.max_multi_patterns | unsigned int  |  specify the number of extra multi patterns | 0
-qi.profile | bool  |  profile quantifier instantiation | false
-qi.profile_freq | unsigned int  |  how frequent results are reported by qi.profile | 4294967295
-qi.quick_checker | unsigned int  |  specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances | 0
-quasi_macros | bool  |  try to find universally quantified formulas that are quasi-macros | false
-random_seed | unsigned int  |  random seed for the smt solver | 0
-refine_inj_axioms | bool  |  refine injectivity axioms | true
-relevancy | unsigned int  |  relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant | 2
-restart.max | unsigned int  |  maximal number of restarts. | 4294967295
-restart_factor | double  |  when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold | 1.1
-restart_strategy | unsigned int  |  0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic | 1
-restricted_quasi_macros | bool  |  try to find universally quantified formulas that are restricted quasi-macros | false
-seq.max_unfolding | unsigned int  |  maximal unfolding depth for checking string equations and regular expressions | 1000000000
-seq.split_w_len | bool  |  enable splitting guided by length constraints | true
-seq.validate | bool  |  enable self-validation of theory axioms created by seq theory | false
-str.aggressive_length_testing | bool  |  prioritize testing concrete length values over generating more options | false
-str.aggressive_unroll_testing | bool  |  prioritize testing concrete regex unroll counts over generating more options | true
-str.aggressive_value_testing | bool  |  prioritize testing concrete string constant values over generating more options | false
-str.fast_length_tester_cache | bool  |  cache length tester constants instead of regenerating them | false
-str.fast_value_tester_cache | bool  |  cache value tester constants instead of regenerating them | true
-str.fixed_length_naive_cex | bool  |  construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only) | true
-str.fixed_length_refinement | bool  |  use abstraction refinement in fixed-length equation solver (Z3str3 only) | false
-str.overlap_priority | double  |  theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true | -0.1
-str.regex_automata_difficulty_threshold | unsigned int  |  difficulty threshold for regex automata heuristics | 1000
-str.regex_automata_failed_automaton_threshold | unsigned int  |  number of failed automaton construction attempts after which a full automaton is automatically built | 10
-str.regex_automata_failed_intersection_threshold | unsigned int  |  number of failed automaton intersection attempts after which intersection is always computed | 10
-str.regex_automata_intersection_difficulty_threshold | unsigned int  |  difficulty threshold for regex intersection heuristics | 1000
-str.regex_automata_length_attempt_threshold | unsigned int  |  number of length/path constraint attempts before checking unsatisfiability of regex terms | 10
-str.string_constant_cache | bool  |  cache all generated string constants generated from anywhere in theory_str | true
-str.strong_arrangements | bool  |  assert equivalences instead of implications when generating string arrangement axioms | true
-string_solver | symbol  |  solver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver) | seq
-theory_aware_branching | bool  |  Allow the context to use extra information from theory solvers regarding literal branching prioritization. | false
-theory_case_split | bool  |  Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead. | false
-threads | unsigned int  |  maximal number of parallel threads. | 1
-threads.cube_frequency | unsigned int  |  frequency for using cubing | 2
-threads.max_conflicts | unsigned int  |  maximal number of conflicts between rounds of cubing for parallel SMT | 400
-
-## Module sls
-
-Description: Experimental Stochastic Local Search Solver (for QFBV only).
- Parameter | Type | Description | Default
- ----------|------|-------------|--------
-early_prune | bool  |  use early pruning for score prediction | true
-max_memory | unsigned int  |  maximum amount of memory in megabytes | 4294967295
-max_restarts | unsigned int  |  maximum number of restarts | 4294967295
-paws_init | unsigned int  |  initial/minimum assertion weights | 40
-paws_sp | unsigned int  |  smooth assertion weights with probability paws_sp / 1024 | 52
-random_offset | bool  |  use random offset for candidate evaluation | true
-random_seed | unsigned int  |  random seed | 0
-rescore | bool  |  rescore/normalize top-level score every base restart interval | true
-restart_base | unsigned int  |  base restart interval given by moves per run | 100
-restart_init | bool  |  initialize to 0 or random value (= 1) after restart | false
-scale_unsat | double  |  scale score of unsat expressions by this factor | 0.5
-track_unsat | bool  |  keep a list of unsat assertions as done in SAT - currently disabled internally | false
-vns_mc | unsigned int  |  in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit | 0
-vns_repick | bool  |  in local minima, try picking a different assertion (only for walksat) | false
-walksat | bool  |  use walksat assertion selection (instead of gsat) | true
-walksat_repick | bool  |  repick assertion if randomizing in local minima | true
-walksat_ucb | bool  |  use bandit heuristic for walksat assertion selection (instead of random) | true
-walksat_ucb_constant | double  |  the ucb constant c in the term score + c * f(touched) | 20.0
-walksat_ucb_forget | double  |  scale touched by this factor every base restart interval | 1.0
-walksat_ucb_init | bool  |  initialize total ucb touched to formula size | false
-walksat_ucb_noise | double  |  add noise 0 <= 256 * ucb_noise to ucb score for assertion selection | 0.0002
-wp | unsigned int  |  random walk with probability wp / 1024 | 100

README.md

@@ -105,6 +105,19 @@ Z3 has a build system using CMake. Read the [README-CMake.md](README-CMake.md)
 file for details. It is recommended for most build tasks, 
 except for building OCaml bindings.
 
+## Building Z3 using vcpkg
+
+vcpkg is a full platform package manager, you can easily install libzmq with vcpkg.
+ 
+Execute:
+
+```bash
+git clone https://github.com/microsoft/vcpkg.git
+./bootstrap-vcpkg.bat # For powershell
+./bootstrap-vcpkg.sh # For bash
+./vcpkg install z3
+```
+
 ## Dependencies
 Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.
 It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained 

RELEASE_NOTES.md

@@ -10,10 +10,137 @@ Version 4.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
-Version 4.11.1
+Version 4.12.0
+==============
+- add clause logging API.
+  - The purpose of logging API and self-checking is to enable an array of use cases.
+    - proof mining (what instantiations did Z3 use)? 
+      - A refresh of the AxiomProfiler could use the logging API. 
+        The (brittle) trace feature should be deprecated.
+    - debugging
+      - a built-in self certifier implements a custom proof checker for 
+        the format used by the new solver (sat.euf=true).
+    - other potential options:
+      - integration into certified tool chains      
+      - interpolation 
+  - Z3_register_on_clause (also exposed over C++, Python and .Net)
+  - it applies to z3's main CDCL(T) core and a new CDCL(T) core (sat.euf=true).
+  - The added API function allows to register a callback for when clauses 
+    are inferred. More precisely, when clauses are assumed (as part of input), 
+    deleted, or deduced.
+    Clauses that are deduced by the CDCL SAT engine using standard 
+    inferences are marked as 'rup'.
+    Clauses that are deduced by theories are marked by default 
+    by 'smt', and when more detailed information
+    is available with proof hints or proof objects. 
+    Instantations are considered useful to track so they
+    are logged using terms of the form 
+
+         (inst (not (forall (x) body)) body[t/x] (bind t)), where
+
+    'inst' is a name of a function that produces a proof term representing 
+    the instantiation.
+- add options for proof logging, trimming, and checking for the new core.
+  - sat.smt.proof (symbol) add SMT proof to file (default: )
+  - sat.smt.proof.check (bool) check SMT proof while it is created (default: false)
+    - it applies a custom self-validator. The self-validator comprises of 
+      several small checkers and represent a best-effort validation mechanism. 
+      If there are no custom validators associated with inferences, or the custom 
+      validators fail to certify inferences, the self-validator falls back to 
+      invoking z3 (SMT) solving on the lemma.
+      - euf - propagations and conflicts from congruence closure 
+              (theory of equality and uninterpreted functions) are checked
+              based on a proof format that tracks uses of congruence closure and 
+              equalities. It only performs union find operations.
+      - tseitin - clausification steps are checked for Boolean operators.
+      - farkas, bound, implies_eq - arithmetic inferences that can be justified using 
+              a combination of Farkas lemma and cuts are checked.
+              Note: the arithmetic solver may produce proof hints that the proof 
+              checker cannot check. It is mainly a limitation
+              of the arithmetic solver not pulling relevant information. 
+              Ensuring a tight coupling with proof hints and the validator
+              capabilites is open ended future work and good material for theses. 
+      - bit-vector inferences - are treated as trusted 
+        (there is no validation, it always blindly succeeds)
+      - arrays, datatypes - there is no custom validation for 
+        other theories at present. Lemmas are validated using SMT.
+  - sat.smt.proof.check_rup (bool) apply forward RUP proof checking (default: true)
+    - this option can incur significant runtime overhead. 
+      Effective proof checking relies on first trimming proofs into a 
+      format where dependencies are tracked and then checking relevant inferences. 
+      Turn this option off if you just want to check theory inferences.                         
+- add options to validate proofs offline. It applies to proofs 
+  saved when sat.smt.proof is set to a valid file name.
+  - solver.proof.check (bool) check proof logs (default: true)
+    - the option sat.smt.proof_check_rup can be used to control what is checked
+  - solver.proof.save (bool) save proof log into a proof object 
+      that can be extracted using (get-proof) (default: false)
+    - experimental: saves a proof log into a term
+  - solver.proof.trim (bool) trim the offline proof and print the trimmed proof to the console
+    - experimental: performs DRUP trimming to reduce the set of hypotheses 
+      and inferences relevant to derive the empty clause.
+- JS support for Arrays, thanks to Walden Yan
+- More portable memory allocation, thanks to Nuno Lopes 
+  (avoid custom handling to calculate memory usage)
+
+- clause logging and proofs: many open-ended directions.
+  Many directions and functionality features remain in an open-ended state, 
+  subject to fixes, improvements, and contributions.
+  We list a few of them here:
+  - comprehensive efficient self-validators for arithmetic, and other theories
+  - an efficient proof checker when several theory solvers cooperate in a propagation or 
+    conflict. The theory combination case is currently delegated to the smt solver. 
+    The proper setup for integrating theory lemmas is in principle not complicated, 
+    but the implementation requires some changes.
+  - external efficient proof validators (based on certified tool chains) 
+    can be integrated over the API.
+  - dampening repeated clauses: A side-effect of conflict resolution is to 
+    log theory lemmas. It often happens that the theory lemma becomes
+    the conflict clause, that is then logged as rup. Thus, two clauses are 
+    logged.
+  - support for online trim so that proofs generated using clause logging can be used for SPACER
+    - SPACER also would benefit from more robust proof hints for arithmetic 
+      lemmas (bounds and implied equalities are sometimes not logged correctly)
+  - integration into axiom profiling through online and/or offline interfaces.
+    - an online interface attaches a callback with a running solver. This is available.
+    - an offline interface saves a clause proof to a file (currently just 
+      supported for sat.euf) and then reads the file in a separate process
+      The separate process attaches a callback on inferred clauses. 
+      This is currently not available but a relatively small feature.
+  - more detailed proof hints for the legacy solver clause logger. 
+    Other than quantifier instantiations, no detailed information is retained for 
+    theory clauses. 
+  - integration of pre-processing proofs with logging proofs. There is 
+    currently no supported bridge to create a end-to-end proof objects.
+
+
+Version 4.11.2
 ==============
 - add error handling to fromString method in JavaScript
-- fix regression in default parameters for CDCL (Nuno Lopes)
+- fix regression in default parameters for CDCL, thanks to Nuno Lopes
+- fix model evaluation bugs for as-array nested under functions (data-type constructors)
+- add rewrite simplifications for datatypes with a single constructor
+- add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind.
+  The commit logs related to Global Guidance contain detailed information.
+- change proof logging format for the new core to use SMTLIB commands.
+  The format was so far an extension of DRAT used by SAT solvers, but not well compatible
+  with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with
+  three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses.
+  They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas".
+  "rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when
+  the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the
+  format. Quantifier instantiations are also tracked as proof hints.
+  Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in,
+  self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally
+  insufficient as generated clauses are in principle required to only be satisfiability preserving.
+  Proof checking and tranformation operations is overall open ended.
+  The log for the first commit introducing this change contains further information on the format.
+- fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer).
+- handle _toExpr for quantified formulas in JS bindings
+
+Version 4.11.1
+==============
+- skipped
 
 Version 4.11.0
 ==============

azure-pipelines.yml

@@ -202,7 +202,7 @@ jobs:
         setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
         setupCmd3: 'set /P JlCxxDir=<tmp.env'
         bindings:  '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx $(cmakeJava) $(cmakeNet) $(cmakePy) -DCMAKE_BUILD_TYPE=RelWithDebInfo'
-        runTests:  'True'
+        runTests:  'False'
       arm64:
         arch: 'amd64_arm64'
         setupCmd1: ''

contrib/qprofdiff/main.cpp

@@ -65,7 +65,7 @@ int parse(string const & filename, map<string, map_entry> & data) {
                 inx != string::npos;
                 inx = line.find(" : ", from)) {
                 tokens[ti] = trim(line.substr(from, inx-from));
-                from = inx+1;
+                from = inx+3; //3 is the length of " : "
                 ti++;
             }
             if (from != line.length() && ti < 4)

doc/mk_tactic_doc.py

@@ -0,0 +1,91 @@
+# Copyright (c) Microsoft Corporation 2015
+"""
+Tactic documentation generator script
+"""
+
+import os
+import re
+import sys
+import subprocess
+
+BUILD_DIR='../build'
+SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
+OUTPUT_DIRECTORY = os.path.join(os.getcwd(), 'api')
+
+def doc_path(path):
+    return os.path.join(SCRIPT_DIR, path)
+
+is_doc = re.compile("Tactic Documentation")
+is_doc_end = re.compile("\-\-\*\/")
+is_tac_name = re.compile("## Tactic (.*)")
+
+def is_ws(s):
+    return all([0 for ch in s if ch != ' ' and ch != '\n'])
+
+def extract_params(ous, tac):
+    z3_exe = BUILD_DIR + "/z3"
+    out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
+    if not out:
+        return
+    out = out.decode(sys.stdout.encoding)
+    if is_ws(out):
+        return
+    ous.write("### Parameters\n\n")
+    for line in out:
+        ous.write(line.replace("\r",""))
+    ous.write("\n")
+    
+def generate_tactic_doc(ous, f, ins):
+    tac_name = None
+    for line in ins:
+        m = is_tac_name.search(line)
+        if m:
+            tac_name = m.group(1)
+        if is_doc_end.search(line):
+            if tac_name:
+                extract_params(ous, tac_name)
+            break
+        ous.write(line)
+
+def extract_tactic_doc(ous, f):
+    with open(f) as ins:
+        for line in ins:
+            if is_doc.search(line):
+                generate_tactic_doc(ous, f, ins)
+
+def find_tactic_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_tac_name.search(line)
+            if m:
+                return m.group(1)
+    print(f"no tactic in {path}")
+    return ""
+
+def presort_files():
+    tac_files = []
+    for root, dirs, files in os.walk(doc_path("../src")):
+        for f in files:
+            if f.endswith("tactic.h"):
+                tac_files += [(f, os.path.join(root, f))]
+    tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1]))
+    return tac_files
+    
+def help(ous):
+    presort_files()
+    ous.write("---\n")
+    ous.write("title: Tactics Summary\n")
+    ous.write("sidebar_position: 5\n")
+    ous.write("---\n")
+    tac_files = presort_files()
+    for file, path in tac_files:
+        extract_tactic_doc(ous, path)
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        os.makedirs(d)
+
+mk_dir(os.path.join(OUTPUT_DIRECTORY, 'md'))
+
+with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous:
+    help(ous)

examples/c/test_capi.c

@@ -561,6 +561,7 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v)
     }
     case Z3_QUANTIFIER_AST: {
         fprintf(out, "quantifier");
+        break;
     }
     default:
         fprintf(out, "#unknown");
@@ -2946,6 +2947,28 @@ void mk_model_example() {
     Z3_del_context(ctx);
 }
 
+void divides_example()
+{
+    Z3_context ctx;
+    Z3_solver s;
+    Z3_ast x, number;
+    Z3_ast c;
+
+    ctx    = mk_context();
+    s      = mk_solver(ctx);
+
+    x      = mk_int_var(ctx, "x");
+    number = mk_int(ctx, 2);
+
+    c      = Z3_mk_divides(ctx, number, x);
+    Z3_solver_assert(ctx, s, c);
+
+    check2(ctx, s, Z3_L_TRUE);
+
+    del_solver(ctx, s);
+    Z3_del_context(ctx);
+}
+
 /**@}*/
 /**@}*/
 
@@ -2955,6 +2978,7 @@ int main() {
 #ifdef LOG_Z3_CALLS
     Z3_open_log("z3.log");
 #endif
+    divides_example();
     display_version();
     simple_example();
     demorgan();

examples/python/prooflogs.py

@@ -0,0 +1,93 @@
+# This script illustrates uses of proof logs over the Python interface.
+
+from z3 import *
+
+example1 = """
+(declare-sort T) 
+
+(declare-fun subtype (T T) Bool)
+
+;; subtype is reflexive
+(assert (forall ((x T)) (subtype x x)))
+
+;; subtype is antisymmetric
+(assert (forall ((x T) (y T)) (=> (and (subtype x y)
+                                       (subtype y x))
+                                       (= x y))))
+;; subtype is transitive
+(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x y)
+                                             (subtype y z))
+                                             (subtype x z))))
+;; subtype has the tree-property
+(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x z)
+                                             (subtype y z))
+                                        (or (subtype x y)
+                                            (subtype y x)))))
+
+;; now we define a simple example using the axiomatization above.
+(declare-const obj-type T)
+(declare-const int-type T)
+(declare-const real-type T)
+(declare-const complex-type T)
+(declare-const string-type T)
+
+;; we have an additional axiom: every type is a subtype of obj-type
+(assert (forall ((x T)) (subtype x obj-type)))
+
+(assert (subtype int-type real-type))
+(assert (subtype real-type complex-type))
+(assert (not (subtype string-type real-type)))
+(declare-const root-type T)
+(assert (subtype obj-type root-type))
+"""
+
+def monitor_plain():
+    print("Monitor all inferred clauses")
+    s = Solver()
+    s.from_string(example1)
+    onc = OnClause(s, lambda pr, clause : print(pr, clause))
+    print(s.check())
+
+def log_instance(pr, clause):
+    if pr.decl().name() == "inst":
+        q = pr.arg(0).arg(0) # first argument is Not(q)
+        for ch in pr.children():
+            if ch.decl().name() == "bind":
+                print("Binding")
+                print(q)
+                print(ch.children())
+                break
+
+def monitor_instances():
+    print("Monitor just quantifier bindings")
+    s = Solver()
+    s.from_string(example1)
+    onc = OnClause(s, log_instance)
+    print(s.check())
+    
+def monitor_with_proofs():
+    print("Monitor clauses annotated with detailed justifications")
+    set_param(proof=True)
+    s = Solver()
+    s.from_string(example1)
+    onc = OnClause(s, lambda pr, clause : print(pr, clause))
+    print(s.check())
+
+def monitor_new_core():
+    print("Monitor proof objects from the new core")
+    set_param("sat.euf", True)
+    set_param("tactic.default_tactic", "sat")
+    s = Solver()
+    s.from_string(example1)
+    onc = OnClause(s, lambda pr, clause : print(pr, clause))
+    print(s.check())
+
+
+if __name__ == "__main__":
+    monitor_plain()
+    monitor_instances()
+    monitor_new_core()
+
+
+# Monitoring with proofs cannot be done in the same session
+#   monitor_with_proofs()

examples/python/proofreplay.py

@@ -0,0 +1,113 @@
+# This script illustrates uses of proof replay and proof logs over the Python interface.
+
+from z3 import *
+
+example1 = """
+(declare-sort T) 
+
+(declare-fun subtype (T T) Bool)
+
+;; subtype is reflexive
+(assert (forall ((x T)) (subtype x x)))
+
+;; subtype is antisymmetric
+(assert (forall ((x T) (y T)) (=> (and (subtype x y)
+                                       (subtype y x))
+                                       (= x y))))
+;; subtype is transitive
+(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x y)
+                                             (subtype y z))
+                                             (subtype x z))))
+;; subtype has the tree-property
+(assert (forall ((x T) (y T) (z T)) (=> (and (subtype x z)
+                                             (subtype y z))
+                                        (or (subtype x y)
+                                            (subtype y x)))))
+
+;; now we define a simple example using the axiomatization above.
+(declare-const obj-type T)
+(declare-const int-type T)
+(declare-const real-type T)
+(declare-const complex-type T)
+(declare-const string-type T)
+
+;; we have an additional axiom: every type is a subtype of obj-type
+(assert (forall ((x T)) (subtype x obj-type)))
+
+(assert (subtype int-type real-type))
+(assert (subtype real-type complex-type))
+(assert (not (subtype string-type real-type)))
+(declare-const root-type T)
+(assert (subtype obj-type root-type))
+"""
+
+if __name__ == "__main__":
+    print("Solve and log inferences")
+    print("--------------------------------------------------------")
+
+    # inference logging, replay, and checking is supported for
+    # the core enabled by setting sat.euf = true.
+    # setting the default tactic to 'sat' bypasses other tactics that could
+    # end up using different solvers.     
+    set_param("sat.euf", True)
+    set_param("tactic.default_tactic", "sat")
+
+    # Set a log file to trace inferences
+    set_param("sat.smt.proof", "proof_log.smt2")
+    s = Solver()
+    s.from_string(example1)
+    print(s.check())
+    print(s.statistics())
+    print("Parse the logged inferences and replay them")
+    print("--------------------------------------------------------")
+
+    # Reset the log file to an invalid (empty) file name.
+    set_param("sat.smt.proof", "")
+
+    # Turn off proof checking. It is on by default when parsing proof logs.
+    set_param("solver.proof.check", False)        
+    s = Solver()
+    onc = OnClause(s, lambda pr, clause : print(pr, clause))
+    s.from_file("proof_log.smt2")
+
+    
+    print("Parse the logged inferences and check them")
+    print("--------------------------------------------------------")
+    s = Solver()
+
+    # Now turn on proof checking. It invokes the self-validator.
+    # The self-validator produces log lines of the form:
+    # (proofs +tseitin 60 +alldiff 8 +euf 3 +rup 5 +inst 6 -quant 3 -inst 2)
+    # (verified-smt
+    #  (inst (forall (vars (x T) (y T) (z T)) (or (subtype (:var 2) (:var 1)) ...
+    # The 'proofs' line summarizes inferences that were self-validated.
+    # The pair +tseitin 60 indicates that 60 inferences were validated as Tseitin
+    # encodings.
+    # The pair -inst 2 indicates that two quantifier instantiations were not self-validated
+    # They were instead validated using a call to SMT solving. A log for an smt invocation
+    # is exemplified in the next line.
+    # Note that the pair +inst 6 indicates that 6 quantifier instantations were validated
+    # using a syntactic (cheap) check. Some quantifier instantiations based on quantifier elimination
+    # are not simple substitutions and therefore a simple syntactic check does not suffice.
+    set_param("solver.proof.check", True)
+    s.from_file("proof_log.smt2")
+
+    print("Verify and self-validate on the fly")
+    print("--------------------------------------------------------")
+    set_param("sat.smt.proof.check", True)
+    s = Solver()
+    s.from_string(example1)
+    print(s.check())
+    print(s.statistics())
+
+    print("Verify and self-validate on the fly, but don't check rup")
+    print("--------------------------------------------------------")
+    set_param("sat.smt.proof.check", True)
+    set_param("sat.smt.proof.check_rup", False)
+    s = Solver()
+    s.from_string(example1)
+    print(s.check())
+    print(s.statistics())
+
+    
+

examples/tptp/tptp5.cpp

@@ -2305,12 +2305,26 @@ static void display_smt2(std::ostream& out) {
         return;
     }
 
+    z3::expr_vector asms(ctx);
     size_t num_assumptions = fmls.m_formulas.size();
+    for (size_t i = 0; i < num_assumptions; ++i) 
+        asms.push_back(fmls.m_formulas[i]);
 
-    Z3_ast* assumptions = new Z3_ast[num_assumptions];
-    for (size_t i = 0; i < num_assumptions; ++i) {
-        assumptions[i] = fmls.m_formulas[i];
+    for (size_t i = 0; i < asms.size(); ++i) {
+        z3::expr fml = asms[i];
+        if (fml.is_and()) {
+            z3::expr arg0 = fml.arg(0);
+            asms.set(i, arg0);
+            for (unsigned j = 1; j < fml.num_args(); ++j)
+                asms.push_back(fml.arg(j));
+            --i;
+        }
     }
+    
+    Z3_ast* assumptions = new Z3_ast[asms.size()];
+    for (size_t i = 0; i < asms.size(); ++i) 
+        assumptions[i] = asms[i];        
+    Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB_FULL);
     Z3_string s = 
         Z3_benchmark_to_smtlib_string(
             ctx, 
@@ -2318,7 +2332,7 @@ static void display_smt2(std::ostream& out) {
             0,         // no logic is set
             "unknown", // no status annotation
             "",        // attributes
-            static_cast<unsigned>(num_assumptions), 
+            static_cast<unsigned>(asms.size()), 
             assumptions, 
             ctx.bool_val(true));
 

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 11, 1, 0) # express a default build version or pick up ci build version
+    set_version(4, 12, 0, 0) # express a default build version or pick up ci build version
     
 # Z3 Project definition
 def init_project_def():
@@ -20,24 +20,27 @@ def init_project_def():
     add_lib('simplex', ['util'], 'math/simplex')
     add_lib('hilbert', ['util'], 'math/hilbert')
     add_lib('automata', ['util'], 'math/automata')
+    add_lib('params', ['util'])
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
-    add_lib('euf', ['ast', 'util'], 'ast/euf')
-    add_lib('params', ['util'])
-    add_lib('smt_params', ['params'], 'smt/params')
+    add_lib('smt_params', ['ast', 'params'], 'smt/params')
+    add_lib('parser_util', ['ast'], 'parsers/util')
+    add_lib('euf', ['ast'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
     add_lib('sat', ['params', 'util', 'dd', 'grobner'])    
     add_lib('nlsat', ['polynomial', 'sat'])
     add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
     add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter')
-    add_lib('macros', ['rewriter'], 'ast/macros')
+    add_lib('bit_blaster',  ['rewriter'], 'ast/rewriter/bit_blaster')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
-    add_lib('model', ['rewriter', 'macros'])
-    add_lib('tactic', ['ast', 'model'])
-    add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
-    add_lib('parser_util', ['ast'], 'parsers/util')
-    add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
+    add_lib('substitution', ['rewriter'], 'ast/substitution')
+    add_lib('proofs', ['rewriter'], 'ast/proofs')
+    add_lib('macros', ['rewriter'], 'ast/macros')
+    add_lib('model',  ['macros'])
+    add_lib('converters', ['model'], 'ast/converters')
+    add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
+    add_lib('tactic', ['simplifiers'])
     add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
@@ -45,20 +48,19 @@ def init_project_def():
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
-    add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
     add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions')
-    add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
-    add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
-    add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
 
     add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions',
                     'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
+    add_lib('sat_smt', ['sat', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
+    add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
+    add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')    
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
@@ -82,9 +84,9 @@ def init_project_def():
     add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
-    add_lib('api', ['portfolio',  'realclosure', 'opt'],
-            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds')
+    add_lib('api', ['portfolio',  'realclosure', 'opt', 'extra_cmds'],
+            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',

scripts/nightly.yaml

@@ -1,7 +1,7 @@
 variables:
   Major: '4'
-  Minor: '11'
-  Patch: '1'
+  Minor: '12'
+  Patch: '0'
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
 

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.11.1'
+  ReleaseVersion: '4.12.0'
 
 stages:
 

scripts/update_api.py

@@ -339,6 +339,10 @@ def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handl
   _elems.Check(ctx)
   return ceh
 
+def Z3_solver_register_on_clause(ctx, s, user_ctx, on_clause_eh, _elems = Elementaries(_lib.Z3_solver_register_on_clause)):
+    _elems.f(ctx, s, user_ctx, on_clause_eh)
+    _elems.Check(ctx)
+    
 def Z3_solver_propagate_init(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh, _elems = Elementaries(_lib.Z3_solver_propagate_init)):
     _elems.f(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh)
     _elems.Check(ctx)
@@ -776,6 +780,13 @@ def mk_java(java_src, java_dir, package_name):
                     java_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
                     java_wrapper.write('     jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
                     java_wrapper.write('  }\n')
+                elif param_type(param) == STRING:
+                    java_wrapper.write('  {\n')
+                    java_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
+                    java_wrapper.write('     jfieldID fid = jenv->GetFieldID(mc, "value", "Ljava/lang/String;");')
+                    java_wrapper.write('     jstring fval = jenv->NewStringUTF(_a%s);\n' % i)
+                    java_wrapper.write('     jenv->SetObjectField(a%s, fid, fval);\n' % i)
+                    java_wrapper.write('  }\n')
                 else:
                     java_wrapper.write('  {\n')
                     java_wrapper.write('     jclass mc    = jenv->GetObjectClass(a%s);\n' % i)
@@ -1308,7 +1319,8 @@ z3_ml_callbacks = frozenset([
     'Z3_solver_propagate_eq',
     'Z3_solver_propagate_diseq',
     'Z3_solver_propagate_created',
-    'Z3_solver_propagate_decide'
+    'Z3_solver_propagate_decide',
+    'Z3_solver_register_on_clause'
     ])
 
 def mk_ml(ml_src_dir, ml_output_dir):
@@ -1837,6 +1849,7 @@ _error_handler_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
 _lib.Z3_set_error_handler.restype  = None
 _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
+Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 Z3_push_eh  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
 Z3_pop_eh   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
 Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
@@ -1848,6 +1861,7 @@ Z3_eq_eh    = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_
 Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 
+_lib.Z3_solver_register_on_clause.restype = None
 _lib.Z3_solver_propagate_init.restype = None
 _lib.Z3_solver_propagate_final.restype = None
 _lib.Z3_solver_propagate_fixed.restype = None

src/CMakeLists.txt

@@ -46,12 +46,15 @@ add_subdirectory(math/subpaving)
 add_subdirectory(ast)
 add_subdirectory(params)
 add_subdirectory(ast/rewriter)
+add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(ast/normal_forms)
 add_subdirectory(ast/macros)
 add_subdirectory(model)
-add_subdirectory(tactic)
-add_subdirectory(ast/substitution)
 add_subdirectory(ast/euf)
+add_subdirectory(ast/converters)
+add_subdirectory(ast/substitution)
+add_subdirectory(ast/simplifiers)
+add_subdirectory(tactic)
 add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)
@@ -69,7 +72,6 @@ add_subdirectory(qe/mbp)
 add_subdirectory(qe/lite)
 add_subdirectory(solver/assertions)
 add_subdirectory(ast/pattern)
-add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(math/lp)
 add_subdirectory(sat/smt)
 add_subdirectory(sat/tactic)
@@ -115,6 +117,27 @@ if (Z3_BUILD_LIBZ3_SHARED)
 else()
   set(lib_type "STATIC")
 endif()
+# Enable static msvc runtime.
+if (MSVC AND Z3_BUILD_LIBZ3_MSVC_STATIC)
+    set(CompilerFlags
+        CMAKE_CXX_FLAGS
+        CMAKE_CXX_FLAGS_DEBUG
+        CMAKE_CXX_FLAGS_RELEASE
+        CMAKE_CXX_FLAGS_MINSIZEREL
+        CMAKE_CXX_FLAGS_RELWITHDEBINFO
+        CMAKE_C_FLAGS
+        CMAKE_C_FLAGS_DEBUG
+        CMAKE_C_FLAGS_RELEASE
+        CMAKE_C_FLAGS_MINSIZEREL
+        CMAKE_C_FLAGS_RELWITHDEBINFO
+        )
+    foreach(CompilerFlag ${CompilerFlags})
+        string(REPLACE "/MD" "/MT" ${CompilerFlag} "${${CompilerFlag}}")
+        string(REPLACE "/MDd" "/MTd" ${CompilerFlag} "${${CompilerFlag}}")
+        set(${CompilerFlag} "${${CompilerFlag}}" CACHE STRING "msvc compiler flags" FORCE)
+        message("MSVC flags: ${CompilerFlag}:${${CompilerFlag}}")
+    endforeach()
+endif()
 add_library(libz3 ${lib_type} ${object_files})
 target_include_directories(libz3 INTERFACE
   $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/api>

src/ackermannization/ackermannize_bv_model_converter.h

@@ -16,7 +16,7 @@
  --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info);

src/ackermannization/ackermannize_bv_tactic.h

@@ -11,7 +11,37 @@ Author:
 
 Mikolas Janota
 
-Revision History:
+Tactic Documentation:
+
+## Tactic ackernannize_bv
+
+### Short Description
+
+A tactic for performing Ackermann reduction for bit-vector formulas
+
+### Long Description
+
+The Ackermann reduction replaces uninterpreted functions $f(t_1), f(t_2)$
+by fresh variables $f_1, f_2$ and addes axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$.
+The reduction has the effect of eliminating uninterpreted functions. When the reduction
+produces a pure bit-vector benchmark, it allows Z3 to use a specialized SAT solver.
+
+### Example
+
+```z3
+(declare-const x (_ BitVec 32))
+(declare-const y (_ BitVec 32))
+(declare-fun f ((_ BitVec 32)) (_ BitVec 8))
+
+(assert (not (= (f x) (f y))))
+(apply ackermannize_bv)
+```
+
+### Notes
+
+* does not support proofs, does not support unsatisfiable cores
+
+
 --*/
 
 #pragma once

src/ackermannization/ackr_model_converter.h

@@ -15,7 +15,7 @@ Revision History:
 --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model);

src/ackermannization/lackr_model_converter_lazy.h

@@ -16,7 +16,7 @@
  --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);

src/api/CMakeLists.txt

@@ -68,4 +68,5 @@ z3_add_component(api
     opt
     portfolio
     realclosure
+    extra_cmds
 )

src/api/api_arith.cpp

@@ -22,6 +22,8 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "math/polynomial/algebraic_numbers.h"
 
+#include <iostream>
+
 #define MK_ARITH_OP(NAME, OP) MK_NARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
 #define MK_BINARY_ARITH_OP(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
 #define MK_ARITH_PRED(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
@@ -88,7 +90,25 @@ extern "C" {
     MK_ARITH_PRED(Z3_mk_gt,  OP_GT);
     MK_ARITH_PRED(Z3_mk_le,  OP_LE);
     MK_ARITH_PRED(Z3_mk_ge,  OP_GE);
-    MK_ARITH_PRED(Z3_mk_divides, OP_IDIVIDES);
+
+    Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast n1, Z3_ast n2) {
+        Z3_TRY;
+        LOG_Z3_mk_divides(c, n1, n2);
+        RESET_ERROR_CODE();
+        rational val;
+        if (!is_expr(n1) || !mk_c(c)->autil().is_numeral(to_expr(n1), val) || !val.is_unsigned()) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            RETURN_Z3(nullptr);
+        }
+        parameter p(val.get_unsigned());
+        expr* arg = to_expr(n2);
+        expr* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_IDIVIDES, 1, &p, 1, &arg);
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP);
     MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP);
     MK_UNARY(Z3_mk_is_int,   mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP);

src/api/api_array.cpp

@@ -294,14 +294,19 @@ extern "C" {
         return Z3_mk_store(c, set, elem, Z3_mk_false(c));
     }
 
+    static bool is_array_sort(Z3_context c, Z3_sort t) {
+        return 
+            to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
+            to_sort(t)->get_decl_kind() == ARRAY_SORT;
+    }
+
     Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t) {
         Z3_TRY;
         LOG_Z3_get_array_sort_domain(c, t);
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, nullptr);
-        if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
-            to_sort(t)->get_decl_kind() == ARRAY_SORT) {
-            Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(0).get_ast());
+        if (is_array_sort(c, t)) {
+            Z3_sort r = of_sort(get_array_domain(to_sort(t), 0));
             RETURN_Z3(r);
         }
         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -314,10 +319,8 @@ extern "C" {
         LOG_Z3_get_array_sort_domain_n(c, t, idx);
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, nullptr);
-        if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
-            to_sort(t)->get_decl_kind() == ARRAY_SORT &&
-            get_array_arity(to_sort(t)) > idx) {
-            Z3_sort r = reinterpret_cast<Z3_sort>(get_array_domain(to_sort(t), idx));
+        if (is_array_sort(c, t) && get_array_arity(to_sort(t)) > idx) {
+            Z3_sort r = of_sort(get_array_domain(to_sort(t), idx));
             RETURN_Z3(r);
         }
         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@@ -330,10 +333,8 @@ extern "C" {
         LOG_Z3_get_array_sort_range(c, t);
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, nullptr);
-        if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
-            to_sort(t)->get_decl_kind() == ARRAY_SORT) {
-            unsigned n = to_sort(t)->get_num_parameters();
-            Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(n-1).get_ast());
+        if (is_array_sort(c, t)) {
+            Z3_sort r = of_sort(get_array_range(to_sort(t)));
             RETURN_Z3(r);
         }
         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);

src/api/api_ast.cpp

@@ -137,7 +137,7 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
         if (!p.has_def(d)) {
-            std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
+            std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
             SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
             return;
         }
@@ -158,6 +158,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return;
         }
+        if (!pd.get_def()->get_cases().empty()) {
+            std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
+            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            return;            
+        }
+                
         if (abs_body->get_sort() != d->get_range()) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);            
             return;

src/api/api_context.cpp

@@ -51,6 +51,8 @@ namespace api {
     }
 
     void context::del_object(api::object* o) {
+        if (!o)
+            return;
 #ifndef SINGLE_THREAD
         if (m_concurrent_dec_ref) {
             lock_guard lock(m_mux);
@@ -149,11 +151,13 @@ namespace api {
 
 
     context::~context() {
+        if (m_parser)
+            smt2::free_parser(m_parser);
         m_last_obj = nullptr;
         flush_objects();
         for (auto& kv : m_allocated_objects) {
             api::object* val = kv.m_value;
-            DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
+            DEBUG_CODE(if (!m_concurrent_dec_ref) warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
             dealloc(val);
         }
         if (m_params.owns_manager())

src/api/api_context.h

@@ -50,6 +50,11 @@ namespace realclosure {
     class manager;
 };
 
+namespace smt2 {
+    class parser;
+    void free_parser(parser*);
+};
+
 namespace api {
        
     class seq_expr_solver : public expr_solver {
@@ -233,6 +238,19 @@ namespace api {
 
         void check_sorts(ast * n);
 
+
+        // ------------------------------------------------
+        //
+        // State reused by calls to Z3_eval_smtlib2_string
+        //
+        // ------------------------------------------------
+        //
+        // The m_parser field is reused by all calls of Z3_eval_smtlib2_string using this context.
+        // It is an optimization to save the cost of recreating these objects on each invocation.
+        //
+        // See https://github.com/Z3Prover/z3/pull/6422 for the motivation
+        smt2::parser*                m_parser = nullptr;
+
         // ------------------------
         //
         // Polynomial manager & caches

src/api/api_datalog.cpp

@@ -395,8 +395,7 @@ extern "C" {
         Z3_string     s) {
         Z3_TRY;
         LOG_Z3_fixedpoint_from_string(c, d, s);
-        std::string str(s);
-        std::istringstream is(str);
+        std::istringstream is(s);
         RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
         Z3_CATCH_RETURN(nullptr);
     }

src/api/api_datatype.cpp

@@ -102,6 +102,13 @@ extern "C" {
         sort* e;
 
         ptr_vector<constructor_decl> constrs;
+        symbol sname = to_symbol(name);
+
+        if (mk_c(c)->get_dt_plugin()->is_declared(sname)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "enumeration sort name is already declared");
+            RETURN_Z3(nullptr);
+        }
+
         for (unsigned i = 0; i < n; ++i) {
             symbol e_name(to_symbol(enum_names[i]));
             std::string recognizer_s("is_");
@@ -112,8 +119,9 @@ extern "C" {
         }
 
 
+
         {
-            datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, n, constrs.data());
+            datatype_decl * dt = mk_datatype_decl(dt_util, sname, 0, nullptr, n, constrs.data());
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts);
             del_datatype_decl(dt);
 

src/api/api_opt.cpp

@@ -383,8 +383,7 @@ extern "C" {
         Z3_string     s) {
         Z3_TRY;
         //LOG_Z3_optimize_from_string(c, d, s);
-        std::string str(s);
-        std::istringstream is(str);
+        std::istringstream is(s);
         Z3_optimize_from_stream(c, d, is, nullptr);
         Z3_CATCH;
     }

src/api/api_params.cpp

@@ -116,7 +116,7 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         to_params(p)->m_params.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -208,7 +208,7 @@ extern "C" {
             buffer << to_param_descrs_ptr(p)->get_param_name(i);
         }
         buffer << ")";
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

src/api/api_parsers.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include "solver/solver_na2as.h"
 #include "muz/fp/dl_cmds.h"
 #include "opt/opt_cmds.h"
+#include "cmd_context/extra_cmds/proof_cmds.h"
 
 
 
@@ -42,6 +43,7 @@ extern "C" {
             ast_manager& m = c.m();
             ctx = alloc(cmd_context, false, &(m));
             install_dl_cmds(*ctx.get());
+            install_proof_cmds(*ctx.get());
             install_opt_cmds(*ctx.get());
             install_smt2_extra_cmds(*ctx.get());            
             ctx->register_plist();
@@ -124,7 +126,7 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) {
+    static Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) {
         Z3_TRY;
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);        
@@ -155,14 +157,14 @@ extern "C" {
     Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string str) {
         Z3_TRY;
         LOG_Z3_parser_context_from_string(c, pc, str);
-        std::string s(str);
-        std::istringstream is(s);
+        std::istringstream is(str);
         auto& ctx = to_parser_context(pc)->ctx;
         Z3_ast_vector r = Z3_parser_context_parse_stream(c, ctx, false, is);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
 
+    static
     Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
                                        unsigned num_sorts,
                                        Z3_symbol const _sort_names[],
@@ -174,6 +176,7 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(m));
         install_dl_cmds(*ctx.get());
+        install_proof_cmds(*ctx.get());
         install_opt_cmds(*ctx.get());
         install_smt2_extra_cmds(*ctx.get());
         ctx->register_plist();
@@ -198,8 +201,7 @@ extern "C" {
                                           Z3_func_decl const decls[]) {
         Z3_TRY;
         LOG_Z3_parse_smtlib2_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
-        std::string s(str);
-        std::istringstream is(s);
+        std::istringstream is(str);
         Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
@@ -232,19 +234,20 @@ extern "C" {
             auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
             mk_c(c)->cmd() = ctx;
             install_dl_cmds(*ctx);
+            install_proof_cmds(*ctx);
             install_opt_cmds(*ctx);
             install_smt2_extra_cmds(*ctx);
             ctx->register_plist();
             ctx->set_solver_factory(mk_smt_strategic_solver_factory());
         }
         scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
-        std::string s(str);
-        std::istringstream is(s);
+        std::istringstream is(str);
         ctx->set_regular_stream(ous);
         ctx->set_diagnostic_stream(ous);
         cmd_context::scoped_redirect _redirect(*ctx);
         try {
-            if (!parse_smt2_commands(*ctx.get(), is)) {
+            // See api::context::m_parser for a motivation about the reuse of the parser
+            if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
                 RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
             }
@@ -257,6 +260,4 @@ extern "C" {
         RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
         Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
     }
-
-
-};
+}

src/api/api_seq.cpp

@@ -212,6 +212,8 @@ extern "C" {
                 buffer.push_back('\\');
                 buffer.push_back('u');
                 buffer.push_back('{');
+                if (ch == 0)
+                    buff.push_back('0');
                 while (ch > 0) {
                     unsigned d = ch & 0xF;
                     if (d < 10)

src/api/api_solver.cpp

@@ -43,6 +43,7 @@ Revision History:
 #include "sat/sat_solver.h"
 #include "sat/tactic/goal2sat.h"
 #include "sat/tactic/sat2goal.h"
+#include "cmd_context/extra_cmds/proof_cmds.h"
 
 
 extern "C" {
@@ -257,8 +258,10 @@ extern "C" {
 
     void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
         auto& solver = *to_solver(s);
-        if (!solver.m_cmd_context) 
+        if (!solver.m_cmd_context) {
             solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m()));
+            install_proof_cmds(*solver.m_cmd_context);            
+        }
         auto& ctx = solver.m_cmd_context;
         ctx->set_ignore_check(true);
         std::stringstream errstrm;
@@ -270,6 +273,7 @@ extern "C" {
             return;
         }
 
+
         bool initialized = to_solver(s)->m_solver.get() != nullptr;
         if (!initialized)
             init_solver(c, s);
@@ -277,6 +281,10 @@ extern "C" {
             to_solver(s)->assert_expr(e);
         ctx->reset_tracked_assertions();
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
+        auto* ctx_s = ctx->get_solver();
+        if (ctx_s && ctx_s->get_proof())
+            to_solver_ref(s)->set_proof(ctx_s->get_proof());
+
     }
 
     static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) {
@@ -310,8 +318,7 @@ extern "C" {
     void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) {
         Z3_TRY;
         LOG_Z3_solver_from_string(c, s, c_str);
-        std::string str(c_str);
-        std::istringstream is(str);
+        std::istringstream is(c_str);
         if (is_dimacs_string(c_str)) {
             solver_from_dimacs_stream(c, s, is);
         }
@@ -399,7 +406,11 @@ extern "C" {
             params.validate(r);
             to_solver_ref(s)->updt_params(params);
         }
-        to_solver(s)->m_params.append(params);
+        auto& solver = *to_solver(s);        
+        solver.m_params.append(params);
+        
+        if (solver.m_cmd_context && solver.m_cmd_context->get_proof_cmds())
+            solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params);
 
         init_solver_log(c, s);
         
@@ -684,7 +695,29 @@ extern "C" {
         RESET_ERROR_CODE();
         init_solver(c, s);
         expr_ref_vector core(mk_c(c)->m());
-        to_solver_ref(s)->get_unsat_core(core);
+        solver_params sp(to_solver(s)->m_params);
+        unsigned timeout     = mk_c(c)->get_timeout();
+        timeout              = to_solver(s)->m_params.get_uint("timeout", timeout);
+        timeout              = sp.timeout() != UINT_MAX ? sp.timeout() : timeout;
+        unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", true);
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+        to_solver(s)->set_eh(&eh);
+        {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            try {
+                to_solver_ref(s)->get_unsat_core(core);
+            }
+            catch (...) {
+                to_solver_ref(s)->set_reason_unknown(eh);
+                to_solver(s)->set_eh(nullptr);
+                if (core.empty())
+                    throw;
+            }                    
+        }
+        to_solver(s)->set_eh(nullptr);
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
         for (expr* e : core) {
@@ -870,6 +903,26 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_solver_congruence_root(c, s, a);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        expr* r = to_solver_ref(s)->congruence_root(to_expr(a));
+        RETURN_Z3(of_expr(r));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_solver_congruence_next(c, s, a);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        expr* sib = to_solver_ref(s)->congruence_next(to_expr(a));
+        RETURN_Z3(of_expr(sib));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     class api_context_obj : public user_propagator::context_obj {
         api::context* c;
     public:
@@ -877,6 +930,45 @@ extern "C" {
         ~api_context_obj() override { dealloc(c); }
     };
 
+    struct scoped_ast_vector {
+        Z3_ast_vector_ref* v;
+        scoped_ast_vector(Z3_ast_vector_ref* v): v(v) { v->inc_ref(); }
+        ~scoped_ast_vector() { v->dec_ref(); }
+    };
+
+    void Z3_API Z3_solver_register_on_clause(
+        Z3_context  c, 
+        Z3_solver   s, 
+        void*       user_context,
+        Z3_on_clause_eh on_clause_eh) {
+        Z3_TRY;
+        RESET_ERROR_CODE();
+        init_solver(c, s);     
+        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned n, expr* const* _literals) {
+            Z3_ast_vector_ref * literals = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+            mk_c(c)->save_object(literals);
+            expr_ref pr(proof, mk_c(c)->m());
+            scoped_ast_vector _sc(literals);
+            for (unsigned i = 0; i < n; ++i)
+                literals->m_ast_vector.push_back(_literals[i]);
+            on_clause_eh(user_ctx, of_expr(pr.get()), of_ast_vector(literals));
+        };
+        to_solver_ref(s)->register_on_clause(user_context, _on_clause);
+        auto& solver = *to_solver(s);
+
+        if (!solver.m_cmd_context) {
+            solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m()));
+            install_proof_cmds(*solver.m_cmd_context);            
+        }
+
+        if (!solver.m_cmd_context->get_proof_cmds()) {
+            init_proof_cmds(*solver.m_cmd_context);
+            solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params);            
+        }
+        solver.m_cmd_context->get_proof_cmds()->register_on_clause(user_context, _on_clause);
+        Z3_CATCH;   
+    }
+
     void Z3_API Z3_solver_propagate_init(
         Z3_context  c, 
         Z3_solver   s, 

src/api/api_stats.cpp

@@ -28,7 +28,7 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         to_stats_ref(s).display_smt2(buffer);
-        std::string result = buffer.str();
+        std::string result = std::move(buffer).str();
         // Hack for removing the trailing '\n'
         SASSERT(result.size() > 0);
         result.resize(result.size()-1);

src/api/c++/z3++.h

@@ -158,7 +158,7 @@ namespace z3 {
     class context {
     private:
         friend class user_propagator_base;
-        bool       m_enable_exceptions;
+        bool       m_enable_exceptions = true;
         rounding_mode m_rounding_mode;
         Z3_context m_ctx = nullptr;
         void init(config & c) {
@@ -366,8 +366,14 @@ namespace z3 {
         void      recdef(func_decl, expr_vector const& args, expr const& body);
         func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
 
+        /**
+           \brief create an uninterpreted constant.
+         */
         expr constant(symbol const & name, sort const & s);
         expr constant(char const * name, sort const & s);
+        /**
+           \brief create uninterpreted constants of a given sort.
+         */
         expr bool_const(char const * name);
         expr int_const(char const * name);
         expr real_const(char const * name);
@@ -378,6 +384,12 @@ namespace z3 {
         template<size_t precision>
         expr fpa_const(char const * name);
 
+        /**
+           \brief create a de-Bruijn variable.
+         */
+        expr variable(unsigned index, sort const& s);
+        
+
         expr fpa_rounding_mode();
 
         expr bool_val(bool b);
@@ -1566,6 +1578,11 @@ namespace z3 {
         */
         expr substitute(expr_vector const& dst);
 
+        /**
+           \brief Apply function substitution by macro definitions.           
+        */
+        expr substitute(func_decl_vector const& funs, expr_vector const& bodies);
+
 
     class iterator {
             expr& e;
@@ -1902,21 +1919,21 @@ namespace z3 {
     inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
     inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
 
-    inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
     inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
 
-    inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
     inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
 
-    inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
     inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
 
-    inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
+    inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
+    inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr min(expr const& a, expr const& b) { 
         check_context(a, b); 
         Z3_ast r;
@@ -1930,6 +1947,7 @@ namespace z3 {
             assert(a.is_fpa());
             r = Z3_mk_fpa_min(a.ctx(), a, b); 
         }
+        a.check_error();
         return expr(a.ctx(), r); 
     }
     inline expr max(expr const& a, expr const& b) { 
@@ -1945,6 +1963,7 @@ namespace z3 {
             assert(a.is_fpa());
             r = Z3_mk_fpa_max(a.ctx(), a, b); 
         }
+        a.check_error();
         return expr(a.ctx(), r); 
     }
     inline expr bvredor(expr const & a) {
@@ -2670,10 +2689,10 @@ namespace z3 {
     public:
         struct simple {};
         struct translate {};
-        solver(context & c):object(c) { init(Z3_mk_solver(c)); }
-        solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }
+        solver(context & c):object(c) { init(Z3_mk_solver(c)); check_error(); }
+        solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); check_error(); }
         solver(context & c, Z3_solver s):object(c) { init(s); }
-        solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
+        solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
         solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
         solver(solver const & s):object(s) { init(s.m_solver); }
         ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
@@ -3575,6 +3594,11 @@ namespace z3 {
         return expr(*this, r);
     }
     inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
+    inline expr context::variable(unsigned idx, sort const& s) { 
+        Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
+        check_error();
+        return expr(*this, r);
+    }
     inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
     inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
     inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
@@ -4059,6 +4083,41 @@ namespace z3 {
         return expr(ctx(), r);
     }
 
+    inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
+        array<Z3_ast> _dst(dst.size());
+        array<Z3_func_decl> _funs(funs.size());
+        if (dst.size() != funs.size()) {
+            Z3_THROW(exception("length of argument lists don't align"));
+            return expr(ctx(), nullptr);
+        }
+        for (unsigned i = 0; i < dst.size(); ++i) {
+            _dst[i] = dst[i];
+            _funs[i] = funs[i];
+        }
+        Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
+        check_error();
+        return expr(ctx(), r);
+    }
+
+    typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t;
+
+    class on_clause {
+        context& c;
+        on_clause_eh_t m_on_clause;
+
+        static void _on_clause_eh(void* _ctx, Z3_ast _proof, Z3_ast_vector _literals) {
+            on_clause* ctx = static_cast<on_clause*>(_ctx);
+            expr_vector lits(ctx->c, _literals);
+            expr proof(ctx->c, _proof);
+            ctx->m_on_clause(proof, lits);
+        }
+    public:
+        on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {
+            m_on_clause = on_clause_eh;
+            Z3_solver_register_on_clause(c, s, this, _on_clause_eh);
+            c.check_error();
+        }        
+    };
 
     class user_propagator_base {
 
@@ -4314,6 +4373,16 @@ namespace z3 {
             Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
         }
 
+        void conflict(expr_vector const& fixed, expr_vector const& lhs, expr_vector const& rhs) {
+            assert(cb);
+            assert(lhs.size() == rhs.size());
+            expr conseq = ctx().bool_val(false);
+            array<Z3_ast> _fixed(fixed);
+            array<Z3_ast> _lhs(lhs);
+            array<Z3_ast> _rhs(rhs);
+            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
+        }
+
         void propagate(expr_vector const& fixed, expr const& conseq) {
             assert(cb);
             assert((Z3_context)conseq.ctx() == (Z3_context)ctx());

src/api/dotnet/AST.cs

@@ -208,37 +208,22 @@ namespace Microsoft.Z3
         internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); }
         internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            // Console.WriteLine("AST IncRef()");
-            if (Context == null || o == IntPtr.Zero)
-                return;
-            Context.AST_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            if (Context != null && o != IntPtr.Zero)
+                Native.Z3_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            // Console.WriteLine("AST DecRef()");
-            if (Context == null || o == IntPtr.Zero)
-                return;
-            Context.AST_DRQ.Add(o);
-            base.DecRef(o);
+            if (Context != null && o != IntPtr.Zero)
+            {
+                lock (Context)
+                {
+                    if (Context.nCtx != IntPtr.Zero)
+                        Native.Z3_dec_ref(Context.nCtx, o);
+                }
+            }
         }
 
         internal static AST Create(Context ctx, IntPtr obj)

src/api/dotnet/ASTMap.cs

@@ -125,31 +125,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.ASTMap_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_ast_map_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ASTMap_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_ast_map_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/ASTVector.cs

@@ -233,31 +233,19 @@ namespace Microsoft.Z3
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Debug.Assert(ctx != null); }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
-            }
-        };
 
         internal override void IncRef(IntPtr o)
         {
-            Context.ASTVector_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_ast_vector_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ASTVector_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_ast_vector_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/ApplyResult.cs

@@ -67,31 +67,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.ApplyResult_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_apply_result_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ApplyResult_DRQ.Add(o);
-            base.DecRef(o);
+            lock(Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_apply_result_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/CMakeLists.txt

@@ -59,7 +59,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     Context.cs
     DatatypeExpr.cs
     DatatypeSort.cs
-    Deprecated.cs
     EnumSort.cs
     Expr.cs
     FiniteDomainExpr.cs
@@ -76,7 +75,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     FuncInterp.cs
     Global.cs
     Goal.cs
-    IDecRefQueue.cs
     IntExpr.cs
     IntNum.cs
     IntSort.cs
@@ -89,6 +87,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     NativeFuncInterp.cs
     NativeModel.cs
     NativeSolver.cs
+    OnClause.cs
     Optimize.cs
     ParamDescrs.cs
     Params.cs

src/api/dotnet/Context.cs

@@ -42,6 +42,7 @@ namespace Microsoft.Z3
             lock (creation_lock)
             {
                 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
+                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                 InitContext();
             }
         }
@@ -75,6 +76,7 @@ namespace Microsoft.Z3
                 foreach (KeyValuePair<string, string> kv in settings)
                     Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
                 m_ctx = Native.Z3_mk_context_rc(cfg);
+                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                 Native.Z3_del_config(cfg);
                 InitContext();
             }
@@ -4793,7 +4795,6 @@ namespace Microsoft.Z3
             PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
             m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
             Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
-            GC.SuppressFinalize(this);
         }
 
         internal void CheckContextMatch(Z3Object other)
@@ -4852,123 +4853,9 @@ namespace Microsoft.Z3
 
         private void ObjectInvariant()
         {
-            Debug.Assert(m_AST_DRQ != null);
-            Debug.Assert(m_ASTMap_DRQ != null);
-            Debug.Assert(m_ASTVector_DRQ != null);
-            Debug.Assert(m_ApplyResult_DRQ != null);
-            Debug.Assert(m_FuncEntry_DRQ != null);
-            Debug.Assert(m_FuncInterp_DRQ != null);
-            Debug.Assert(m_Goal_DRQ != null);
-            Debug.Assert(m_Model_DRQ != null);
-            Debug.Assert(m_Params_DRQ != null);
-            Debug.Assert(m_ParamDescrs_DRQ != null);
-            Debug.Assert(m_Probe_DRQ != null);
-            Debug.Assert(m_Solver_DRQ != null);
-            Debug.Assert(m_Statistics_DRQ != null);
-            Debug.Assert(m_Tactic_DRQ != null);
-            Debug.Assert(m_Fixedpoint_DRQ != null);
-            Debug.Assert(m_Optimize_DRQ != null);
+            // none
         }
 
-        readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
-        readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
-        readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
-        readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
-        readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
-        readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
-        readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
-        readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
-        readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
-        readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
-        readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
-        readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
-        readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
-        readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
-        readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
-        readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
-
-        /// <summary>
-        /// AST DRQ
-        /// </summary>
-        public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } }
-
-        /// <summary>
-        /// ASTMap DRQ
-        /// </summary>
-        public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } }
-
-        /// <summary>
-        /// ASTVector DRQ
-        /// </summary>
-        public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } }
-
-        /// <summary>
-        /// ApplyResult DRQ
-        /// </summary>
-        public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } }
-
-        /// <summary>
-        /// FuncEntry DRQ
-        /// </summary>
-        public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } }
-
-        /// <summary>
-        /// FuncInterp DRQ
-        /// </summary>
-        public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } }
-
-        /// <summary>
-        /// Goal DRQ
-        /// </summary>
-        public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } }
-
-        /// <summary>
-        /// Model DRQ
-        /// </summary>
-        public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } }
-
-        /// <summary>
-        /// Params DRQ
-        /// </summary>
-        public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } }
-
-        /// <summary>
-        /// ParamDescrs DRQ
-        /// </summary>
-        public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } }
-
-        /// <summary>
-        /// Probe DRQ
-        /// </summary>
-        public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } }
-
-        /// <summary>
-        /// Solver DRQ
-        /// </summary>
-        public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } }
-
-        /// <summary>
-        /// Statistics DRQ
-        /// </summary>
-        public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } }
-
-        /// <summary>
-        /// Tactic DRQ
-        /// </summary>
-        public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } }
-
-        /// <summary>
-        /// FixedPoint DRQ
-        /// </summary>
-        public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } }
-
-        /// <summary>
-        /// Optimize DRQ
-        /// </summary>
-        public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } }
-
-        internal long refCount = 0;
-
         /// <summary>
         /// Finalizer.
         /// </summary>
@@ -4984,22 +4871,6 @@ namespace Microsoft.Z3
         public void Dispose()
         {
             // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
-            AST_DRQ.Clear(this);
-            ASTMap_DRQ.Clear(this);
-            ASTVector_DRQ.Clear(this);
-            ApplyResult_DRQ.Clear(this);
-            FuncEntry_DRQ.Clear(this);
-            FuncInterp_DRQ.Clear(this);
-            Goal_DRQ.Clear(this);
-            Model_DRQ.Clear(this);
-            Params_DRQ.Clear(this);
-            ParamDescrs_DRQ.Clear(this);
-            Probe_DRQ.Clear(this);
-            Solver_DRQ.Clear(this);
-            Statistics_DRQ.Clear(this);
-            Tactic_DRQ.Clear(this);
-            Fixedpoint_DRQ.Clear(this);
-            Optimize_DRQ.Clear(this);
 
             if (m_boolSort != null) m_boolSort.Dispose();
             if (m_intSort != null) m_intSort.Dispose();
@@ -5011,16 +4882,19 @@ namespace Microsoft.Z3
             m_realSort = null;
             m_stringSort = null;
             m_charSort = null;
-            if (refCount == 0 && m_ctx != IntPtr.Zero)
+            if (m_ctx != IntPtr.Zero)
             {
-                m_n_err_handler = null;
                 IntPtr ctx = m_ctx;
-                m_ctx = IntPtr.Zero;
-                if (!is_external) 
-                   Native.Z3_del_context(ctx);
+                lock (this)
+                {
+                    m_n_err_handler = null;
+                    m_ctx = IntPtr.Zero;
+                }
+                if (!is_external)
+                    Native.Z3_del_context(ctx);
             }
-            else
-                GC.ReRegisterForFinalize(this);
+
+            GC.SuppressFinalize(this);
         }
 
 

src/api/dotnet/Deprecated.cs

@@ -1,35 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    Deprecated.cs
-
-Abstract:
-
-    Expose deprecated features for use from the managed API 
-    those who use them for experiments.
-
-Author:
-
-    Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-    
---*/
-using System.Diagnostics;
-using System;
-using System.Collections.Generic;
-using System.Runtime.InteropServices;
-
-namespace Microsoft.Z3
-{
-    /// <summary>
-    /// The main interaction with Z3 happens via the Context.
-    /// </summary>
-    public class Deprecated 
-    {
-
-
-    }
-}

src/api/dotnet/Fixedpoint.cs

@@ -318,31 +318,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Fixedpoint_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_fixedpoint_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Fixedpoint_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_fixedpoint_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/FuncInterp.cs

@@ -85,31 +85,18 @@ namespace Microsoft.Z3
             #region Internal
             internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
-            internal class DecRefQueue : IDecRefQueue
-            {
-                public DecRefQueue() : base() { }
-                public DecRefQueue(uint move_limit) : base(move_limit) { }
-                internal override void IncRef(Context ctx, IntPtr obj)
-                {
-                    Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
-                }
-
-                internal override void DecRef(Context ctx, IntPtr obj)
-                {
-                    Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
-                }
-            };
-
             internal override void IncRef(IntPtr o)
             {
-                Context.FuncEntry_DRQ.IncAndClear(Context, o);
-                base.IncRef(o);
+                Native.Z3_func_entry_inc_ref(Context.nCtx, o);
             }
 
             internal override void DecRef(IntPtr o)
             {
-                Context.FuncEntry_DRQ.Add(o);
-                base.DecRef(o);
+                lock (Context)
+                {
+                    if (Context.nCtx != IntPtr.Zero)
+                        Native.Z3_func_entry_dec_ref(Context.nCtx, o);
+                }
             }
             #endregion
         };
@@ -190,31 +177,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.FuncInterp_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_func_interp_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.FuncInterp_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_func_interp_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/Goal.cs

@@ -252,33 +252,20 @@ namespace Microsoft.Z3
             : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0)))
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_goal_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_goal_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Goal_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_goal_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Goal_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_goal_dec_ref(Context.nCtx, o);
+            }
         }
 
         #endregion

src/api/dotnet/IDecRefQueue.cs

@@ -1,103 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    DecRefQueue.cs
-
-Abstract:
-
-    Z3 Managed API: DecRef Queues
-
-Author:
-
-    Christoph Wintersteiger (cwinter) 2012-03-16
-
-Notes:
-    
---*/
-
-using System.Diagnostics;
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-
-namespace Microsoft.Z3
-{
-    /// <summary>
-    /// DecRefQueue interface
-    /// </summary>
-    public abstract class IDecRefQueue
-    {
-        #region Object invariant
-
-        private void ObjectInvariant()
-        {
-            Debug.Assert(this.m_queue != null);
-        }
-
-        #endregion
-
-        readonly private Object m_lock = new Object();
-        readonly private List<IntPtr> m_queue = new List<IntPtr>();
-        private uint m_move_limit;
-
-        internal IDecRefQueue(uint move_limit = 1024)
-        {
-            m_move_limit = move_limit;
-        }
-
-        /// <summary>
-        /// Sets the limit on numbers of objects that are kept back at GC collection.
-        /// </summary>
-        /// <param name="l"></param>
-        public void SetLimit(uint l) { m_move_limit = l; }
-
-        internal abstract void IncRef(Context ctx, IntPtr obj);
-        internal abstract void DecRef(Context ctx, IntPtr obj);
-
-        internal void IncAndClear(Context ctx, IntPtr o)
-        {
-            Debug.Assert(ctx != null);
-
-            IncRef(ctx, o);
-            if (m_queue.Count >= m_move_limit) Clear(ctx);
-        }
-
-        internal void Add(IntPtr o)
-        {
-            if (o == IntPtr.Zero) return;
-
-            lock (m_lock)
-            {
-                m_queue.Add(o);
-            }
-        }
-
-        internal void Clear(Context ctx)
-        {
-            Debug.Assert(ctx != null);
-
-            lock (m_lock)
-            {
-                foreach (IntPtr o in m_queue)
-                    DecRef(ctx, o);
-                m_queue.Clear();
-            }
-        }
-    }
-
-    abstract class DecRefQueueContracts : IDecRefQueue
-    {
-        internal override void IncRef(Context ctx, IntPtr obj)
-        {
-            Debug.Assert(ctx != null);
-        }
-
-        internal override void DecRef(Context ctx, IntPtr obj)
-        {
-            Debug.Assert(ctx != null);
-        }
-    }
-}

src/api/dotnet/Model.cs

@@ -302,33 +302,20 @@ namespace Microsoft.Z3
             : base(ctx, obj)
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_model_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_model_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Model_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_model_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Model_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_model_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/OnClause.cs

@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    OnClause.cs
+
+Abstract:
+
+    Callback on clause inferences
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-19
+    
+Notes:
+
+
+--*/
+
+using System;
+using System.Diagnostics;
+using System.Linq;
+using System.Collections.Generic;
+using System.Runtime.InteropServices;
+
+namespace Microsoft.Z3
+{
+
+    using Z3_context = System.IntPtr;
+    using Z3_solver = System.IntPtr;
+    using voidp = System.IntPtr;
+    using Z3_ast = System.IntPtr;
+    using Z3_ast_vector = System.IntPtr;
+
+
+    /// <summary>
+    /// OnClause - clause inference callback
+    /// </summary>        
+    public class OnClause : IDisposable
+    {
+        /// <summary>
+        /// Delegate type for when clauses are inferred.
+	/// An inference is a pair comprising of
+        /// - a proof (hint). A partial (or comprehensive) derivation justifying the inference.
+	/// - a clause (vector of literals)	
+        /// The life-time of the proof hint and clause vector is limited to the scope of the callback.
+        /// should the callback want to store hints or clauses it will need to call Dup on the hints
+        /// and/or extract literals from the clause, respectively.
+        /// </summary>                
+        public delegate void OnClauseEh(Expr proof_hint, ASTVector clause);
+
+        
+        // access managed objects through a static array.
+        // thread safety is ignored for now.
+        GCHandle gch;
+        Solver solver;
+        Context ctx;
+	OnClauseEh on_clause;
+
+        Native.Z3_on_clause_eh on_clause_eh;
+
+	static void _on_clause(voidp ctx, Z3_ast _proof_hint, Z3_ast_vector _clause) 
+        {
+             var onc = (OnClause)GCHandle.FromIntPtr(ctx).Target;
+             using var proof_hint = Expr.Create(onc.ctx, _proof_hint);
+             using var clause = new ASTVector(onc.ctx, _clause);
+             onc.on_clause(proof_hint, clause);
+	}
+
+        /// <summary>
+        /// OnClause constructor
+        /// </summary>        
+        public OnClause(Solver s, OnClauseEh onc)
+        {
+            gch = GCHandle.Alloc(this);
+            solver = s;
+            ctx = solver.Context;
+            on_clause = onc;
+            on_clause_eh = _on_clause;
+            Native.Z3_solver_register_on_clause(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), on_clause_eh);
+        }
+
+        /// <summary>
+        /// Release private memory.
+        /// </summary>            
+        ~OnClause()
+        {
+            Dispose();
+        }
+        
+        /// <summary>
+        /// Must be called. The object will not be garbage collected automatically even if the context is disposed
+        /// </summary>
+        public virtual void Dispose()
+        {
+            if (!gch.IsAllocated)
+                return;
+            gch.Free();
+        }
+    }
+}

src/api/dotnet/Optimize.cs

@@ -440,31 +440,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Optimize_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_optimize_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Optimize_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_optimize_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/ParamDescrs.cs

@@ -91,33 +91,20 @@ namespace Microsoft.Z3
             : base(ctx, obj)
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }       
 
         internal override void IncRef(IntPtr o)
         {
-            Context.ParamDescrs_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_param_descrs_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ParamDescrs_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_param_descrs_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/Params.cs

@@ -147,33 +147,20 @@ namespace Microsoft.Z3
             : base(ctx, Native.Z3_mk_params(ctx.nCtx))
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_params_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_params_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Params_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_params_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Params_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_params_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/Probe.cs

@@ -70,31 +70,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_probe_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_probe_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Probe_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_probe_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Probe_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_probe_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/Solver.cs

@@ -538,31 +538,18 @@ namespace Microsoft.Z3
             this.BacktrackLevel = uint.MaxValue;
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_solver_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_solver_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Solver_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_solver_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Solver_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_solver_dec_ref(Context.nCtx, o);
+            }
         }
 
         private Status lboolToStatus(Z3_lbool r) 

src/api/dotnet/Statistics.cs

@@ -19,8 +19,6 @@ Notes:
 
 using System;
 using System.Diagnostics;
-
-
 namespace Microsoft.Z3
 {
 
@@ -189,31 +187,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_stats_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_stats_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Statistics_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_stats_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Statistics_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_stats_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/Tactic.cs

@@ -107,34 +107,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        /// <summary>
-        /// DecRefQueue
-        /// </summary>
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Tactic_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_tactic_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Tactic_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_tactic_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }

src/api/dotnet/UserPropagator.cs

@@ -37,7 +37,7 @@ namespace Microsoft.Z3
     /// <summary>
     /// Propagator context for .Net
     /// </summary>        
-    public class UserPropagator
+    public class UserPropagator : IDisposable
     {
         /// <summary>
         /// Delegate type for fixed callback
@@ -205,10 +205,20 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Release provate memory.
+        /// Release private memory.
         /// </summary>            
         ~UserPropagator()
         {
+            Dispose();
+        }
+        
+        /// <summary>
+        /// Must be called. The object will not be garbage collected automatically even if the context is disposed
+        /// </summary>
+        public virtual void Dispose()
+        {
+            if (!gch.IsAllocated)
+                return;
             gch.Free();
             if (solver == null)
                 ctx.Dispose();

src/api/dotnet/Z3Object.cs

@@ -50,12 +50,7 @@ namespace Microsoft.Z3
                 m_n_obj = IntPtr.Zero;                
             }
 
-            if (m_ctx != null)
-            {
-                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
-                    GC.ReRegisterForFinalize(m_ctx);
-                m_ctx = null;
-            }
+            m_ctx = null;
 
             GC.SuppressFinalize(this);
         }
@@ -76,19 +71,15 @@ namespace Microsoft.Z3
         internal Z3Object(Context ctx)
         {
             Debug.Assert(ctx != null);
-
-            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
         internal Z3Object(Context ctx, IntPtr obj)
         {
             Debug.Assert(ctx != null);
-
-            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
-            IncRef(obj);
             m_n_obj = obj;
+            IncRef(obj);
         }
 
         internal virtual void IncRef(IntPtr o) { }
@@ -109,7 +100,7 @@ namespace Microsoft.Z3
 
         internal static IntPtr GetNativeObject(Z3Object s)
         {
-            if (s == null) return new IntPtr();
+            if (s == null) return IntPtr.Zero;
             return s.NativeObject;
         }
 

src/api/java/ArraySort.java

@@ -35,6 +35,18 @@ public class ArraySort<D extends Sort, R extends Sort> extends Sort
                 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
     }
 
+    /**
+     * The domain of a multi-dimensional array sort.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     * @return a sort
+     **/
+    public D getDomain(int idx)
+    {
+        return (D) Sort.create(getContext(),
+			       Native.getArraySortDomainN(getContext().nCtx(), getNativeObject(), idx));
+    }
+
     /**
      * The range of the array sort.
      * @throws Z3Exception 

src/api/js/README.md

@@ -11,6 +11,9 @@ You'll need to have emscripten set up, along with all of its dependencies. The e
 
 Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeScript wrapper, and `npm run build:wasm` to build the wasm artifact.
 
+### Build on your own
+
+Consult the file [build-wasm.ts](https://github.com/Z3Prover/z3/blob/master/src/api/js/scripts/build-wasm.ts) for configurations used for building  wasm.
 
 ## Tests
 

src/api/js/package.json

@@ -35,7 +35,8 @@
   "contributors": [
     "Kevin Gibbons <bakkot@gmail.com>",
     "Nikolaj Bjorner",
-    "Olaf Tomalka <olaf@tomalka.me>"
+    "Olaf Tomalka <olaf@tomalka.me>",
+    "Walden Yan <waldenyan20@gmail.com>"
   ],
   "devDependencies": {
     "@types/jest": "^27.5.1",
@@ -49,6 +50,7 @@
     "prettier": "^2.5.1",
     "rimraf": "^3.0.2",
     "sprintf-js": "^1.1.2",
+    "ts-expect": "^1.3.0",
     "ts-jest": "^28.0.3",
     "ts-node": "^10.8.0",
     "typedoc": "^0.22.17",

src/api/js/scripts/parse-api.ts

@@ -45,6 +45,8 @@ const types = {
   __proto__: null,
 
   // these are function types I can't be bothered to parse
+  // NSB: They can be extracted automatically from z3_api.h thanks to the use 
+  // of a macro.
   Z3_error_handler: 'Z3_error_handler',
   Z3_push_eh: 'Z3_push_eh',
   Z3_pop_eh: 'Z3_pop_eh',
@@ -54,6 +56,7 @@ const types = {
   Z3_final_eh: 'Z3_final_eh',
   Z3_created_eh: 'Z3_created_eh',
   Z3_decide_eh: 'Z3_decide_eh',
+  Z3_on_clause_eh: 'Z3_on_clause_eh',
 } as unknown as Record<string, string>;
 
 export type ApiParam = { kind: string; sizeIndex?: number; type: string };

src/api/js/src/high-level/high-level.test.ts

@@ -2,6 +2,7 @@ import assert from 'assert';
 import asyncToArray from 'iter-tools/methods/async-to-array';
 import { init, killThreads } from '../jest';
 import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types';
+import { expectType } from "ts-expect";
 
 /**
  * Generate all possible solutions from given assumptions.
@@ -113,7 +114,7 @@ describe('high-level', () => {
     const { Solver, Not, Int } = api.Context('main');
     const solver = new Solver();
     solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))")
-    expect(await solver.check()).toStrictEqual('sat')    
+    expect(await solver.check()).toStrictEqual('sat')
     const x = Int.const('x')
     solver.add(Not(x.eq(1)))
     expect(await solver.check()).toStrictEqual('unsat')
@@ -211,6 +212,7 @@ describe('high-level', () => {
         }
         return cells;
       }
+
       const INSTANCE = toSudoku(`
         ....94.3.
         ...51...7
@@ -390,6 +392,106 @@ describe('high-level', () => {
     });
   });
 
+  describe('arrays', () => {
+
+    it('Example 1', async () => {
+      const Z3 = api.Context('main');
+
+      const arr = Z3.Array.const('arr', Z3.Int.sort(), Z3.Int.sort());
+      const [idx, val] = Z3.Int.consts('idx val');
+
+      const conjecture = (arr.store(idx, val).select(idx).eq(val));
+      await prove(conjecture);
+    });
+
+    it('domain and range type inference', async () => {
+      const { BitVec, Array, isArray, isArraySort } = api.Context('main');
+
+      const arr = Array.const('arr', BitVec.sort(160), BitVec.sort(256));
+
+      const domain = arr.domain();
+      expect(domain.size()).toStrictEqual(160);
+      expect(arr.domain_n(0).size()).toStrictEqual(160);
+      const range = arr.range();
+      expect(range.size()).toStrictEqual(256);
+
+      assert(isArray(arr) && isArraySort(arr.sort));
+
+      const arr2 = Array.const('arr2', BitVec.sort(1), BitVec.sort(2), BitVec.sort(3));
+      const dom2 = arr2.domain_n(1);
+
+      // We can call size() on dom2 and see that it is two bits
+      // purely from type inference
+      expectType<2>(dom2.size());
+
+      // Won't let us create an array constant with only one of domain/range
+      // and is detected at compile time
+      // @ts-expect-error
+      const arr3 = Array.const('arr3', BitVec.sort(1));
+    })
+
+    it('can do simple proofs', async () => {
+      const { BitVec, Array, isArray, isArraySort, isConstArray, Eq, Not } = api.Context('main');
+
+      const idx = BitVec.const('idx', 160);
+      const val = BitVec.const('val', 256);
+
+      const FIVE_VAL = BitVec.val(5, 256);
+
+      const arr = Array.const('arr', BitVec.sort(160), BitVec.sort(256));
+
+      const constArr = Array.K(BitVec.sort(160), FIVE_VAL);
+      assert(isArray(arr) && isArraySort(arr.sort) && isConstArray(constArr));
+
+      const arr2 = arr.store(0, 5);
+      await prove(Eq(arr2.select(0), FIVE_VAL));
+      await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256))));
+      await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx)));
+
+      // TODO: add in Quantifiers and better typing of arrays
+      // await prove(
+      //   ForAll([idx], idx.add(1).ugt(idx).and(arr.select(idx.add(1)).ugt(arr.select(idx)))).implies(
+      //     arr.select(0).ult(arr.select(1000))
+      //   )
+      // );
+    });
+
+    it('Finds arrays that differ but that sum to the same', async () => {
+      const Z3 = api.Context('main');
+      const { Array, BitVec } = Z3;
+
+      const mod = 1n << 32n;
+
+      const arr1 = Array.const('arr', BitVec.sort(2), BitVec.sort(32));
+      const arr2 = Array.const('arr2', BitVec.sort(2), BitVec.sort(32));
+
+      const same_sum = arr1.select(0)
+        .add(arr1.select(1))
+        .add(arr1.select(2))
+        .add(arr1.select(3))
+        .eq(
+          arr2.select(0)
+            .add(arr2.select(1))
+            .add(arr2.select(2))
+            .add(arr2.select(3))
+        );
+
+      const different = arr1.select(0).neq(arr2.select(0))
+        .or(arr1.select(1).neq(arr2.select(1)))
+        .or(arr1.select(2).neq(arr2.select(2)))
+        .or(arr1.select(3).neq(arr2.select(3)));
+
+      const model = await solve(same_sum.and(different));
+
+      const arr1Vals = [0, 1, 2, 3].map(i => model.eval(arr1.select(i)).value());
+      const arr2Vals = [0, 1, 2, 3].map(i => model.eval(arr2.select(i)).value());
+      expect((arr1Vals.reduce((a, b) => a + b, 0n) % mod) === arr2Vals.reduce((a, b) => a + b, 0n) % mod);
+      for (let i = 0; i < 4; i++) {
+        expect(arr1Vals[i] !== arr2Vals[i]);
+      }
+    });
+  });
+
   describe('Solver', () => {
     it('can use push and pop', async () => {
       const { Solver, Int } = api.Context('main');

src/api/js/src/high-level/high-level.ts

@@ -37,7 +37,7 @@ import {
   AnyExpr,
   AnySort,
   Arith,
-  ArithSort,
+  ArithSort, ArrayIndexType,
   Ast,
   AstMap,
   AstMapCtor,
@@ -48,7 +48,7 @@ import {
   BitVecSort,
   Bool,
   BoolSort,
-  CheckSatResult,
+  CheckSatResult, CoercibleFromMap,
   CoercibleRational,
   CoercibleToBitVec,
   CoercibleToExpr,
@@ -63,6 +63,8 @@ import {
   Model,
   Probe,
   RatNum,
+  SMTArray,
+  SMTArraySort,
   Solver,
   Sort,
   SortToExprMap,
@@ -86,12 +88,11 @@ function isCoercibleRational(obj: any): obj is CoercibleRational {
     (obj.denominator !== null &&
       (typeof obj.denominator === 'number' || typeof obj.denominator === 'bigint'))
   );
-  r &&
-    assert(
-      (typeof obj.numerator !== 'number' || Number.isSafeInteger(obj.numerator)) &&
-        (typeof obj.denominator !== 'number' || Number.isSafeInteger(obj.denominator)),
-      'Fraction numerator and denominator must be integers',
-    );
+  r && assert(
+    (typeof obj!.numerator !== 'number' || Number.isSafeInteger(obj!.numerator)) &&
+    (typeof obj!.denominator !== 'number' || Number.isSafeInteger(obj!.denominator)),
+    'Fraction numerator and denominator must be integers',
+  );
   return r;
 }
 
@@ -151,7 +152,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
   function createContext<Name extends string>(name: Name, options?: Record<string, any>): Context<Name> {
     const cfg = Z3.mk_config();
     if (options != null) {
-      Object.entries(options).forEach(([key, value]) => check(Z3.set_param_value(cfg, key, value.toString())));
+      Object.entries(options).forEach(
+        ([key, value]) => check(Z3.set_param_value(cfg, key, value.toString()))
+      );
     }
     const contextPtr = Z3.mk_context_rc(cfg);
     Z3.set_ast_print_mode(contextPtr, Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
@@ -216,20 +219,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
           return new ArithSortImpl(ast);
         case Z3_sort_kind.Z3_BV_SORT:
           return new BitVecSortImpl(ast);
+        case Z3_sort_kind.Z3_ARRAY_SORT:
+          return new ArraySortImpl(ast);
         default:
           return new SortImpl(ast);
       }
     }
 
-    function _toExpr(ast: Z3_ast): Bool<Name> | IntNum<Name> | RatNum<Name> | Arith<Name> | Expr<Name> {
+    function _toExpr(ast: Z3_ast): AnyExpr<Name> {
       const kind = check(Z3.get_ast_kind(contextPtr, ast));
       if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
         if (Z3.is_quantifier_forall(contextPtr, ast))
-           return new BoolImpl(ast);
+          return new BoolImpl(ast);
         if (Z3.is_quantifier_exists(contextPtr, ast))
-           return new BoolImpl(ast);
+          return new BoolImpl(ast);
         if (Z3.is_lambda(contextPtr, ast))
-           return new ExprImpl(ast);
+          return new ExprImpl(ast);
         assert(false);
       }
       const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));
@@ -251,6 +256,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
             return new BitVecNumImpl(ast);
           }
           return new BitVecImpl(ast);
+        case Z3_sort_kind.Z3_ARRAY_SORT:
+          return new ArrayImpl(ast);
         default:
           return new ExprImpl(ast);
       }
@@ -440,6 +447,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return r;
     }
 
+    function isArraySort(obj: unknown): obj is SMTArraySort<Name> {
+      const r = obj instanceof ArraySortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isArray(obj: unknown): obj is SMTArray<Name> {
+      const r = obj instanceof ArrayImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isConstArray(obj: unknown): boolean {
+      return isAppOf(obj, Z3_decl_kind.Z3_OP_CONST_ARRAY);
+    }
+
     function isProbe(obj: unknown): obj is Probe<Name> {
       const r = obj instanceof ProbeImpl;
       r && _assertContext(obj);
@@ -508,9 +531,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     // expression simplification //
     ///////////////////////////////
 
-    async function simplify(e : Expr<Name>) {
-       const result = await Z3.simplify(contextPtr, e.ast)       
-       return _toExpr(check(result));
+    async function simplify(e: Expr<Name>) {
+      const result = await Z3.simplify(contextPtr, e.ast)
+      return _toExpr(check(result));
     }
 
     /////////////
@@ -677,6 +700,44 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         );
       },
     };
+    const Array = {
+      sort<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        ...sig: [...DomainSort, RangeSort]
+      ): SMTArraySort<Name, DomainSort, RangeSort> {
+        const arity = sig.length - 1;
+        const r = sig[arity];
+        const d = sig[0];
+        if (arity === 1) {
+          return new ArraySortImpl(Z3.mk_array_sort(contextPtr, d.ptr, r.ptr));
+        }
+        const dom = sig.slice(0, arity);
+        return new ArraySortImpl(Z3.mk_array_sort_n(contextPtr, dom.map(s => s.ptr), r.ptr));
+      },
+      const<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        name: string, ...sig: [...DomainSort, RangeSort]
+      ): SMTArray<Name, DomainSort, RangeSort> {
+        return new ArrayImpl<DomainSort, RangeSort>(
+          check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(...sig).ptr))
+        );
+      },
+      consts<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        names: string | string[],
+        ...sig: [...DomainSort, RangeSort]
+      ): SMTArray<Name, DomainSort, RangeSort>[] {
+        if (typeof names === 'string') {
+          names = names.split(' ');
+        }
+        return names.map(name => Array.const(name, ...sig));
+      },
+      K<DomainSort extends AnySort<Name>, RangeSort extends AnySort<Name>>(
+        domain: DomainSort,
+        value: SortToExprMap<RangeSort, Name>
+      ): SMTArray<Name, [DomainSort], RangeSort> {
+        return new ArrayImpl<[DomainSort], RangeSort>(
+          check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr))
+        );
+      }
+    }
 
     ////////////////
     // Operations //
@@ -948,6 +1009,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
       readonly ptr: Z3_solver;
       readonly ctx: Context<Name>;
+
       constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) {
         this.ctx = ctx;
         let myPtr: Z3_solver;
@@ -964,21 +1026,26 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       push() {
         Z3.solver_push(contextPtr, this.ptr);
       }
+
       pop(num: number = 1) {
         Z3.solver_pop(contextPtr, this.ptr, num);
       }
+
       numScopes() {
         return Z3.solver_get_num_scopes(contextPtr, this.ptr);
       }
+
       reset() {
         Z3.solver_reset(contextPtr, this.ptr);
       }
+
       add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]) {
         _flattenArgs(exprs).forEach(expr => {
           _assertContext(expr);
           check(Z3.solver_assert(contextPtr, this.ptr, expr.ast));
         });
       }
+
       addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string) {
         if (typeof constant === 'string') {
           constant = Bool.const(constant);
@@ -1019,7 +1086,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return check(Z3.solver_to_string(contextPtr, this.ptr));
       }
 
-      fromString(s : string) {
+      fromString(s: string) {
         Z3.solver_from_string(contextPtr, this.ptr, s);
         throwIfError();
       }
@@ -1043,20 +1110,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return this.values();
       }
 
-      *entries(): IterableIterator<[number, FuncDecl<Name>]> {
+      * entries(): IterableIterator<[number, FuncDecl<Name>]> {
         const length = this.length();
         for (let i = 0; i < length; i++) {
           yield [i, this.get(i)];
         }
       }
 
-      *keys(): IterableIterator<number> {
+      * keys(): IterableIterator<number> {
         for (const [key] of this.entries()) {
           yield key;
         }
       }
 
-      *values(): IterableIterator<FuncDecl<Name>> {
+      * values(): IterableIterator<FuncDecl<Name>> {
         for (const [, value] of this.entries()) {
           yield value;
         }
@@ -1076,11 +1143,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
       eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>;
       eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>;
+      eval<Bits extends number = number>(expr: BitVec<Bits, Name>, modelCompletion?: boolean): BitVecNum<Bits, Name>;
       eval(expr: Expr<Name>, modelCompletion: boolean = false) {
         _assertContext(expr);
         const r = check(Z3.model_eval(contextPtr, this.ptr, expr.ast, modelCompletion));
         if (r === null) {
-          throw new Z3Error('Failed to evaluatio expression in the model');
+          throw new Z3Error('Failed to evaluate expression in the model');
         }
         return _toExpr(r);
       }
@@ -1092,7 +1160,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       get(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
       get(
         i: number | FuncDecl<Name> | Expr<Name> | Sort<Name>,
-        to?: number,
+        to?: number
       ): FuncDecl<Name> | FuncInterp<Name> | Expr<Name> | AstVector<Name, AnyAst<Name>> | FuncDecl<Name>[] {
         assert(to === undefined || typeof i === 'number');
         if (typeof i === 'number') {
@@ -1362,15 +1430,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       not(): Bool<Name> {
         return Not(this);
       }
+
       and(other: Bool<Name> | boolean): Bool<Name> {
         return And(this, other);
       }
+
       or(other: Bool<Name> | boolean): Bool<Name> {
         return Or(this, other);
       }
+
       xor(other: Bool<Name> | boolean): Bool<Name> {
         return Xor(this, other);
       }
+
+      implies(other: Bool<Name> | boolean): Bool<Name> {
+        return Implies(this, other);
+      }
     }
 
     class ProbeImpl implements Probe<Name> {
@@ -1571,27 +1646,35 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       add(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvadd(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       mul(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvmul(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sub(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsub(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sdiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsdiv(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       udiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvudiv(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       smod(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsmod(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       urem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvurem(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       srem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsrem(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       neg(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvneg(contextPtr, this.ast)));
       }
@@ -1599,33 +1682,43 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       or(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       and(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvand(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       nand(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvnand(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       xor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvxor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       xnor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvxnor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       shr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvashr(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       lshr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvlshr(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       shl(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvshl(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       rotateRight(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_ext_rotate_right(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       rotateLeft(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_ext_rotate_left(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       not(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvnot(contextPtr, this.ast)));
       }
@@ -1633,12 +1726,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       extract(high: number, low: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_extract(contextPtr, high, low, this.ast)));
       }
+
       signExt(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_sign_ext(contextPtr, count, this.ast)));
       }
+
       zeroExt(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_zero_ext(contextPtr, count, this.ast)));
       }
+
       repeat(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_repeat(contextPtr, count, this.ast)));
       }
@@ -1646,24 +1742,31 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       sle(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsle(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ule(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvule(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       slt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvslt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ult(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvult(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sge(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsge(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       uge(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvuge(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sgt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsgt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ugt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvugt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
@@ -1671,6 +1774,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       redAnd(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvredand(contextPtr, this.ast)));
       }
+
       redOr(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvredor(contextPtr, this.ast)));
       }
@@ -1678,24 +1782,31 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       addNoOverflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvadd_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       addNoUnderflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvadd_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       subNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsub_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       subNoUndeflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsub_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       sdivNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsdiv_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       mulNoOverflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvmul_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       mulNoUndeflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvmul_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       negNoOverflow(): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvneg_no_overflow(contextPtr, this.ast)));
       }
@@ -1703,6 +1814,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
     class BitVecNumImpl<Bits extends number> extends BitVecImpl<Bits> implements BitVecNum<Bits, Name> {
       declare readonly __typename: BitVecNum['__typename'];
+
       value() {
         return BigInt(this.asString());
       }
@@ -1718,14 +1830,87 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         }
         return val;
       }
+
       asString() {
         return Z3.get_numeral_string(contextPtr, this.ast);
       }
+
       asBinaryString() {
         return Z3.get_numeral_binary_string(contextPtr, this.ast);
       }
     }
 
+    class ArraySortImpl<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
+      RangeSort extends AnySort<Name> = Sort<Name>>
+      extends SortImpl
+      implements SMTArraySort<Name, DomainSort, RangeSort> {
+      declare readonly __typename: SMTArraySort['__typename'];
+
+      domain(): DomainSort[0] {
+        return _toSort(check(Z3.get_array_sort_domain(contextPtr, this.ptr)));
+      }
+
+      domain_n<T extends number>(i: T): DomainSort[T] {
+        return _toSort(check(Z3.get_array_sort_domain_n(contextPtr, this.ptr, i)));
+      }
+
+      range(): RangeSort {
+        return _toSort(check(Z3.get_array_sort_range(contextPtr, this.ptr))) as RangeSort;
+      }
+
+    }
+
+    class ArrayImpl<
+      DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
+      RangeSort extends AnySort<Name> = Sort<Name>
+    > extends ExprImpl<Z3_ast, ArraySortImpl<DomainSort, RangeSort>>
+      implements SMTArray<Name, DomainSort, RangeSort> {
+      declare readonly __typename: SMTArray['__typename'];
+
+      domain(): DomainSort[0] {
+        return this.sort.domain();
+      }
+
+      domain_n<T extends number>(i: T): DomainSort[T] {
+        return this.sort.domain_n(i);
+      }
+
+      range(): RangeSort {
+        return this.sort.range();
+      }
+
+      select(...indices: ArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name> {
+        const args = indices.map((arg, i) => this.domain_n(i).cast(arg as any));
+        if (args.length === 1) {
+          return _toExpr(check(Z3.mk_select(contextPtr, this.ast, args[0].ast))) as SortToExprMap<RangeSort, Name>;
+        }
+        const _args = args.map(arg => arg.ast);
+        return _toExpr(check(Z3.mk_select_n(contextPtr, this.ast, _args))) as SortToExprMap<RangeSort, Name>;
+      }
+
+      store(
+        ...indicesAndValue: [
+          ...ArrayIndexType<Name, DomainSort>,
+          CoercibleFromMap<SortToExprMap<RangeSort, Name>, Name>
+        ]
+      ): SMTArray<Name, DomainSort, RangeSort> {
+        const args = indicesAndValue.map((arg, i) => {
+          if (i === indicesAndValue.length - 1) {
+            return this.range().cast(arg as CoercibleFromMap<SortToExprMap<RangeSort, Name>, Name>);
+          }
+          return this.domain_n(i).cast(arg as any);
+        });
+        if (args.length <= 1) {
+          throw new Z3Error("Array store requires both index and value arguments");
+        }
+        if (args.length === 2) {
+          return _toExpr(check(Z3.mk_store(contextPtr, this.ast, args[0].ast, args[1].ast))) as SMTArray<Name, DomainSort, RangeSort>;
+        }
+        const _idxs = args.slice(0, args.length - 1).map(arg => arg.ast);
+        return _toExpr(check(Z3.mk_store_n(contextPtr, this.ast, _idxs, args[args.length - 1].ast))) as SMTArray<Name, DomainSort, RangeSort>;
+      }
+    }
+
     class AstVectorImpl<Item extends AnyAst<Name>> {
       declare readonly __typename: AstVector['__typename'];
       readonly ctx: Context<Name>;
@@ -1744,20 +1929,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return this.values();
       }
 
-      *entries(): IterableIterator<[number, Item]> {
+      * entries(): IterableIterator<[number, Item]> {
         const length = this.length();
         for (let i = 0; i < length; i++) {
           yield [i, this.get(i)];
         }
       }
 
-      *keys(): IterableIterator<number> {
+      * keys(): IterableIterator<number> {
         for (let [key] of this.entries()) {
           yield key;
         }
       }
 
-      *values(): IterableIterator<Item> {
+      * values(): IterableIterator<Item> {
         for (let [, value] of this.entries()) {
           yield value;
         }
@@ -1842,7 +2027,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return Z3.ast_map_size(contextPtr, this.ptr);
       }
 
-      *entries(): IterableIterator<[Key, Value]> {
+      * entries(): IterableIterator<[Key, Value]> {
         for (const key of this.keys()) {
           yield [key, this.get(key)];
         }
@@ -1852,11 +2037,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(Z3.ast_map_keys(contextPtr, this.ptr));
       }
 
-      *values(): IterableIterator<Value> {
+      * values(): IterableIterator<Value> {
         for (const [_, value] of this.entries()) {
           yield value;
         }
       }
+
       get(key: Key): Value {
         return _toAst(check(Z3.ast_map_find(contextPtr, this.ptr, key.ast))) as Value;
       }
@@ -1928,6 +2114,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       isBitVecSort,
       isBitVec,
       isBitVecVal, // TODO fix ordering
+      isArraySort,
+      isArray,
+      isConstArray,
       isProbe,
       isTactic,
       isAstVector,
@@ -1946,6 +2135,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Int,
       Real,
       BitVec,
+      Array,
 
       ////////////////
       // Operations //

src/api/python/z3/z3.py

@@ -1194,7 +1194,7 @@ def _coerce_expr_merge(s, a):
         else:
             if z3_debug():
                 _z3_assert(s1.ctx == s.ctx, "context mismatch")
-                _z3_assert(False, "sort mismatch")
+                _z3_assert(False, "sort mismatch")        
     else:
         return s
 
@@ -1207,6 +1207,11 @@ def _coerce_exprs(a, b, ctx=None):
         a = StringVal(a, b.ctx)
     if isinstance(b, str) and isinstance(a, SeqRef):
         b = StringVal(b, a.ctx)
+    if isinstance(a, float) and isinstance(b, ArithRef):
+        a = RealVal(a, b.ctx)
+    if isinstance(b, float) and isinstance(a, ArithRef):
+        b = RealVal(b, a.ctx)
+
     s = None
     s = _coerce_expr_merge(s, a)
     s = _coerce_expr_merge(s, b)
@@ -1464,7 +1469,9 @@ def FreshConst(sort, prefix="c"):
 
 def Var(idx, s):
     """Create a Z3 free variable. Free variables are used to create quantified formulas.
-
+    A free variable with index n is bound when it occurs within the scope of n+1 quantified
+    declarations.
+    
     >>> Var(0, IntSort())
     Var(0)
     >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
@@ -1552,13 +1559,15 @@ class BoolRef(ExprRef):
     def __mul__(self, other):
         """Create the Z3 expression `self * other`.
         """
-        if other == 1:
-            return self
-        if other == 0:
-            return 0
+        if isinstance(other, int) and other == 1:
+            return If(self, 1, 0)
+        if isinstance(other, int) and other == 0:
+            return IntVal(0, self.ctx)
+        if isinstance(other, BoolRef):
+            other = If(other, 1, 0)
         return If(self, other, 0)
 
-
+    
 def is_bool(a):
     """Return `True` if `a` is a Z3 Boolean expression.
 
@@ -4588,10 +4597,10 @@ class ArrayRef(ExprRef):
 
 def _array_select(ar, arg):
     if isinstance(arg, tuple):
-        args = [ar.domain_n(i).cast(arg[i]) for i in range(len(arg))]
+        args = [ar.sort().domain_n(i).cast(arg[i]) for i in range(len(arg))]
         _args, sz = _to_ast_array(args)
         return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx)
-    arg = ar.domain().cast(arg)
+    arg = ar.sort().domain().cast(arg)
     return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)
 
     
@@ -6653,7 +6662,7 @@ class ModelRef(Z3PPObject):
                 n = Z3_func_entry_get_num_args(x.ctx_ref(), e.entry)
                 v = AstVector()
                 for j in range(n):
-                    v.push(entry.arg_value(j))                    
+                    v.push(e.arg_value(j))                    
                 val = Z3_func_entry_get_value(x.ctx_ref(), e.entry)
                 Z3_func_interp_add_entry(x.ctx_ref(), fi2.f, v.vector, val)
             return
@@ -7232,6 +7241,22 @@ class Solver(Z3PPObject):
         cube are likely more useful to cube on."""
         return self.cube_vs
 
+    def root(self, t):
+        t = _py2expr(t, self.ctx)
+        """Retrieve congruence closure root of the term t relative to the current search state
+        The function primarily works for SimpleSolver. Terms and variables that are
+        eliminated during pre-processing are not visible to the congruence closure.
+        """
+        return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
+
+    def next(self, t):
+        t = _py2expr(t, self.ctx)
+        """Retrieve congruence closure sibling of the term t relative to the current search state
+        The function primarily works for SimpleSolver. Terms and variables that are
+        eliminated during pre-processing are not visible to the congruence closure.
+        """
+        return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
+
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""
         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
@@ -8832,7 +8857,7 @@ def substitute_vars(t, *m):
     return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
 
 def substitute_funs(t, *m):
-    """Apply subistitution m on t, m is a list of pairs of a function and expression (from, to)
+    """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
     Every occurrence in to of the function from is replaced with the expression to.
     The expression to can have free variables, that refer to the arguments of from.
     For examples, see 
@@ -10079,7 +10104,7 @@ def FPs(names, fpsort, ctx=None):
     >>> x.ebits()
     8
     >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
-    fpMul(RNE(), fpAdd(RNE(), x, y), z)
+    x + y * z
     """
     ctx = _get_ctx(ctx)
     if isinstance(names, str):
@@ -10186,9 +10211,9 @@ def fpAdd(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpAdd(rm, x, y)
-    fpAdd(RNE(), x, y)
-    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
     x + y
+    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
+    fpAdd(RTZ(), x, y)
     >>> fpAdd(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10203,7 +10228,7 @@ def fpSub(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpSub(rm, x, y)
-    fpSub(RNE(), x, y)
+    x - y
     >>> fpSub(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10218,7 +10243,7 @@ def fpMul(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpMul(rm, x, y)
-    fpMul(RNE(), x, y)
+    x * y
     >>> fpMul(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10233,7 +10258,7 @@ def fpDiv(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpDiv(rm, x, y)
-    fpDiv(RNE(), x, y)
+    x / y
     >>> fpDiv(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -11301,6 +11326,45 @@ def TransitiveClosure(f):
     """
     return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
 
+def to_Ast(ptr,):
+    ast = Ast(ptr)
+    super(ctypes.c_void_p, ast).__init__(ptr)
+    return ast
+
+def to_ContextObj(ptr,):
+    ctx = ContextObj(ptr)
+    super(ctypes.c_void_p, ctx).__init__(ptr)
+    return ctx
+
+def to_AstVectorObj(ptr,):
+    v = AstVectorObj(ptr)
+    super(ctypes.c_void_p, v).__init__(ptr)    
+    return v
+
+# NB. my-hacky-class only works for a single instance of OnClause
+# it should be replaced with a proper correlation between OnClause
+# and object references that can be passed over the FFI.
+# for UserPropagator we use a global dictionary, which isn't great code.
+
+_my_hacky_class = None
+def on_clause_eh(ctx, p, clause):
+    onc = _my_hacky_class
+    p = _to_expr_ref(to_Ast(p), onc.ctx)
+    clause = AstVector(to_AstVectorObj(clause), onc.ctx)
+    onc.on_clause(p, clause)
+    
+_on_clause_eh = Z3_on_clause_eh(on_clause_eh)
+
+class OnClause:
+    def __init__(self, s, on_clause):
+        self.s = s
+        self.ctx = s.ctx
+        self.on_clause = on_clause
+        self.idx = 22
+        global _my_hacky_class
+        _my_hacky_class = self
+        Z3_solver_register_on_clause(self.ctx.ref(), self.s.solver, self.idx, _on_clause_eh)        
+        
 
 class PropClosures:
     def __init__(self):
@@ -11358,11 +11422,6 @@ def user_prop_pop(ctx, cb, num_scopes):
     prop.cb = cb
     prop.pop(num_scopes)
 
-def to_ContextObj(ptr,):
-    ctx = ContextObj(ptr)
-    super(ctypes.c_void_p, ctx).__init__(ptr)
-    return ctx
-
 
 def user_prop_fresh(ctx, _new_ctx):
     _prop_closures.set_threaded()
@@ -11377,10 +11436,6 @@ def user_prop_fresh(ctx, _new_ctx):
     _prop_closures.set(new_prop.id, new_prop)
     return new_prop.id
 
-def to_Ast(ptr,):
-    ast = Ast(ptr)
-    super(ctypes.c_void_p, ast).__init__(ptr)
-    return ast
 
 def user_prop_fixed(ctx, cb, id, value):
     prop = _prop_closures.get(ctx)
@@ -11442,6 +11497,7 @@ _user_prop_eq = Z3_eq_eh(user_prop_eq)
 _user_prop_diseq = Z3_eq_eh(user_prop_diseq)
 _user_prop_decide = Z3_decide_eh(user_prop_decide)
 
+
 def PropagateFunction(name, *sig):
     """Create a function that gets tracked by user propagator.
        Every term headed by this function symbol is tracked.
@@ -11462,7 +11518,8 @@ def PropagateFunction(name, *sig):
         dom[i] = sig[i].ast
     ctx = rng.ctx
     return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
-      
+
+    
 
 class UserPropagateBase:
 

src/api/z3_api.h

@@ -1433,6 +1433,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_as
 Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast* t, unsigned* idx, Z3_lbool* phase));
+Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, Z3_ast_vector literals));
 
 
 /**
@@ -3762,7 +3763,7 @@ extern "C" {
        If \c s does not contain \c substr, then the value is -1, 
        def_API('Z3_mk_seq_last_index', AST, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr);
+    Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr);
 
     /**
        \brief Convert string to integer.
@@ -3892,7 +3893,7 @@ extern "C" {
 
        def_API('Z3_mk_re_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
      */
-    Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast, unsigned n);
+    Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast re, unsigned n);
 
     /**
        \brief Create the intersection of the regular languages.
@@ -4050,7 +4051,10 @@ extern "C" {
     Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
 
     /**
-       \brief Create a bound variable.
+       \brief Create a variable. 
+
+       Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables
+       even if they appear as free variables in the expression produced by \c Z3_mk_bound.
 
        Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
        the meaning of de-Bruijn indices by indicating the compilation process from
@@ -5317,8 +5321,9 @@ extern "C" {
                                 Z3_ast const to[]);
 
     /**
-       \brief Substitute the free variables in \c a with the expressions in \c to.
+       \brief Substitute the variables in \c a with the expressions in \c to.
        For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{to[i]}.
+       Note that a variable is created using the function \ref Z3_mk_bound. 
 
        def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
     */
@@ -5876,7 +5881,7 @@ extern "C" {
        def_API('Z3_eval_smtlib2_string', STRING, (_in(CONTEXT), _in(STRING),))
     */
 
-    Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
+    Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str);
 
 
     /** 
@@ -6877,6 +6882,44 @@ extern "C" {
     */
     void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz,  unsigned levels[]);
 
+    /**
+       \brief retrieve the congruence closure root of an expression.
+       The root is retrieved relative to the state where the solver was in when it completed.
+       If it completed during a set of case splits, the congruence roots are relative to these case splits.
+       That is, the congruences are not consequences but they are true under the current state.
+
+       def_API('Z3_solver_congruence_root', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a);
+
+
+    /**
+       \brief retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic list.
+       Repeated calls on the siblings will result in returning to the original expression.
+
+       def_API('Z3_solver_congruence_next', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a);
+
+
+    /**
+       \brief register a callback to that retrieves assumed, inferred and deleted clauses during search.
+       
+       \param c - context.
+       \param s - solver object.
+       \param user_context - a context used to maintain state for callbacks.
+       \param on_clause_eh - a callback that is invoked by when a clause is 
+                               - asserted to the CDCL engine (corresponding to an input clause after pre-processing)
+                               - inferred by CDCL(T) using either a SAT or theory conflict/propagation
+                               - deleted by the CDCL(T) engine
+
+       def_API('Z3_solver_register_on_clause', VOID, (_in(CONTEXT), _in(SOLVER), _in(VOID_PTR), _fnptr(Z3_on_clause_eh)))
+    */
+    void Z3_API Z3_solver_register_on_clause(
+        Z3_context  c, 
+        Z3_solver   s, 
+        void*       user_context,
+        Z3_on_clause_eh on_clause_eh);
 
     /**
        \brief register a user-properator with the solver.
@@ -7006,7 +7049,7 @@ extern "C" {
        def_API('Z3_solver_propagate_consequence', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, AST), _in(UINT), _in_array(4, AST), _in_array(4, AST), _in(AST)))
     */
     
-    void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);
+    void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);
 
     /**
        \brief Check whether the assertions in a given solver are consistent or not.

src/ast/arith_decl_plugin.h

@@ -447,12 +447,17 @@ public:
     app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); }
     app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.data()); }
     app * mk_add(expr_ref_buffer const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_buffer<expr> const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_vector<expr> const& args) const { return mk_add(args.size(), args.data()); }
 
     app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); }
     app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); }
     app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2); }
     app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2, arg3); }
     app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_MUL, num_args, args); }
+    app * mk_mul(ptr_buffer<expr> const& args) const { return mk_mul(args.size(), args.data()); }
+    app * mk_mul(ptr_vector<expr> const& args) const { return mk_mul(args.size(), args.data()); }
+    app * mk_mul(expr_ref_vector const& args) const { return mk_mul(args.size(), args.data()); }
     app * mk_uminus(expr * arg) const { return m_manager.mk_app(arith_family_id, OP_UMINUS, arg); }
     app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV, arg1, arg2); }
     app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV, arg1, arg2); }

src/ast/array_decl_plugin.cpp

@@ -122,7 +122,7 @@ bool array_decl_plugin::is_array_sort(sort* s) const {
 
 func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * domain) {
     if (arity != 1) {
-        m_manager->raise_exception("invalid const array definition, invalid domain size");
+        m_manager->raise_exception("invalid const array definition, expected one argument");
         return nullptr;
     }
     if (!is_array_sort(s)) {
@@ -529,19 +529,6 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
             return nullptr;
         }
         return mk_array_ext(arity, domain, parameters[0].get_int());
-    case OP_ARRAY_MAXDIFF:
-    case OP_ARRAY_MINDIFF: {
-        if (num_parameters != 0)
-            m_manager->raise_exception("min/maxdiff don't take any parameters");
-        if (arity != 2 || domain[0] != domain[1] || !is_array_sort(domain[0]) || 1 != get_array_arity(domain[0]))
-            m_manager->raise_exception("min/maxdiff don't take two arrays of same sort and with integer index");
-        sort* idx = get_array_domain(domain[0], 0);
-        arith_util arith(*m_manager);
-        if (!arith.is_int(idx))
-            m_manager->raise_exception("min/maxdiff take integer index domain");
-        return m_manager->mk_func_decl(k == OP_ARRAY_MAXDIFF ? symbol("maxdiff") : symbol("mindiff"), 
-                                       arity, domain, arith.mk_int(), func_decl_info(m_family_id, k));
-    }
     case OP_ARRAY_DEFAULT:
         return mk_default(arity, domain);
     case OP_SET_UNION:
@@ -603,9 +590,6 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
         op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
         op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
 
-        op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF));
-        op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF));
-
 #if 0
         op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE));
         op_names.push_back(builtin_name("card", OP_SET_CARD));

src/ast/array_decl_plugin.h

@@ -45,8 +45,6 @@ enum array_op_kind {
     OP_ARRAY_EXT,
     OP_ARRAY_DEFAULT,
     OP_ARRAY_MAP,
-    OP_ARRAY_MAXDIFF,
-    OP_ARRAY_MINDIFF,
     OP_SET_UNION,
     OP_SET_INTERSECT,
     OP_SET_DIFFERENCE,
@@ -161,8 +159,6 @@ public:
     bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
     bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
-    bool is_maxdiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAXDIFF); }
-    bool is_mindiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MINDIFF); }
     bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
     bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); }
     bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
@@ -189,8 +185,6 @@ public:
     bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
 
     MATCH_BINARY(is_subset);
-    MATCH_BINARY(is_maxdiff);
-    MATCH_BINARY(is_mindiff);
 };
 
 class array_util : public array_recognizers {
@@ -213,6 +207,10 @@ public:
         return mk_store(args.size(), args.data());
     }
 
+    app* mk_store(ptr_buffer<expr> const& args) const {
+        return mk_store(args.size(), args.data());
+    }
+
     app * mk_select(unsigned num_args, expr * const * args) const {
         return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
     }

src/ast/ast.cpp

@@ -856,11 +856,11 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_MODUS_PONENS_OEQ:             return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
     case PR_TH_LEMMA:                     return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
     case PR_HYPER_RESOLVE:                return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0);
-    case PR_ASSUMPTION_ADD:               return mk_proof_decl("add-assume", k, num_parents, m_assumption_add_decl);
-    case PR_LEMMA_ADD:                    return mk_proof_decl("add-lemma", k, num_parents, m_lemma_add_decl);
-    case PR_TH_ASSUMPTION_ADD:            return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl);
-    case PR_TH_LEMMA_ADD:                 return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl);
-    case PR_REDUNDANT_DEL:                return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl);
+    case PR_ASSUMPTION_ADD:               return mk_proof_decl("assume", k, num_parents, m_assumption_add_decl);
+    case PR_LEMMA_ADD:                    return mk_proof_decl("infer", k, num_parents, m_lemma_add_decl);
+    case PR_TH_ASSUMPTION_ADD:            return mk_proof_decl("th-assume", k, num_parents, m_th_assumption_add_decl);
+    case PR_TH_LEMMA_ADD:                 return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_add_decl);
+    case PR_REDUNDANT_DEL:                return mk_proof_decl("del", k, num_parents, m_redundant_del_decl);
     case PR_CLAUSE_TRAIL:                 return mk_proof_decl("proof-trail", k, num_parents, false);
     default:
         UNREACHABLE();
@@ -1969,6 +1969,14 @@ app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2,
     return mk_app(fid, k, 0, nullptr, 3, args);
 }
 
+app * ast_manager::mk_app(symbol const& name, unsigned n, expr* const* args, sort* range) {
+    ptr_buffer<sort> sorts;
+    for (unsigned i = 0; i < n; ++i)
+        sorts.push_back(args[i]->get_sort());
+    return mk_app(mk_func_decl(name, n, sorts.data(), range), n, args);
+}
+
+
 sort * ast_manager::mk_sort(symbol const & name, sort_info * info) {
     unsigned sz      = sort::get_obj_size();
     void * mem       = allocate_node(sz);
@@ -2242,7 +2250,9 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     if (type_error) {
         std::ostringstream buffer;
         buffer << "Wrong number of arguments (" << num_args
-               << ") passed to function " << mk_pp(decl, *this);
+               << ") passed to function " << mk_pp(decl, *this) << " ";
+        for (unsigned i = 0; i < num_args; ++i)
+            buffer << "\narg: " << mk_pp(args[i], *this) << "\n";
         throw ast_exception(std::move(buffer).str());
     }
     app * r = nullptr;
@@ -3027,11 +3037,23 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
             found_complement = true;
         }
     }
+    // patch to deal with lambdas introduced during search.
+    // lambdas can occur in terms both internalized and in raw form.
+    if (!found_complement && !is_or(f1) && num_proofs == 2) {
+        args.push_back(proofs[0]);
+        args.push_back(proofs[1]);
+        args.push_back(mk_false());
+        found_complement = true;
+    }
+
     if (!found_complement) {
         args.append(num_proofs, (expr**)proofs);
         CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n";
                for (unsigned i = 1; i < num_proofs; ++i)
                    tout << mk_pp(proofs[i], *this) << "\n";
+               tout << "facts\n";
+               for (unsigned i = 0; i < num_proofs; ++i)
+                   tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
                );
         SASSERT(is_or(f1));
         ptr_buffer<expr> new_lits;

src/ast/ast.h

@@ -531,6 +531,13 @@ public:
 #endif
 };
 
+#define MATCH_QUATARY(_MATCHER_)                                                                                \
+    bool _MATCHER_(expr const* n, expr*& a1, expr*& a2, expr *& a3, expr *& a4) const {                                \
+        if (_MATCHER_(n) && to_app(n)->get_num_args() == 4) {                                                   \
+            a1 = to_app(n)->get_arg(0); a2 = to_app(n)->get_arg(1); a3 = to_app(n)->get_arg(2); a4 = to_app(n)->get_arg(3); return true; } \
+        return false;                                                                                           \
+    }
+
 #define MATCH_TERNARY(_MATCHER_)                                                                                \
     bool _MATCHER_(expr const* n, expr*& a1, expr*& a2, expr *& a3) const {                                     \
         if (_MATCHER_(n) && to_app(n)->get_num_args() == 3) {                                                   \
@@ -724,6 +731,8 @@ public:
     unsigned get_num_args() const { return m_num_args; }
     expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
     expr * const * get_args() const { return m_args; }
+    std::tuple<expr*,expr*> args2() const { SASSERT(m_num_args == 2); return {get_arg(0), get_arg(1)}; }
+    std::tuple<expr*,expr*,expr*> args3() const { SASSERT(m_num_args == 3); return {get_arg(0), get_arg(1), get_arg(2)}; }
     unsigned get_size() const { return get_obj_size(get_num_args()); }
     expr * const * begin() const { return m_args; }
     expr * const * end() const { return m_args + m_num_args; }
@@ -1378,6 +1387,7 @@ inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->ge
 inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); }
 inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; }
 inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; }
+inline bool is_uninterp(func_decl const * n) { return n->get_family_id() == null_family_id; }
 inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; }
 inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); }
 inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); }
@@ -1874,6 +1884,8 @@ public:
         return mk_app(decl, 3, args);
     }
 
+    app * mk_app(symbol const& name, unsigned n, expr* const* args, sort* range);
+
     app * mk_const(func_decl * decl) {
         SASSERT(decl->get_arity() == 0);
         return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));

src/ast/ast_ll_pp.cpp

@@ -86,6 +86,7 @@ class ll_printer {
         default:
             display_child_ref(n);
         }
+
     }
 
     template<typename T>

src/ast/ast_pp_util.cpp

@@ -64,6 +64,17 @@ void ast_pp_util::display_decls(std::ostream& out) {
     m_rec_decls = n;
 }
 
+void ast_pp_util::reset() {
+    coll.reset();
+    m_removed.reset();
+    m_sorts.clear(0u);
+    m_decls.clear(0u);
+    m_rec_decls.clear(0u); 
+    m_is_defined.reset();
+    m_defined.reset();
+    m_defined_lim.reset(); 
+}
+
 void ast_pp_util::display_skolem_decls(std::ostream& out) {
     ast_smt_pp pp(m);
     unsigned n = coll.get_num_decls();

src/ast/ast_pp_util.h

@@ -40,8 +40,7 @@ class ast_pp_util {
     
     ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), m_defined(m), coll(m) {}
 
-    void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); 
-        m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); }
+    void reset();
 
     void collect(expr* e);
 

src/ast/ast_smt2_pp.cpp

@@ -561,15 +561,18 @@ class smt2_printer {
 
     void pp_var(var * v) {
         format * f;
-        if (v->get_idx() < m_var_names.size()) {
-            symbol s = m_var_names[m_var_names.size() - v->get_idx() - 1];
+        unsigned idx = v->get_idx();
+        if (idx < m_var_names.size()) {
+            symbol s;
+            if (m_reverse && idx < m_arity)
+                s = m_var_names[m_var_names.size() - m_arity + idx];
+            else
+                s = m_var_names[m_var_names.size() - idx - 1];
             std::string vname;
-            if (is_smt2_quoted_symbol (s)) {
-                vname = mk_smt2_quoted_symbol (s);
-            }
-            else {
-                vname = s.str();
-            }
+            if (is_smt2_quoted_symbol (s)) 
+                vname = mk_smt2_quoted_symbol (s);            
+            else 
+                vname = s.str();            
             f = mk_string(m(), vname);
         }
         else {
@@ -1139,9 +1142,13 @@ public:
         r = mk_seq1<format**, f2f>(m(), args, args+3, f2f(), cmd); 
     }
 
+    bool m_reverse = false;
+    unsigned m_arity = 0;
 
-    void operator()(func_decl * f, expr * e, format_ref & r, char const* cmd) {
+    void operator()(func_decl * f, expr * e, format_ref & r, char const* cmd, bool reverse) {
         unsigned len;
+        flet<bool> _reverse(m_reverse, reverse);
+        m_arity = f->get_arity();
         format * fname = m_env.pp_fdecl_name(f, len);
         register_var_names(f->get_arity());        
         format * args[4];
@@ -1202,9 +1209,9 @@ void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const &
     pr(f, r, cmd);
 }
 
-void mk_smt2_format(func_decl * f, expr * e, smt2_pp_environment & env, params_ref const & p, format_ref & r, char const* cmd) {
+void mk_smt2_format(func_decl * f, expr * e, smt2_pp_environment & env, params_ref const & p, format_ref & r, char const* cmd, bool reverse) {
     smt2_printer pr(env, p);
-    pr(f, e, r, cmd);
+    pr(f, e, r, cmd, reverse);
 }
 
 void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p,
@@ -1251,7 +1258,6 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
     if (!f) return out << "null";
     ast_manager & m = env.get_manager();
     format_ref r(fm(m));
-    sbuffer<symbol> var_names;
     mk_smt2_format(f, env, p, r, cmd);
     if (indent > 0)
         r = mk_indent(m, indent, r.get());
@@ -1259,12 +1265,11 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
     return out;
 }
 
-std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
+std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd, bool reverse) {
     if (!f) return out << "null";
     ast_manager & m = env.get_manager();
     format_ref r(fm(m));
-    sbuffer<symbol> var_names;
-    mk_smt2_format(f, e, env, p, r, cmd);
+    mk_smt2_format(f, e, env, p, r, cmd, reverse);
     if (indent > 0)
         r = mk_indent(m, indent, r.get());
     pp(out, r.get(), m, p);

src/ast/ast_smt2_pp.h

@@ -104,7 +104,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
                            unsigned num_vars = 0, char const * var_prefix = nullptr);
 std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun");
-std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
+std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun", bool reverse = false);
 std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
 std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
 

src/ast/bv_decl_plugin.h

@@ -411,6 +411,11 @@ public:
     app * mk_numeral(rational const & val, sort* s) const;
     app * mk_numeral(rational const & val, unsigned bv_size) const;
     app * mk_numeral(uint64_t u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); }
+    app * mk_zero(sort* s) const { return mk_numeral(rational::zero(), s); }
+    app * mk_zero(unsigned bv_size) const { return mk_numeral(rational::zero(), bv_size); }
+    app * mk_one(sort* s) const { return mk_numeral(rational::one(), s); }
+    app * mk_one(unsigned bv_size) const { return mk_numeral(rational::one(), bv_size); }
+
     sort * mk_sort(unsigned bv_size);
 
     unsigned get_bv_size(sort const * s) const {
@@ -430,6 +435,9 @@ public:
     }
     app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args);  }
     app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(expr_ref_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(ptr_buffer<expr> const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(ptr_vector<expr> const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
     app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args);  }
     app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args);  }
     app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args);  }
@@ -445,8 +453,17 @@ public:
     app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
     app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); }
     app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
+    app * mk_bv_add(ptr_buffer<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(ptr_vector<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_vector const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_buffer const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
     app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
     app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
+    app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); }
+    app* mk_bv_mul(ptr_buffer<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(ptr_vector<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_vector const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_buffer const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
     app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); }
     app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); }
     app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); }

src/ast/converters/CMakeLists.txt

@@ -0,0 +1,12 @@
+z3_add_component(converters
+  SOURCES
+    expr_inverter.cpp
+    equiv_proof_converter.cpp
+    generic_model_converter.cpp
+    horn_subsume_model_converter.cpp
+    model_converter.cpp
+    proof_converter.cpp
+    replace_proof_converter.cpp
+  COMPONENT_DEPENDENCIES
+    model
+)

src/ast/converters/equiv_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 #include "ast/ast_pp.h"
 #include "ast/scoped_proof.h"
 

src/ast/converters/equiv_proof_converter.h

@@ -23,7 +23,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 
 class equiv_proof_converter : public proof_converter {
     ast_manager&            m;

src/ast/converters/expr_inverter.cpp

@@ -0,0 +1,858 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    expr_inverter.cpp
+
+Abstract:
+
+    inverter interface and instance
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-11
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_util.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/converters/expr_inverter.h"
+
+class basic_expr_inverter : public iexpr_inverter {
+    iexpr_inverter& inv;
+
+    bool process_eq(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
+        expr* v;
+        expr* t;
+        if (uncnstr(arg1)) 
+            v = arg1, t = arg2;        
+        else if (uncnstr(arg2)) 
+            v = arg2, t = arg1;        
+        else
+            return false;
+
+        expr_ref d(m);
+        if (!inv.mk_diff(t, d))
+            return false;
+
+        mk_fresh_uncnstr_var_for(f, r);
+        if (m_mc)
+            add_def(v, m.mk_ite(r, t, d));
+
+        return true;
+    }
+
+public:
+
+    basic_expr_inverter(ast_manager& m, iexpr_inverter& inv) : iexpr_inverter(m), inv(inv) {}
+
+    family_id get_fid() const override { return m.get_basic_family_id(); }
+
+    /**
+     * if (c, x, x') -> fresh
+     * x := fresh
+     * x' := fresh
+     * 
+     * if (x, x', e) -> fresh
+     * x := true
+     * x' := fresh
+     * 
+     * if (x, t, x') -> fresh
+     * x := false
+     * x' := fresh
+     * 
+     * not x -> fresh
+     * x := not fresh
+     * 
+     * x & x' -> fresh
+     * x := fresh
+     * x' := true
+     * 
+     * x or x' -> fresh
+     * x := fresh
+     * x' := false
+     *
+     * x = t -> fresh
+     * x := if(fresh, t, diff(t))
+     * where diff is a diagnonalization function available in domains of size > 1.
+     *
+     */
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, proof_ref& pr) override {
+        SASSERT(f->get_family_id() == m.get_basic_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_ITE:
+            SASSERT(num == 3);
+            if (uncnstr(args[1]) && uncnstr(args[2])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[1], r);
+                add_def(args[2], r);
+                return true;
+            }
+            if (uncnstr(args[0]) && uncnstr(args[1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_true());
+                add_def(args[1], r);
+                return true;
+            }
+            if (uncnstr(args[0]) && uncnstr(args[2])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_false());
+                add_def(args[2], r);
+                return true;
+            }
+            return false;
+        case OP_NOT:
+            SASSERT(num == 1);
+            if (uncnstr(args[0])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_not(r));
+                return true;
+            }
+            return false;
+        case OP_AND:
+            if (num > 0 && uncnstr(num, args)) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_defs(num, args, r, m.mk_true());
+                return true;
+            }
+            return false;
+        case OP_OR:
+            if (num > 0 && uncnstr(num, args)) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_defs(num, args, r, m.mk_false());
+                return true;
+            }
+            return false;
+        case OP_EQ:
+            SASSERT(num == 2);
+            return process_eq(f, args[0], args[1], r);
+        default:
+            return false;
+        }        
+        return false;
+    }
+    
+    bool mk_diff(expr* t, expr_ref& r) override {
+        SASSERT(m.is_bool(t));
+        r = mk_not(m, t);
+        return true;
+    }
+};
+
+class arith_expr_inverter : public iexpr_inverter {
+    arith_util a;
+public:
+
+    arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {}
+
+    family_id get_fid() const override { return a.get_family_id(); }
+
+    bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) {
+        expr* v;
+        expr* t;
+        if (uncnstr(arg1)) {
+            v = arg1;
+            t = arg2;
+        }
+        else if (uncnstr(arg2)) {
+            v = arg2;
+            t = arg1;
+            le = !le;
+        }
+        else 
+            return false;
+        
+        mk_fresh_uncnstr_var_for(f, r);
+        if (m_mc) {
+            // v = ite(u, t, t + 1) if le
+            // v = ite(u, t, t - 1) if !le
+            add_def(v, m.mk_ite(r, t, a.mk_add(t, a.mk_numeral(rational(le ? 1 : -1), arg1->get_sort()))));
+        }
+        return true;
+    }
+
+    bool process_add(unsigned num, expr* const* args, expr_ref& u) {
+        if (num == 0)
+            return false;
+        unsigned i;
+        expr* v = nullptr;
+        for (i = 0; i < num; i++) {
+            expr* arg = args[i];
+            if (uncnstr(arg)) {
+                v = arg;
+                break;
+            }
+        }
+        if (v == nullptr)
+            return false;
+        mk_fresh_uncnstr_var_for(v->get_sort(), u);
+        if (!m_mc)
+            return true;
+        ptr_buffer<expr> new_args;
+        for (unsigned j = 0; j < num; j++) 
+            if (j != i)
+                new_args.push_back(args[j]);
+        
+        if (new_args.empty()) 
+            add_def(v, u);
+        else {
+            expr* rest = a.mk_add(new_args); 
+            add_def(v, a.mk_sub(u, rest));
+        }
+        return true;
+    }
+
+    bool process_arith_mul(unsigned num, expr* const* args, expr_ref & u) {
+        if (num == 0)
+            return false;
+        sort* s = args[0]->get_sort();
+        if (uncnstr(num, args)) {
+            mk_fresh_uncnstr_var_for(s, u);
+            if (m_mc)
+                add_defs(num, args, u, a.mk_numeral(rational(1), s));
+            return true;
+        }
+        // c * v case for reals
+        bool is_int;
+        rational val;
+        if (num == 2 && uncnstr(args[1]) && a.is_numeral(args[0], val, is_int) && !is_int) {
+            if (val.is_zero())
+                return false;
+            mk_fresh_uncnstr_var_for(s, u);
+            if (m_mc) {
+                val = rational(1) / val;
+                add_def(args[1], a.mk_mul(a.mk_numeral(val, false), u));
+            }
+            return true;
+        }
+        return false;
+    }
+
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, proof_ref& pr) override {
+        SASSERT(f->get_family_id() == a.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_ADD:
+            return process_add(num, args, r);
+        case OP_MUL:
+            return process_arith_mul(num, args, r);
+        case OP_LE:
+            SASSERT(num == 2);
+            return process_le_ge(f, args[0], args[1], true, r);
+        case OP_GE:
+            SASSERT(num == 2);
+            return process_le_ge(f, args[0], args[1], false, r);
+        default:
+            return false;
+        }
+    }
+
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        SASSERT(a.is_int_real(t));
+        r = a.mk_add(t, a.mk_numeral(rational(1), a.is_int(t)));
+        return true;
+    }
+};
+
+class bv_expr_inverter : public iexpr_inverter {
+    bv_util bv;
+
+    bool process_add(unsigned num, expr* const* args, expr_ref& u) {
+        if (num == 0)
+            return false;
+        unsigned i;
+        expr* v = nullptr;
+        for (i = 0; i < num; i++) {
+            expr* arg = args[i];
+            if (uncnstr(arg)) {
+                v = arg;
+                break;
+            }
+        }
+        if (!v)
+            return false;
+        mk_fresh_uncnstr_var_for(v->get_sort(), u);
+        if (!m_mc)
+            return true;
+        ptr_buffer<expr> new_args;
+        for (unsigned j = 0; j < num; j++)
+            if (j != i)
+                new_args.push_back(args[j]);
+
+        if (new_args.empty())
+            add_def(v, u);
+        else {
+            expr* rest = bv.mk_bv_add(new_args);
+            add_def(v, bv.mk_bv_sub(u, rest));
+        }
+        return true;
+    }
+
+    bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+        if (num == 0)
+            return false;
+        if (uncnstr(num, args)) {
+            sort* s = args[0]->get_sort();
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc)
+                add_defs(num, args, r, bv.mk_one(s));
+            return true;
+        }
+        // c * v (c is odd) case
+        unsigned sz;
+        rational val;
+        rational inv;
+        if (num == 2 &&
+            uncnstr(args[1]) &&
+            bv.is_numeral(args[0], val, sz) &&
+            val.mult_inverse(sz, inv)) {
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc)
+                add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv, sz), r));
+            return true;
+        }
+
+        //
+        // x * K -> fresh[hi-sh-1:0] ++ 0...0
+        // where sh = parity of K
+        // then x -> J^-1*fresh 
+        // where J = K >> sh
+        // Because x * K = fresh * K * J^-1 = fresh * 2^sh = fresh[hi-sh-1:0] ++ 0...0
+        //
+        if (num == 2 &&
+            uncnstr(args[1]) &&
+            bv.is_numeral(args[0], val, sz) &&
+            val.is_pos()) {
+            unsigned sh = 0;
+            while (val.is_even()) {
+                val /= rational(2);
+                ++sh;
+            }
+            mk_fresh_uncnstr_var_for(f, r);
+            if (sh > 0)
+                r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_zero(sh));
+
+            if (m_mc) {
+                rational inv_r;
+                VERIFY(val.mult_inverse(sz, inv_r));
+                add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), r)); 
+            }
+            return true;
+        }
+
+        //
+        // assume x is unconstrained, we can handle general multiplication as follows: 
+        // x * y -> if y = 0 then y else fresh << parity(y)
+        // and x -> if y = 0 then y else (y >> parity(y))^-1
+        // parity can be defined using a "giant" ite expression.
+        //
+
+#if 0
+        for (unsigned i = 0; i < num; ++i)
+            if (uncnstr(args[i]))
+                IF_VERBOSE(11, verbose_stream() << "MISSED mult-unconstrained " << mk_bounded_pp(args[i], m) << "\n");
+#endif
+
+        return false;
+    }
+
+
+    bool process_extract(func_decl* f, expr* arg, expr_ref& r) {
+        if (!uncnstr(arg))
+            return false;
+        mk_fresh_uncnstr_var_for(f, r);
+        if (!m_mc)
+            return true;
+        unsigned high = bv.get_extract_high(f);
+        unsigned low = bv.get_extract_low(f);
+        unsigned bv_size = bv.get_bv_size(arg->get_sort());
+        if (bv_size == high - low + 1) 
+            add_def(arg, r);        
+        else {
+            ptr_buffer<expr> args;
+            if (high < bv_size - 1)
+                args.push_back(bv.mk_zero(bv_size - high - 1));
+            args.push_back(r);
+            if (low > 0)
+                args.push_back(bv.mk_zero(low));
+            add_def(arg, bv.mk_concat(args.size(), args.data()));
+        }
+        return true;
+    }
+
+    bool process_bv_div(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
+        if (uncnstr(arg1) && uncnstr(arg2)) {
+            sort* s = arg1->get_sort();
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc) {
+                add_def(arg1, r);
+                add_def(arg2, bv.mk_one(s));
+            }
+            return true;
+        }
+        return false;
+    }
+
+    bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+        if (num == 0)
+            return false;
+        if (!uncnstr(num, args))
+            return false;
+        mk_fresh_uncnstr_var_for(f, r);
+        if (m_mc) {
+            unsigned i = num;
+            unsigned low = 0;
+            while (i > 0) {
+                --i;
+                expr* arg = args[i];
+                unsigned sz = bv.get_bv_size(arg);
+                add_def(arg, bv.mk_extract(low + sz - 1, low, r));
+                low += sz;
+            }
+        }
+        return true;
+    }
+
+    bool process_bv_le(func_decl* f, expr* arg1, expr* arg2, bool is_signed, expr_ref& r) {
+        unsigned bv_sz = bv.get_bv_size(arg1);
+        if (uncnstr(arg1) && uncnstr(arg2)) {
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc) {
+                add_def(arg1, m.mk_ite(r, bv.mk_zero(bv_sz), bv.mk_one(bv_sz)));
+                add_def(arg2, bv.mk_zero(bv_sz));
+            }
+            return true;
+        }
+        if (uncnstr(arg1)) {
+            // v <= t
+            expr* v = arg1;
+            expr* t = arg2;
+            // v <= t --->  (u or t == MAX)   u is fresh
+            //     add definition v = ite(u or t == MAX, t, t+1)
+            
+            rational MAX;
+            if (is_signed)
+                MAX = rational::power_of_two(bv_sz - 1) - rational(1);
+            else
+                MAX = rational::power_of_two(bv_sz) - rational(1);
+            mk_fresh_uncnstr_var_for(f, r);
+            r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MAX, bv_sz)));
+            if (m_mc)
+                add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_one(bv_sz))));
+            return true;
+        }
+        if (uncnstr(arg2)) {
+            // v >= t
+            expr* v = arg2;
+            expr* t = arg1;
+            // v >= t --->  (u ot t == MIN)  u is fresh
+            //    add definition v = ite(u or t == MIN, t, t-1)
+            rational MIN;
+            if (is_signed)
+                MIN = -rational::power_of_two(bv_sz - 1);
+            else
+                MIN = rational(0);
+            mk_fresh_uncnstr_var_for(f, r);
+            r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MIN, bv_sz)));
+            if (m_mc)
+                add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_one(bv_sz))));
+            return true;
+        }
+        return false;
+    }
+
+    bool process_bvnot(expr* e, expr_ref& r) {
+        if (!uncnstr(e))
+            return false;
+        mk_fresh_uncnstr_var_for(e->get_sort(), r);
+        if (m_mc)
+            add_def(e, bv.mk_bv_not(r));
+        return true;
+    }
+
+    bool process_shift(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
+        if (uncnstr(arg1) && uncnstr(arg2)) {
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc) {
+                add_def(arg1, r);
+                add_def(arg2, bv.mk_zero(arg2->get_sort()));
+            }
+            return true;
+        }
+        return false;
+    }
+
+    public:
+        bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {}
+
+        family_id get_fid() const override { return bv.get_family_id(); }
+
+    /**
+     * x + t -> fresh
+     * x := fresh - t
+     *
+     * x * x' * x'' -> fresh
+     * x := fresh
+     * x', x'' := 1
+     *
+     * c * x -> fresh, c is odd
+     * x := fresh*c^-1
+     *
+     * x[sz-1:0] -> fresh
+     * x := fresh
+     *
+     * x[hi:lo] -> fresh
+     * x := fresh1 ++ fresh ++ fresh2
+     *
+     * x udiv x', x sdiv x' -> fresh
+     * x' := 1
+     * x := fresh
+     *
+     * x ++ x' ++ x'' -> fresh
+     * x   := fresh[hi1:lo1]
+     * x'  := fresh[hi2:lo2]
+     * x'' := fresh[hi3:lo3]
+     *
+     * x <= t -> fresh or t == MAX
+     * x := if(fresh, t, t + 1)
+     * t <= x -> fresh or t == MIN
+     * x := if(fresh, t, t - 1)
+     *
+     * ~x -> fresh
+     * x := ~fresh
+     *
+     * x | y -> fresh
+     * x := fresh
+     * y := 0
+     *
+     */
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, proof_ref& pr) override {
+        SASSERT(f->get_family_id() == bv.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_BADD:
+            return process_add(num, args, r);
+        case OP_BMUL:
+            return process_bv_mul(f, num, args, r);
+        case OP_BSDIV:
+        case OP_BUDIV:
+        case OP_BSDIV_I:
+        case OP_BUDIV_I:
+            SASSERT(num == 2);
+            return process_bv_div(f, args[0], args[1], r);
+        case OP_SLEQ:
+            SASSERT(num == 2);
+            return process_bv_le(f, args[0], args[1], true, r);
+        case OP_ULEQ:
+            SASSERT(num == 2);
+            return process_bv_le(f, args[0], args[1], false, r);
+        case OP_CONCAT:
+            return process_concat(f, num, args, r);
+        case OP_EXTRACT:
+            SASSERT(num == 1);
+            return process_extract(f, args[0], r);
+        case OP_BNOT:
+            SASSERT(num == 1);
+            return process_bvnot(args[0], r);
+        case OP_BOR:
+            if (num > 0 && uncnstr(num, args)) {
+                sort* s = args[0]->get_sort();
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc)
+                    add_defs(num, args, r, bv.mk_zero(s));
+                return true;
+            }
+            return false;
+        case OP_BAND:
+            if (num > 0 && uncnstr(num, args)) {
+                sort* s = args[0]->get_sort();
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc)
+                    add_defs(num, args, r, bv.mk_numeral(rational::power_of_two(bv.get_bv_size(s)) - 1, s));
+                return true;
+            }
+            return false;
+        case OP_BSHL:
+        case OP_BASHR:
+        case OP_BLSHR:
+            return process_shift(f, args[0], args[1], r);
+        default:
+            return false;
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        SASSERT(bv.is_bv(t));
+        r = bv.mk_bv_not(t);
+        return true;
+    }
+};
+
+
+
+/**
+ * F[select(x, i)] -> F[fresh]
+ * x := const(fresh)
+
+ * F[store(x, ..., x')] -> F[fresh]
+ * x' := select(x, ...)
+ * x := fresh
+ */
+
+class array_expr_inverter : public iexpr_inverter {
+    array_util a;
+    iexpr_inverter& inv;
+public:
+    array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {}
+
+    family_id get_fid() const override { return a.get_family_id(); }
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, proof_ref& pr) override {
+        SASSERT(f->get_family_id() == a.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_SELECT:
+            if (uncnstr(args[0])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                sort* s = args[0]->get_sort();
+                if (m_mc)
+                    add_def(args[0], a.mk_const_array(s, r));
+                return true;
+            }
+            return false;
+        case OP_STORE:
+            if (uncnstr(args[0]) && uncnstr(args[num - 1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc) {
+                    add_def(args[num - 1], m.mk_app(a.get_family_id(), OP_SELECT, num - 1, args));
+                    add_def(args[0], r);
+                }
+                return true;
+            }
+            return false;
+        default:
+            return false;
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        sort* s = t->get_sort();
+        SASSERT(a.is_array(s));
+        if (m.is_uninterp(get_array_range(s)))
+            return false;
+        unsigned arity = get_array_arity(s);
+        for (unsigned i = 0; i < arity; i++)
+            if (m.is_uninterp(get_array_domain(s, i)))
+                return false;
+        // building 
+        // r = (store t i1 ... in d)
+        // where i1 ... in are arbitrary values
+        // and d is a term different from (select t i1 ... in)
+        expr_ref_vector new_args(m);
+        new_args.push_back(t);
+        for (unsigned i = 0; i < arity; i++)
+            new_args.push_back(m.get_some_value(get_array_domain(s, i)));
+        expr_ref sel(m);
+        sel = a.mk_select(new_args);
+        expr_ref diff_sel(m);
+        if (!inv.mk_diff(sel, diff_sel))
+            return false;
+        new_args.push_back(diff_sel);
+        r = a.mk_store(new_args);
+        return true;
+    }
+};
+
+
+
+class dt_expr_inverter : public iexpr_inverter {
+    datatype_util dt;
+public:
+
+    dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {}
+
+    family_id get_fid() const override { return dt.get_family_id(); }
+    /**
+     *   head(x) -> fresh
+     *   x := cons(fresh, arb)
+     */
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, proof_ref& pr) override {
+        if (dt.is_accessor(f)) {
+            SASSERT(num == 1);
+            if (uncnstr(args[0])) {
+                if (!m_mc) {
+                    mk_fresh_uncnstr_var_for(f, r);
+                    return true;
+                }
+                func_decl* c = dt.get_accessor_constructor(f);
+                for (unsigned i = 0; i < c->get_arity(); i++)
+                    if (!m.is_fully_interp(c->get_domain(i)))
+                        return false;
+                mk_fresh_uncnstr_var_for(f, r);
+                ptr_vector<func_decl> const& accs = *dt.get_constructor_accessors(c);
+                ptr_buffer<expr> new_args;
+                for (unsigned i = 0; i < accs.size(); i++) {
+                    if (accs[i] == f)
+                        new_args.push_back(r);
+                    else
+                        new_args.push_back(m.get_some_value(c->get_domain(i)));
+                }
+                add_def(args[0], m.mk_app(c, new_args));
+                return true;
+            }
+        }
+        return false;
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        // In the current implementation, I only handle the case where
+        // the datatype has a recursive constructor.
+        sort* s = t->get_sort();
+        ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(s);
+        for (func_decl* constructor : constructors) {
+            unsigned num = constructor->get_arity();
+            unsigned target = UINT_MAX;
+            for (unsigned i = 0; i < num; i++) {
+                sort* s_arg = constructor->get_domain(i);
+                if (s == s_arg) {
+                    target = i;
+                    continue;
+                }
+                if (m.is_uninterp(s_arg))
+                    break;
+            }
+            if (target == UINT_MAX)
+                continue;
+            // use the constructor the distinct term constructor(...,t,...)
+            ptr_buffer<expr> new_args;
+            for (unsigned i = 0; i < num; i++) {
+                if (i == target) 
+                    new_args.push_back(t);
+                else 
+                    new_args.push_back(m.get_some_value(constructor->get_domain(i)));
+            }
+            r = m.mk_app(constructor, new_args);
+            return true;
+        }
+        return false;
+    }
+};
+
+
+
+expr_inverter::~expr_inverter() {
+    for (auto* v : m_inverters)
+        dealloc(v);
+}
+
+
+bool iexpr_inverter::uncnstr(unsigned num, expr * const * args) const {
+    for (unsigned i = 0; i < num; i++)
+        if (!m_is_var(args[i]))
+            return false;
+    return true;
+}
+
+/**
+   \brief Create a fresh variable for abstracting (f args[0] ... args[num-1])
+   Return true if it a new variable was created, and false if the variable already existed for this
+   application. Store the variable in v
+*/
+void iexpr_inverter::mk_fresh_uncnstr_var_for(sort * s, expr_ref & v) {
+    v = m.mk_fresh_const(nullptr, s);
+    if (m_mc) 
+        m_mc->hide(v);
+}
+
+void iexpr_inverter::add_def(expr * v, expr * def) {
+    expr_ref _v(v, m);
+    expr_ref _d(def, m);
+    if (!m_mc)
+        return;
+    SASSERT(uncnstr(v));
+    SASSERT(to_app(v)->get_num_args() == 0);
+    m_mc->add(v, def);
+}
+
+void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* identity) {
+    expr_ref _id(identity, m);    
+    if (!m_mc)
+        return;
+    add_def(args[0], u);
+    for (unsigned i = 1; i < num; i++)
+        add_def(args[i], identity);
+}
+
+
+expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
+    auto add = [&](iexpr_inverter* i) {
+        m_inverters.setx(i->get_fid(), i, nullptr);
+    };
+    add(alloc(arith_expr_inverter, m));
+    add(alloc(bv_expr_inverter, m));
+    add(alloc(array_expr_inverter, m, *this));
+    add(alloc(dt_expr_inverter, m));
+    add(alloc(basic_expr_inverter, m, *this));
+}
+
+
+bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr, proof_ref& pr) {
+    if (num == 0)
+        return false;
+            
+    for (unsigned i = 0; i < num; i++) 
+        if (!is_ground(args[i]))
+            return false;
+
+    family_id fid = f->get_family_id();
+    if (fid == null_family_id)
+        return false;
+
+    auto* p = m_inverters.get(fid, nullptr);
+    return p && (*p)(f, num, args, new_expr, pr);       
+}
+
+bool expr_inverter::mk_diff(expr* t, expr_ref& r) {
+    sort * s = t->get_sort();
+    if (!m.is_fully_interp(s))
+        return false;
+
+    // If the interpreted sort has only one element,
+    // then it is unsound to eliminate the unconstrained variable in the equality
+    sort_size sz = s->get_num_elements();
+    if (sz.is_finite() && sz.size() <= 1)
+        return false;
+
+    if (!m_mc) {
+        // easy case, model generation is disabled.
+        mk_fresh_uncnstr_var_for(s, r);
+        return true;
+    }
+
+    family_id fid = s->get_family_id();
+    auto* p = m_inverters.get(fid, nullptr);
+    return p && p->mk_diff(t, r);
+}
+
+void expr_inverter::set_is_var(std::function<bool(expr*)>& is_var) {
+    for (auto* p : m_inverters)
+        if (p)
+            p->set_is_var(is_var);
+}
+
+void expr_inverter::set_model_converter(generic_model_converter* mc) {
+    m_mc = mc;
+    for (auto* p : m_inverters)
+        if (p)
+            p->set_model_converter(mc);
+}
+
+void expr_inverter::set_produce_proofs(bool pr) {
+    m_produce_proofs = pr;
+    for (auto* p : m_inverters)
+        if (p)
+            p->set_produce_proofs(pr);
+}

src/ast/converters/expr_inverter.h

@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    expr_inverter.h
+
+Abstract:
+
+    inverter interface and instance
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-11
+
+
+--*/
+#pragma once
+
+#include "ast/converters/generic_model_converter.h"
+
+class iexpr_inverter {
+protected:
+    ast_manager&                m;
+    std::function<bool(expr*)>  m_is_var;
+    generic_model_converter_ref m_mc;
+    bool                        m_produce_proofs = false;
+
+    bool uncnstr(expr* e) const { return m_is_var(e); }
+    bool uncnstr(unsigned num, expr * const * args) const;
+    void mk_fresh_uncnstr_var_for(sort* s, expr_ref& v);
+    void mk_fresh_uncnstr_var_for(func_decl* f, expr_ref& v) { mk_fresh_uncnstr_var_for(f->get_range(), v); }
+    void add_def(expr * v, expr * def);
+    void add_defs(unsigned num, expr * const * args, expr * u, expr * identity);
+
+public:
+    iexpr_inverter(ast_manager& m): m(m) {}
+    virtual ~iexpr_inverter() {}
+    virtual void set_is_var(std::function<bool(expr*)>& is_var) { m_is_var = is_var; }
+    virtual void set_model_converter(generic_model_converter* mc) { m_mc = mc; }
+    virtual void set_produce_proofs(bool p) { m_produce_proofs = true; }
+    
+    virtual bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, proof_ref& pr) = 0;
+    virtual bool mk_diff(expr* t, expr_ref& r) = 0;
+    virtual family_id get_fid() const = 0;
+};
+
+class expr_inverter : public iexpr_inverter {
+    ptr_vector<iexpr_inverter> m_inverters;
+
+public:
+    expr_inverter(ast_manager& m);
+    ~expr_inverter() override;
+    bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, proof_ref& pr) override;
+    bool mk_diff(expr* t, expr_ref& r) override;
+    void set_is_var(std::function<bool(expr*)>& is_var) override; 
+    void set_model_converter(generic_model_converter* mc) override;
+    void set_produce_proofs(bool p) override;
+    family_id get_fid() const override { return null_family_id;  }
+};

src/ast/converters/generic_model_converter.cpp

@@ -24,19 +24,13 @@ Notes:
 #include "ast/occurs.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
 
-
-generic_model_converter::~generic_model_converter() {
-}
-
-
 void generic_model_converter::add(func_decl * d, expr* e) {
     VERIFY(e);
     VERIFY(d->get_range() == e->get_sort());
-    m_first_idx.insert_if_not_there(d, m_entries.size());
     m_entries.push_back(entry(d, e, m, ADD));
 }
 

src/ast/converters/generic_model_converter.h

@@ -19,9 +19,10 @@ Notes:
 --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 
 class generic_model_converter : public model_converter {
+public:
     enum instruction { HIDE, ADD };
     struct entry {
         func_decl_ref m_f;
@@ -30,18 +31,16 @@ class generic_model_converter : public model_converter {
         entry(func_decl* f, expr* d, ast_manager& m, instruction i):
             m_f(f, m), m_def(d, m), m_instruction(i) {}
     };
+private:
     ast_manager& m;
     std::string  m_orig;
     vector<entry> m_entries;
-    obj_map<func_decl, unsigned> m_first_idx;
 
     expr_ref simplify_def(entry const& e);
 
 public:
     generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
     
-    ~generic_model_converter() override;
-    
     void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
 
     void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); }
@@ -67,6 +66,10 @@ public:
     void set_env(ast_pp_util* visitor) override;
 
     void get_units(obj_map<expr, bool>& units) override;
+
+    vector<entry> const& entries() const { return m_entries; }
+
+    void shrink(unsigned j) { m_entries.shrink(j); }
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;

src/ast/converters/horn_subsume_model_converter.cpp

@@ -18,14 +18,14 @@ Revision History:
 --*/
 
 
-#include "tactic/horn_subsume_model_converter.h"
-#include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
-#include "model/model_smt2_pp.h"
-#include "ast/rewriter/bool_rewriter.h"
-#include "ast/rewriter/th_rewriter.h"
 #include "ast/for_each_expr.h"
 #include "ast/well_sorted.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "model/model_smt2_pp.h"
+#include "ast/converters/horn_subsume_model_converter.h"
 
 void horn_subsume_model_converter::insert(app* head, expr* body) {
     m_delay_head.push_back(head);

src/ast/converters/horn_subsume_model_converter.h

@@ -34,7 +34,7 @@ Subsumption transformation (remove Horn clause):
 
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ast/rewriter/th_rewriter.h"
 
 class horn_subsume_model_converter : public model_converter {

src/ast/converters/model_converter.cpp

@@ -16,7 +16,7 @@ Author:
 Notes:
 
 --*/
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "model/model_v2_pp.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -26,7 +26,7 @@ Notes:
 void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
     VERIFY(e);
     VERIFY(f->get_range() == e->get_sort());
-    ast_smt2_pp(out, f, e, env, params_ref(), 0, "model-add") << "\n";
+    ast_smt2_pp(out, f, e, env, params_ref(), 0, "model-add", true) << "\n";
 }
 
 void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {

src/ast/converters/model_converter.h

@@ -57,7 +57,7 @@ Notes:
 #include "util/ref.h"
 #include "ast/ast_pp_util.h"
 #include "model/model.h"
-#include "tactic/converter.h"
+#include "ast/converters/converter.h"
 
 class labels_vec : public svector<symbol> {};
 class smt2_pp_environment; 
@@ -101,6 +101,10 @@ typedef sref_buffer<model_converter> model_converter_ref_buffer;
 
 model_converter * concat(model_converter * mc1, model_converter * mc2);
 
+inline model_converter * concat(model_converter * mc1, model_converter * mc2, model_converter* mc3) {
+    return concat(mc1, concat(mc2, mc3));
+}
+
 model_converter * model2model_converter(model * m);
 
 model_converter * model_and_labels2model_converter(model * m, labels_vec const &r);

src/ast/converters/proof_converter.cpp

@@ -16,8 +16,7 @@ Author:
 Notes:
 
 --*/
-#include "tactic/proof_converter.h"
-#include "tactic/goal.h"
+#include "ast/converters/proof_converter.h"
 #include "ast/ast_smt2_pp.h"
 
 class concat_proof_converter : public concat_converter<proof_converter> {
@@ -46,41 +45,6 @@ proof_converter * concat(proof_converter * pc1, proof_converter * pc2) {
     return alloc(concat_proof_converter, pc1, pc2);
 }
 
-class subgoal_proof_converter : public proof_converter {
-    proof_converter_ref m_pc;
-    goal_ref_buffer     m_goals;
-public:
-    subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals):
-        m_pc(pc)
-    {
-        for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]);
-    }
-
-    proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
-        // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals.
-        SASSERT(num_source == 0);
-        proof_converter_ref_buffer pc_buffer;          
-        for (goal_ref g : m_goals) {
-            pc_buffer.push_back(g->pc());
-
-        }
-        return apply(m, m_pc, pc_buffer);
-    }
-
-    proof_converter* translate(ast_translation& tr) override {
-        proof_converter_ref pc1 = m_pc->translate(tr);
-        goal_ref_buffer goals;
-        for (goal_ref g : m_goals) goals.push_back(g->translate(tr));
-        return alloc(subgoal_proof_converter, pc1.get(), goals.size(), goals.data());
-    }
-
-    void display(std::ostream& out) override {}
-    
-};
-
-proof_converter * concat(proof_converter *pc, unsigned n, goal* const* goals) {
-    return alloc(subgoal_proof_converter, pc, n, goals);
-}
 
 class proof2pc : public proof_converter {
     proof_ref m_pr;

src/ast/converters/proof_converter.h

@@ -20,8 +20,7 @@ Notes:
 
 #include "ast/ast.h"
 #include "util/ref.h"
-#include "tactic/converter.h"
-class goal;
+#include "ast/converters/converter.h"
 
 class proof_converter : public converter {
 public:
@@ -36,12 +35,6 @@ typedef sref_buffer<proof_converter> proof_converter_ref_buffer;
 
 proof_converter * concat(proof_converter * pc1, proof_converter * pc2);
 
-/**
-   \brief create a proof converter that takes a set of subgoals and converts their proofs to a proof of 
-   the goal they were derived from.
- */
-proof_converter * concat(proof_converter *pc1, unsigned n, goal* const* goals);
-
 proof_converter * proof2proof_converter(ast_manager & m, proof * pr);
 
 void apply(ast_manager & m, proof_converter * pc, proof_ref & pr);

src/ast/converters/replace_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/expr_functors.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"

src/ast/converters/replace_proof_converter.h

@@ -22,7 +22,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/proof_converter.h"
+#include "ast/converters/proof_converter.h"
 
 class replace_proof_converter : public proof_converter {
     ast_manager&    m;