Skip to content

Commit 46ed247

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #404 from sosy-lab/update_bitwuzla_to_0.6.0
Update Bitwuzla to version 0.6.0
2 parents 8d3ab33 + d845056 commit 46ed247

File tree

4 files changed

+73
-8
lines changed

4 files changed

+73
-8
lines changed

‎lib/ivy.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,7 @@ SPDX-License-Identifier: Apache-2.0
167167
<dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
168168
<dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
169169
<dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
170-
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.4.0-g4dbf3b1f" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
170+
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-gab3db0e6" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
171171

172172
<!-- additional JavaSMT components with Solver Binaries -->
173173
<dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-734-g3732f7e08" conf="runtime-yices2->runtime; contrib->sources" />

‎lib/native/source/libbitwuzla/bitwuzla.i‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -291,6 +291,7 @@ namespace bitwuzla {
291291
/** Bitwuzla */
292292
%ignore Bitwuzla::Bitwuzla(const Options &options = Options());
293293
%ignore Bitwuzla::is_unsat_assumption (const Term &term);
294+
%ignore Bitwuzla::print_unsat_core(std::ostream &out, const std::string &format = "smt2") const;
294295
%ignore Bitwuzla::print_formula (std::ostream &out, const std::string &format="smt2") const;
295296
%extend Bitwuzla {
296297
std::string print_formula () {
@@ -308,7 +309,7 @@ namespace bitwuzla {
308309
namespace bitwuzla::parser {
309310
%ignore Parser::Parser(TermManager &tm, Options &options, const std::string &language, std::ostream *out);
310311
%ignore Parser::Parser(TermManager &tm, Options &options, std::ostream *out);
311-
312+
%ignore Parser::configure_auto_print_model(bool value);
312313
%ignore Parser::parse(const std::string &infile_name, std::istream &input, bool parse_only=false);
313314

314315
%exception {

‎lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ public final class Option {
2525
public final static Option VERBOSITY = new Option("VERBOSITY");
2626
public final static Option TIME_LIMIT_PER = new Option("TIME_LIMIT_PER");
2727
public final static Option MEMORY_LIMIT = new Option("MEMORY_LIMIT");
28+
public final static Option RELEVANT_TERMS = new Option("RELEVANT_TERMS");
2829
public final static Option BV_SOLVER = new Option("BV_SOLVER");
2930
public final static Option REWRITE_LEVEL = new Option("REWRITE_LEVEL");
3031
public final static Option SAT_SOLVER = new Option("SAT_SOLVER");
@@ -38,13 +39,28 @@ public final class Option {
3839
public final static Option PROP_PROB_USE_INV_VALUE = new Option("PROP_PROB_USE_INV_VALUE");
3940
public final static Option PROP_SEXT = new Option("PROP_SEXT");
4041
public final static Option PROP_NORMALIZE = new Option("PROP_NORMALIZE");
42+
public final static Option ABSTRACTION = new Option("ABSTRACTION");
43+
public final static Option ABSTRACTION_BV_SIZE = new Option("ABSTRACTION_BV_SIZE");
44+
public final static Option ABSTRACTION_EAGER_REFINE = new Option("ABSTRACTION_EAGER_REFINE");
45+
public final static Option ABSTRACTION_VALUE_LIMIT = new Option("ABSTRACTION_VALUE_LIMIT");
46+
public final static Option ABSTRACTION_VALUE_ONLY = new Option("ABSTRACTION_VALUE_ONLY");
47+
public final static Option ABSTRACTION_ASSERT = new Option("ABSTRACTION_ASSERT");
48+
public final static Option ABSTRACTION_ASSERT_REFS = new Option("ABSTRACTION_ASSERT_REFS");
49+
public final static Option ABSTRACTION_INITIAL_LEMMAS = new Option("ABSTRACTION_INITIAL_LEMMAS");
50+
public final static Option ABSTRACTION_INC_BITBLAST = new Option("ABSTRACTION_INC_BITBLAST");
51+
public final static Option ABSTRACTION_BV_ADD = new Option("ABSTRACTION_BV_ADD");
52+
public final static Option ABSTRACTION_BV_MUL = new Option("ABSTRACTION_BV_MUL");
53+
public final static Option ABSTRACTION_BV_UDIV = new Option("ABSTRACTION_BV_UDIV");
54+
public final static Option ABSTRACTION_BV_UREM = new Option("ABSTRACTION_BV_UREM");
55+
public final static Option ABSTRACTION_EQUAL = new Option("ABSTRACTION_EQUAL");
56+
public final static Option ABSTRACTION_ITE = new Option("ABSTRACTION_ITE");
4157
public final static Option PREPROCESS = new Option("PREPROCESS");
4258
public final static Option PP_CONTRADICTING_ANDS = new Option("PP_CONTRADICTING_ANDS");
4359
public final static Option PP_ELIM_BV_EXTRACTS = new Option("PP_ELIM_BV_EXTRACTS");
60+
public final static Option PP_ELIM_BV_UDIV = new Option("PP_ELIM_BV_UDIV");
4461
public final static Option PP_EMBEDDED_CONSTR = new Option("PP_EMBEDDED_CONSTR");
4562
public final static Option PP_FLATTEN_AND = new Option("PP_FLATTEN_AND");
4663
public final static Option PP_NORMALIZE = new Option("PP_NORMALIZE");
47-
public final static Option PP_NORMALIZE_SHARE_AWARE = new Option("PP_NORMALIZE_SHARE_AWARE");
4864
public final static Option PP_SKELETON_PREPROC = new Option("PP_SKELETON_PREPROC");
4965
public final static Option PP_VARIABLE_SUBST = new Option("PP_VARIABLE_SUBST");
5066
public final static Option PP_VARIABLE_SUBST_NORM_EQ = new Option("PP_VARIABLE_SUBST_NORM_EQ");
@@ -90,7 +106,7 @@ private Option(String swigName, Option swigEnum) {
90106
swigNext = this.swigValue+1;
91107
}
92108

93-
private static Option[] swigValues = { LOGLEVEL, PRODUCE_MODELS, PRODUCE_UNSAT_ASSUMPTIONS, PRODUCE_UNSAT_CORES, SEED, VERBOSITY, TIME_LIMIT_PER, MEMORY_LIMIT, BV_SOLVER, REWRITE_LEVEL, SAT_SOLVER, PROP_CONST_BITS, PROP_INFER_INEQ_BOUNDS, PROP_NPROPS, PROP_NUPDATES, PROP_OPT_LT_CONCAT_SEXT, PROP_PATH_SEL, PROP_PROB_RANDOM_INPUT, PROP_PROB_USE_INV_VALUE, PROP_SEXT, PROP_NORMALIZE, PREPROCESS, PP_CONTRADICTING_ANDS, PP_ELIM_BV_EXTRACTS, PP_EMBEDDED_CONSTR, PP_FLATTEN_AND, PP_NORMALIZE, PP_NORMALIZE_SHARE_AWARE, PP_SKELETON_PREPROC, PP_VARIABLE_SUBST, PP_VARIABLE_SUBST_NORM_EQ, PP_VARIABLE_SUBST_NORM_DISEQ, PP_VARIABLE_SUBST_NORM_BV_INEQ, DBG_RW_NODE_THRESH, DBG_PP_NODE_THRESH, DBG_CHECK_MODEL, DBG_CHECK_UNSAT_CORE, NUM_OPTS };
109+
private static Option[] swigValues = { LOGLEVEL, PRODUCE_MODELS, PRODUCE_UNSAT_ASSUMPTIONS, PRODUCE_UNSAT_CORES, SEED, VERBOSITY, TIME_LIMIT_PER, MEMORY_LIMIT, RELEVANT_TERMS, BV_SOLVER, REWRITE_LEVEL, SAT_SOLVER, PROP_CONST_BITS, PROP_INFER_INEQ_BOUNDS, PROP_NPROPS, PROP_NUPDATES, PROP_OPT_LT_CONCAT_SEXT, PROP_PATH_SEL, PROP_PROB_RANDOM_INPUT, PROP_PROB_USE_INV_VALUE, PROP_SEXT, PROP_NORMALIZE, ABSTRACTION, ABSTRACTION_BV_SIZE, ABSTRACTION_EAGER_REFINE, ABSTRACTION_VALUE_LIMIT, ABSTRACTION_VALUE_ONLY, ABSTRACTION_ASSERT, ABSTRACTION_ASSERT_REFS, ABSTRACTION_INITIAL_LEMMAS, ABSTRACTION_INC_BITBLAST, ABSTRACTION_BV_ADD, ABSTRACTION_BV_MUL, ABSTRACTION_BV_UDIV, ABSTRACTION_BV_UREM, ABSTRACTION_EQUAL, ABSTRACTION_ITE, PREPROCESS, PP_CONTRADICTING_ANDS, PP_ELIM_BV_EXTRACTS, PP_ELIM_BV_UDIV, PP_EMBEDDED_CONSTR, PP_FLATTEN_AND, PP_NORMALIZE, PP_SKELETON_PREPROC, PP_VARIABLE_SUBST, PP_VARIABLE_SUBST_NORM_EQ, PP_VARIABLE_SUBST_NORM_DISEQ, PP_VARIABLE_SUBST_NORM_BV_INEQ, DBG_RW_NODE_THRESH, DBG_PP_NODE_THRESH, DBG_CHECK_MODEL, DBG_CHECK_UNSAT_CORE, NUM_OPTS };
94110
private static int swigNext = 0;
95111
private final int swigValue;
96112
private final String swigName;

‎src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java‎

Lines changed: 52 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,21 @@
88

99
package org.sosy_lab.java_smt.solvers.bitwuzla;
1010

11+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION;
12+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ASSERT;
13+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ASSERT_REFS;
14+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_ADD;
15+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_MUL;
16+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_SIZE;
17+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_UDIV;
18+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_UREM;
19+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_EAGER_REFINE;
20+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_EQUAL;
21+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_INC_BITBLAST;
22+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_INITIAL_LEMMAS;
23+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ITE;
24+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_VALUE_LIMIT;
25+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_VALUE_ONLY;
1126
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.BV_SOLVER;
1227
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_MODEL;
1328
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_UNSAT_CORE;
@@ -18,10 +33,10 @@
1833
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.NUM_OPTS;
1934
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_CONTRADICTING_ANDS;
2035
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_ELIM_BV_EXTRACTS;
36+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_ELIM_BV_UDIV;
2137
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_EMBEDDED_CONSTR;
2238
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_FLATTEN_AND;
2339
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_NORMALIZE;
24-
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_NORMALIZE_SHARE_AWARE;
2540
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_SKELETON_PREPROC;
2641
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_VARIABLE_SUBST;
2742
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_VARIABLE_SUBST_NORM_BV_INEQ;
@@ -41,6 +56,7 @@
4156
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_PROB_RANDOM_INPUT;
4257
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_PROB_USE_INV_VALUE;
4358
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_SEXT;
59+
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.RELEVANT_TERMS;
4460
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.REWRITE_LEVEL;
4561
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.SAT_SOLVER;
4662
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.SEED;
@@ -206,7 +222,7 @@ private static Options setFurtherOptions(Options pOptions, String pFurtherOption
206222
String optionValue = option.getValue();
207223
Option bitwuzlaOption = getBitwuzlaOptByString(optionName);
208224
try {
209-
if (pOptions.is_numeric(bitwuzlaOption)) {
225+
if (pOptions.is_numeric(bitwuzlaOption) || pOptions.is_bool(bitwuzlaOption)) {
210226
pOptions.set(bitwuzlaOption, Integer.parseInt(optionValue));
211227
} else {
212228
pOptions.set(bitwuzlaOption, option.getValue());
@@ -330,6 +346,8 @@ public static Option getBitwuzlaOptByString(String optionName) {
330346
return TIME_LIMIT_PER;
331347
case "MEMORY_LIMIT":
332348
return MEMORY_LIMIT;
349+
case "RELEVANT_TERMS":
350+
return RELEVANT_TERMS;
333351
case "BV_SOLVER":
334352
return BV_SOLVER;
335353
case "REWRITE_LEVEL":
@@ -356,20 +374,50 @@ public static Option getBitwuzlaOptByString(String optionName) {
356374
return PROP_SEXT;
357375
case "PROP_NORMALIZE":
358376
return PROP_NORMALIZE;
377+
case "ABSTRACTION":
378+
return ABSTRACTION;
379+
case "ABSTRACTION_BV_SIZE":
380+
return ABSTRACTION_BV_SIZE;
381+
case "ABSTRACTION_EAGER_REFINE":
382+
return ABSTRACTION_EAGER_REFINE;
383+
case "ABSTRACTION_VALUE_LIMIT":
384+
return ABSTRACTION_VALUE_LIMIT;
385+
case "ABSTRACTION_VALUE_ONLY":
386+
return ABSTRACTION_VALUE_ONLY;
387+
case "ABSTRACTION_ASSERT":
388+
return ABSTRACTION_ASSERT;
389+
case "ABSTRACTION_ASSERT_REFS":
390+
return ABSTRACTION_ASSERT_REFS;
391+
case "ABSTRACTION_INITIAL_LEMMAS":
392+
return ABSTRACTION_INITIAL_LEMMAS;
393+
case "ABSTRACTION_INC_BITBLAST":
394+
return ABSTRACTION_INC_BITBLAST;
395+
case "ABSTRACTION_BV_ADD":
396+
return ABSTRACTION_BV_ADD;
397+
case "ABSTRACTION_BV_MUL":
398+
return ABSTRACTION_BV_MUL;
399+
case "ABSTRACTION_BV_UDIV":
400+
return ABSTRACTION_BV_UDIV;
401+
case "ABSTRACTION_BV_UREM":
402+
return ABSTRACTION_BV_UREM;
403+
case "ABSTRACTION_EQUAL":
404+
return ABSTRACTION_EQUAL;
405+
case "ABSTRACTION_ITE":
406+
return ABSTRACTION_ITE;
359407
case "PREPROCESS":
360408
return PREPROCESS;
361409
case "PP_CONTRADICTING_ANDS":
362410
return PP_CONTRADICTING_ANDS;
363411
case "PP_ELIM_BV_EXTRACTS":
364412
return PP_ELIM_BV_EXTRACTS;
413+
case "PP_ELIM_BV_UDIV":
414+
return PP_ELIM_BV_UDIV;
365415
case "PP_EMBEDDED_CONSTR":
366416
return PP_EMBEDDED_CONSTR;
367417
case "PP_FLATTEN_AND":
368418
return PP_FLATTEN_AND;
369419
case "PP_NORMALIZE":
370420
return PP_NORMALIZE;
371-
case "PP_NORMALIZE_SHARE_AWARE":
372-
return PP_NORMALIZE_SHARE_AWARE;
373421
case "PP_SKELETON_PREPROC":
374422
return PP_SKELETON_PREPROC;
375423
case "PP_VARIABLE_SUBST":

0 commit comments

Comments
 (0)