simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Optimisation for mcsat solver

Browse source
This commit is contained in:
Guillaume Bury 2016-09-23 13:30:51 +02:00
parent 41f1ec0e82
commit 88b8c9f895
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/mcsat/theory_mcsat.ml
View file

@ -52,8 +52,9 @@ let rec iter_aux f = function
f t
let iter_assignable f = function
| { Expr_smt.atom = Expr_smt.Pred p } ->
iter_aux f p;
| { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _ } } -> ()
| { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.App (_, _, l) } } ->
List.iter (iter_aux f) l;
| { Expr_smt.atom = Expr_smt.Equal (a, b) } ->
iter_aux f a; iter_aux f b