QEL: Fast Approximated Quantifier Elimination #6820

agurfinkel · 2023-07-19T09:13:07Z

Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.

Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel: Fast Approximations of Quantifier Elimination. Computer-Aided Verification (CAV). 2023. URL: https://arxiv.org/abs/2306.10009

no change to code

Partial array equality, PEQ, is used as an intermediate expression during MBP for arrays. We need to factor it out so that it can be shared between MBP-QEL and existing MBP. Partial array equality (peq) is used in MBP for arrays. Factoring this out to be used by multiple MBP implementations.

These rules are specializes for terms that are created in QEL. QEL commit is comming later

The rule handles this special case: (cons (head x) (tail x)) --> x

Special rules to simplify PEQs

Spacer prfers to not have a term representing default value of an array. This guides IUC from picking such terms in interpolation

Class properties allow to keep information for an equivalence class. Getters and setters for terms allow accessing information

QEL commit is comming later in the history

Reperesent equalities explicitly by nodes in the term_graph

This changes the default projection engine that spacer uses.

New commands are mbp-qel -- MBP with term graphs qel -- QEL with term graphs qe-lite -- older qelite

NikolajBjorner · 2023-07-22T20:00:58Z

The Mac Build keeps failing on c_example.exe

On the build machine we get:

list_example
valid
valid
valid
valid
valid
valid
valid
Formula (=> ((_ is cons) u) (= u (cons (head u) (tail u))))
valid
valid
##[error]Bash exited with code '1'.

Locally on windows I get (in a "qel" fork):

list_example
valid
valid
valid
valid
valid
valid
valid
Formula (=> ((_ is (cons (Int int_list) int_list)) u) (= u (cons (head u) (tail u))))
valid
invalid
counterexample:
u -> nil

NikolajBjorner · 2023-07-22T20:03:02Z

Some build warnings on my Linux code space

In file included from /workspaces/z3/src/qe/qe_mbp.cpp:30:
/workspaces/z3/src/ast/rewriter/rewriter_def.h:702:6: warning: ‘void rewriter_tpl<Config>::update_inv_binding_at(unsigned int, expr*) [with Config = {anonymous}::rd_over_wr_rewriter]’ defined but not used [-Wunused-function]
  702 | void rewriter_tpl<Config>::update_inv_binding_at(unsigned i, expr* binding) {
      |      ^~~~~~~~~~~~~~~~~~~~
/workspaces/z3/src/ast/rewriter/rewriter_def.h:707:6: warning: ‘void rewriter_tpl<Config>::update_binding_at(unsigned int, expr*) [with Config = {anonymous}::rd_over_wr_rewriter]’ defined but not used [-Wunused-function]
  707 | void rewriter_tpl<Config>::update_binding_at(unsigned i, expr* binding) {
      |      ^~~~~~~~~~~~~~~~~~~~

NikolajBjorner · 2023-07-22T20:11:55Z

[143/264] Building CXX object src/muz/spacer/CMakeFiles/spacer.dir/spacer_global_generalizer.cpp.o
In file included from /workspaces/z3/src/muz/spacer/spacer_global_generalizer.h:22,
                 from /workspaces/z3/src/muz/spacer/spacer_global_generalizer.cpp:19:
/workspaces/z3/src/muz/spacer/spacer_convex_closure.h: In member function ‘void spacer::lemma_global_generalizer::subsumer::setup_cvx_closure(spacer::convex_closure&, const spacer::lemma_cluster&)’:
/workspaces/z3/src/muz/spacer/spacer_convex_closure.h:140:17: warning: ‘bv_width’ may be used uninitialized in this function [-Wmaybe-uninitialized]
  140 |         m_bv_sz = sz;
      |         ~~~~~~~~^~~~
/workspaces/z3/src/muz/spacer/spacer_global_generalizer.cpp:226:14: note: ‘bv_width’ was declared here
  226 |     unsigned bv_width;
      |              ^~~~~~~~

NikolajBjorner · 2023-07-22T20:15:17Z


 1773 |     app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args);
      |           ^~~~~~
/home/vsts/work/1/s/src/muz/spacer/spacer_cluster_util.cpp:177:30: note: ‘kids’ declared here
  177 |             ptr_buffer<expr> kids;
      |                              ^~~~

NikolajBjorner · 2023-07-22T22:41:29Z

src/qe/mbp/mbp_solve_plugin.cpp

            return res;
+


NikolajBjorner · 2023-07-22T22:41:37Z

src/qe/mbp/mbp_solve_plugin.cpp

-            if (!is_pos) {
-                res = mk_not(m, res);
-            }
+          if(try_int_mul_solve(atom, is_pos, res))


if( -> if (

NikolajBjorner · 2023-07-22T22:41:49Z

src/qe/mbp/mbp_solve_plugin.cpp

+
+          if (!a.is_int(lhs)) { return false; }
+
+          if(!a.is_mul(rhs)) {


if( -> if (

NikolajBjorner · 2023-07-22T22:41:56Z

src/qe/mbp/mbp_solve_plugin.cpp

+      // returns `true` if a rewritting happened
+      bool try_int_mul_solve(expr *atom, bool is_pos, expr_ref &res) {
+
+          if (!is_pos)


NikolajBjorner · 2023-07-22T22:42:35Z

src/qe/mbp/mbp_qel.h

+#include "ast/ast.h"
+#include "model/model.h"
+#include "util/params.h"
+


use C++ format for class declaration. See other headers where "public" keyword appears

NikolajBjorner · 2023-07-22T22:43:01Z

src/qe/mbp/mbp_qel.cpp

+                    add_vars(p, vars);
+                }
+            }
+        } while (progress);


} \n while (progress);

NikolajBjorner · 2023-07-22T22:43:32Z

src/qe/mbp/mbp_dt_tg.h

+#include "util/obj_hashtable.h"
+
+namespace mbp {
+class mbp_dt_tg: public mbp_tg_plugin {


indentation is not consistent

NikolajBjorner · 2023-07-22T22:44:20Z

src/ast/array_peq.cpp

@@ -0,0 +1,88 @@
+#include "ast/array_peq.h"


NikolajBjorner · 2023-07-22T22:44:41Z

could you also update RELEASE_NOTES.md?

hgvk94 · 2023-07-26T22:38:01Z

The Mac Build keeps failing on c_example.exe

On the build machine we get:

list_example
valid
valid
valid
valid
valid
valid
valid
Formula (=> ((_ is cons) u) (= u (cons (head u) (tail u))))
valid
valid
##[error]Bash exited with code '1'.

Locally on windows I get (in a "qel" fork):

list_example
valid
valid
valid
valid
valid
valid
valid
Formula (=> ((_ is (cons (Int int_list) int_list)) u) (= u (cons (head u) (tail u))))
valid
invalid
counterexample:
u -> nil

Fixed this. One of our rewrites was not general enough to be put in the theory rewriter. Will update PR.

NikolajBjorner · 2023-08-01T17:29:29Z

src/ast/rewriter/datatype_rewriter.cpp

@@ -21,33 +21,8 @@ Module Name:
 br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
    SASSERT(f->get_family_id() == get_fid());
    switch(f->get_decl_kind()) {
-    case OP_DT_CONSTRUCTOR: {


datatype_rewriter is used from other code paths than QEL.
Why would this code be deleted?

because it is unsound?

yes. The rewriter rewrites cons(head(x), tail(x)) into x. This is sound only if is_cons(x). In our MBP, we meet this precondition. In general, this is unsound

the latest commit (0e78d24) moves the rewrite into qe_mbp

oh, it is not in master branch anyway, or was removed

NikolajBjorner · 2023-08-01T23:34:56Z

RELEASE_NOTES.md

@@ -9,6 +9,7 @@ Version 4.next
  - polysat
    - native word level bit-vector solving.
  - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
+  - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.


Mention the new parameter smt.mbp_qsat_qel and what effect it has on using QEL (in qsat?). Elsewhere QEL is always on? And the command mbp-qel.

NikolajBjorner · 2023-08-01T23:42:59Z

RELEASE_NOTES.md

@@ -9,6 +9,7 @@ Version 4.next
  - polysat
    - native word level bit-vector solving.
  - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
+  - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.



It looks like qel is used to replace qe_lite in spacer, but otherwise qe-lite is exposed as usual as a tactic.
Nowadays I would create a "simplifier" (in ast/simplifiers) that invokes qe functionality such that it can be used incrementally and as a tactic. There is a simple wrapper that takes a simplifier and creates a tactic.
It should be relatively easy because qel preserves equivalence. It can be disabled if proof production is required.

Note that if qel was exposed as a tactic maybe the custom commands are not as critical for testing.
If the result of applying tactics from command-line isn't sufficient for use scenarios, we may wrap such differently. For example, we have the "simplify" command that takes an expression and returns an expression. A version for tactics are applied on expressions to expressions could be created if this is really what is needed for evaluation or command-line use.

Are we really going to have both qe-lite and qel?

In the medium term, we would like to see qe-lite be replaced with qel.

In the short term, there are still some problems that behave better with qe-lite. It is convenient to have qe-lite available for debugging and comparison until we resolve these issues as either bug fixes or expected anomalies.

It would be useful for us to switch all external users to qel to see that it is not creating any new or unexpected issues in the use-cases we have not tested for.

Do you want us to expose qel as a tactic similar to qe-lite for now?

I can't say for sure what to do in short term: the interface to qel requires at least some wrapping to create a simplifier. The wrapping could be through a rewriter where the method for handling quantifiers is changed. So rewriter, simplifier, tactic.
Not sure it is worth writing special case code for this when it really is a quantifier rewriter which applies also to the der rewriter, and qe-lite.

qe_light_tactic.cpp contains some qel namespace but not the calls into term graphs from what I can tell.

hgvk94 and others added 30 commits July 19, 2023 07:35

qe_lite: cleanup and comment

7b241c0

no change to code

rewriter: new rewrite rules

7886d17

These rules are specializes for terms that are created in QEL. QEL commit is comming later

datatype_rw: new rewrite rule for ADTs

7cd2e23

The rule handles this special case: (cons (head x) (tail x)) --> x

array_rewriter rules for rewriting PEQs

163ae2a

Special rules to simplify PEQs

th_rewriter: wire PEQ simplifications

f07a980

spacer_iuc: avoid terms with default in IUC

3610355

Spacer prfers to not have a term representing default value of an array. This guides IUC from picking such terms in interpolation

mbp_term_graph: replace root with repr

9c7e1f8

mbp_term_graph: formatting

822d9b4

mbp_term_graph: class_props, getters, setters

c250ad6

Class properties allow to keep information for an equivalence class. Getters and setters for terms allow accessing information

mbp_term_graph: auxiliary methods for qel

b1c022e

QEL commit is comming later in the history

mbp_term_graph: bug fix

090b95e

mbp_term_graph: pick, refine repr, compute cgrnd

4f7ade9

mbp_term_graph: internalize deq

bd80037

mbp_term_graph: constructor

7998376

mbp_term_graph: optionally internalize equalities

e2b3f72

Reperesent equalities explicitly by nodes in the term_graph

qel

cab7225

formatting

67e76ed

comments on term_lt

398783a

get terms and other api for mbp_qel

c203724

plugins for mbp_qel

53034f7

mbp_qel_util: utilities for mbp_qel

0e55b84

qe_mbp: QEL-based mbp

4140eb3

qel: expose QEL API

9e5b0d5

spacer: replace qe_lite in qe_project_spacer by qel

0509ce5

This changes the default projection engine that spacer uses.

cmd_context: debug commands for qel and mbp_qel

e9782a9

New commands are mbp-qel -- MBP with term graphs qel -- QEL with term graphs qe-lite -- older qelite

qe_mbp: model-based rewriters for arrays

1a7be27

qe_mbp: QEL-based projection functions

0115452

qsat: wire in QEL-based mbp

6fc9db5

qsat: debug code

aa8588c

agurfinkel added 2 commits July 20, 2023 07:17

mbp_qel_util: block comment + format

eb6a93d

mbt_term_graph: clang-format

9c4c1d6

NikolajBjorner reviewed Jul 22, 2023

View reviewed changes

src/qe/mbp/mbp_solve_plugin.cpp

return res;

Copy link

Contributor

NikolajBjorner Jul 22, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

2 -> 4

NikolajBjorner reviewed Jul 22, 2023

View reviewed changes

src/qe/mbp/mbp_solve_plugin.cpp Outdated

if (!a.is_int(lhs)) { return false; }

if(!a.is_mul(rhs)) {

Copy link

Contributor

NikolajBjorner Jul 22, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if( -> if (

NikolajBjorner reviewed Jul 22, 2023

View reviewed changes

src/qe/mbp/mbp_qel.cpp Outdated

add_vars(p, vars);

}

}

} while (progress);

Copy link

Contributor

NikolajBjorner Jul 22, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

} \n while (progress);

NikolajBjorner reviewed Jul 22, 2023

View reviewed changes

src/ast/array_peq.cpp

@@ -0,0 +1,88 @@

#include "ast/array_peq.h"

Copy link

Contributor

NikolajBjorner Jul 22, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

header

bug fix. Move dt rewrite to qe_mbp

0e78d24

NikolajBjorner reviewed Aug 1, 2023

View reviewed changes

hgvk94 added 7 commits August 1, 2023 18:59

array_peq: add header

8f59ff0

run clang format on mbp plugins

939ef12

clang format on mul solver

da034cc

format do-while

54a117d

format

fbb9cdd

format do-while

5ff449c

update release notes

e2649b9

NikolajBjorner reviewed Aug 1, 2023

View reviewed changes

NikolajBjorner merged commit 51d3c27 into Z3Prover:master Aug 2, 2023
20 checks passed

This was referenced Aug 4, 2023

Potential Horn soundness issue #6471

Open

MBP from API returns wrong result #6726

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

QEL: Fast Approximated Quantifier Elimination #6820

QEL: Fast Approximated Quantifier Elimination #6820

agurfinkel commented Jul 19, 2023

NikolajBjorner commented Jul 22, 2023 •

edited

NikolajBjorner commented Jul 22, 2023

NikolajBjorner commented Jul 22, 2023

NikolajBjorner commented Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner Jul 22, 2023

NikolajBjorner commented Jul 22, 2023

hgvk94 commented Jul 26, 2023

NikolajBjorner Aug 1, 2023

NikolajBjorner Aug 1, 2023

hgvk94 Aug 1, 2023

hgvk94 Aug 1, 2023

NikolajBjorner Aug 1, 2023

NikolajBjorner Aug 1, 2023 •

edited

NikolajBjorner Aug 1, 2023 •

edited

agurfinkel Aug 2, 2023

NikolajBjorner Aug 2, 2023

QEL: Fast Approximated Quantifier Elimination #6820

QEL: Fast Approximated Quantifier Elimination #6820

Conversation

agurfinkel commented Jul 19, 2023

NikolajBjorner commented Jul 22, 2023 • edited

NikolajBjorner commented Jul 22, 2023

NikolajBjorner commented Jul 22, 2023

NikolajBjorner commented Jul 22, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner commented Jul 22, 2023

hgvk94 commented Jul 26, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner Aug 1, 2023 • edited

Choose a reason for hiding this comment

NikolajBjorner Aug 1, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner commented Jul 22, 2023 •

edited

NikolajBjorner Aug 1, 2023 •

edited

NikolajBjorner Aug 1, 2023 •

edited