Skip to content

Commit

Permalink
Merge pull request #430 from SRI-CSL/mcsat-array-comb
Browse files Browse the repository at this point in the history 
MCSAT: Array + Nonlinear
  • Loading branch information
@disteph
disteph committed Mar 1, 2023
2 parents 6de3d6f + b087635 commit af766a4
Show file tree
Hide file tree
Showing 8 changed files with 8,173 additions and 8 deletions.
12 changes: 6 additions & 6 deletions src/api/context_config.c
View file
Expand Up @@ -189,9 +189,9 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
CTX_ARCH_EGFUNSPLX, // QF_ALIA
CTX_ARCH_EGFUNSPLX, // QF_ALRA
CTX_ARCH_EGFUNSPLX, // QF_ALIRA
-1, // QF_ANIA
-1, // QF_ANRA
-1, // QF_ANIRA
CTX_ARCH_MCSAT, // QF_ANIA
CTX_ARCH_MCSAT, // QF_ANRA
CTX_ARCH_MCSAT, // QF_ANIRA
CTX_ARCH_EGFUN, // QF_AUF
CTX_ARCH_EGBV, // QF_UFBV
CTX_ARCH_EGSPLX, // QF_UFIDL
Expand All @@ -206,9 +206,9 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
CTX_ARCH_EGFUNSPLX, // QF_AUFLIA
CTX_ARCH_EGFUNSPLX, // QF_AUFLRA
CTX_ARCH_EGFUNSPLX, // QF_AUFLIRA
-1, // QF_AUFNIA
-1, // QF_AUFNRA
-1, // QF_AUFNIRA
CTX_ARCH_MCSAT, // QF_AUFNIA
CTX_ARCH_MCSAT, // QF_AUFNRA
CTX_ARCH_MCSAT, // QF_AUFNIRA

CTX_ARCH_EGFUNSPLXBV, // ALL interpreted as QF_AUFLIRA + QF_BV
};
Expand Down
10 changes: 8 additions & 2 deletions src/mcsat/uf/uf_plugin.c
View file
Expand Up @@ -254,12 +254,16 @@ void uf_plugin_add_to_eq_graph(uf_plugin_t* uf, term_t t, bool record) {
t_desc = eq_term_desc(terms, t);
eq_graph_add_ifun_term(&uf->eq_graph, t, EQ_TERM, 2, t_desc->arg);
// remember array terms
if (is_function_term(terms, t_desc->arg[0])) {
if (is_function_term(terms, t_desc->arg[0]) &&
(term_kind(terms, t_desc->arg[0]) == UNINTERPRETED_TERM ||
term_kind(terms, t_desc->arg[0]) == UPDATE_TERM)) {
weq_graph_add_array_eq_term(&uf->weq_graph, t);
}
uint32_t i;
for (i = 0; i < 2; ++ i) {
if (is_function_term(terms, t_desc->arg[i])) {
if (is_function_term(terms, t_desc->arg[i]) &&
(term_kind(terms, t_desc->arg[i]) == UNINTERPRETED_TERM ||
term_kind(terms, t_desc->arg[i]) == UPDATE_TERM)) {
weq_graph_add_array_term(&uf->weq_graph, t_desc->arg[i]);
}
}
Expand Down Expand Up @@ -389,6 +393,8 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
t_desc = eq_term_desc(terms, t);
} else if (term_kind(terms, t) == BV_EQ_ATOM) {
t_desc = bveq_atom_desc(terms, t);
} else if (term_kind(terms, t) == ARITH_BINEQ_ATOM) {
t_desc = arith_bineq_atom_desc(terms, t);
} else {
assert(false);
}
Expand Down
40 changes: 40 additions & 0 deletions tests/regress/mcsat/avg20_true-unreach-call.i_9.smt2
View file
@@ -0,0 +1,40 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_ANIA)
(set-info :source "|
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2019 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (let ((.cse0 (select |v_#memory_int_110| |main_~#x~0.base|))) (= (select .cse0 (+ |main_~#x~0.offset| 64)) (select .cse0 (+ |main_~#x~0.offset| 72)))))
(check-sat)
(exit)
1 change: 1 addition & 0 deletions tests/regress/mcsat/avg20_true-unreach-call.i_9.smt2.gold
View file
@@ -0,0 +1 @@
sat

0 comments on commit af766a4

Please sign in to comment.