Skip to content

Update Bitwuzla to version 0.6.0 #404

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 27, 2024
Merged

Update Bitwuzla to version 0.6.0 #404

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7968802
Bitwuzla: Update Bitwuzla to version 0.6.0
daniel-raffler Oct 24, 2024
71f2528
Bitwuzla: Fix handling of boolean options that are passed on to Bitwu…
daniel-raffler Oct 24, 2024
d845056
Bitwuzla: use the exact release version 0.6.0.
kfriedberger Oct 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion lib/ivy.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ SPDX-License-Identifier: Apache-2.0
<dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
<dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
<dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.4.0-g4dbf3b1f" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-gab3db0e6" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>

<!-- additional JavaSMT components with Solver Binaries -->
<dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-734-g3732f7e08" conf="runtime-yices2->runtime; contrib->sources" />
Expand Down
3 changes: 2 additions & 1 deletion lib/native/source/libbitwuzla/bitwuzla.i
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,6 +291,7 @@ namespace bitwuzla {
/** Bitwuzla */
%ignore Bitwuzla::Bitwuzla(const Options &options = Options());
%ignore Bitwuzla::is_unsat_assumption (const Term &term);
%ignore Bitwuzla::print_unsat_core(std::ostream &out, const std::string &format = "smt2") const;
%ignore Bitwuzla::print_formula (std::ostream &out, const std::string &format="smt2") const;
%extend Bitwuzla {
std::string print_formula () {
Expand All @@ -308,7 +309,7 @@ namespace bitwuzla {
namespace bitwuzla::parser {
%ignore Parser::Parser(TermManager &tm, Options &options, const std::string &language, std::ostream *out);
%ignore Parser::Parser(TermManager &tm, Options &options, std::ostream *out);

%ignore Parser::configure_auto_print_model(bool value);
%ignore Parser::parse(const std::string &infile_name, std::istream &input, bool parse_only=false);

%exception {
Expand Down
20 changes: 18 additions & 2 deletions lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ public final class Option {
public final static Option VERBOSITY = new Option("VERBOSITY");
public final static Option TIME_LIMIT_PER = new Option("TIME_LIMIT_PER");
public final static Option MEMORY_LIMIT = new Option("MEMORY_LIMIT");
public final static Option RELEVANT_TERMS = new Option("RELEVANT_TERMS");
public final static Option BV_SOLVER = new Option("BV_SOLVER");
public final static Option REWRITE_LEVEL = new Option("REWRITE_LEVEL");
public final static Option SAT_SOLVER = new Option("SAT_SOLVER");
Expand All @@ -38,13 +39,28 @@ public final class Option {
public final static Option PROP_PROB_USE_INV_VALUE = new Option("PROP_PROB_USE_INV_VALUE");
public final static Option PROP_SEXT = new Option("PROP_SEXT");
public final static Option PROP_NORMALIZE = new Option("PROP_NORMALIZE");
public final static Option ABSTRACTION = new Option("ABSTRACTION");
public final static Option ABSTRACTION_BV_SIZE = new Option("ABSTRACTION_BV_SIZE");
public final static Option ABSTRACTION_EAGER_REFINE = new Option("ABSTRACTION_EAGER_REFINE");
public final static Option ABSTRACTION_VALUE_LIMIT = new Option("ABSTRACTION_VALUE_LIMIT");
public final static Option ABSTRACTION_VALUE_ONLY = new Option("ABSTRACTION_VALUE_ONLY");
public final static Option ABSTRACTION_ASSERT = new Option("ABSTRACTION_ASSERT");
public final static Option ABSTRACTION_ASSERT_REFS = new Option("ABSTRACTION_ASSERT_REFS");
public final static Option ABSTRACTION_INITIAL_LEMMAS = new Option("ABSTRACTION_INITIAL_LEMMAS");
public final static Option ABSTRACTION_INC_BITBLAST = new Option("ABSTRACTION_INC_BITBLAST");
public final static Option ABSTRACTION_BV_ADD = new Option("ABSTRACTION_BV_ADD");
public final static Option ABSTRACTION_BV_MUL = new Option("ABSTRACTION_BV_MUL");
public final static Option ABSTRACTION_BV_UDIV = new Option("ABSTRACTION_BV_UDIV");
public final static Option ABSTRACTION_BV_UREM = new Option("ABSTRACTION_BV_UREM");
public final static Option ABSTRACTION_EQUAL = new Option("ABSTRACTION_EQUAL");
public final static Option ABSTRACTION_ITE = new Option("ABSTRACTION_ITE");
public final static Option PREPROCESS = new Option("PREPROCESS");
public final static Option PP_CONTRADICTING_ANDS = new Option("PP_CONTRADICTING_ANDS");
public final static Option PP_ELIM_BV_EXTRACTS = new Option("PP_ELIM_BV_EXTRACTS");
public final static Option PP_ELIM_BV_UDIV = new Option("PP_ELIM_BV_UDIV");
public final static Option PP_EMBEDDED_CONSTR = new Option("PP_EMBEDDED_CONSTR");
public final static Option PP_FLATTEN_AND = new Option("PP_FLATTEN_AND");
public final static Option PP_NORMALIZE = new Option("PP_NORMALIZE");
public final static Option PP_NORMALIZE_SHARE_AWARE = new Option("PP_NORMALIZE_SHARE_AWARE");
public final static Option PP_SKELETON_PREPROC = new Option("PP_SKELETON_PREPROC");
public final static Option PP_VARIABLE_SUBST = new Option("PP_VARIABLE_SUBST");
public final static Option PP_VARIABLE_SUBST_NORM_EQ = new Option("PP_VARIABLE_SUBST_NORM_EQ");
Expand Down Expand Up @@ -90,7 +106,7 @@ private Option(String swigName, Option swigEnum) {
swigNext = this.swigValue+1;
}

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 };
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 };
private static int swigNext = 0;
private final int swigValue;
private final String swigName;
Expand Down
56 changes: 52 additions & 4 deletions src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,21 @@

package org.sosy_lab.java_smt.solvers.bitwuzla;

import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ASSERT;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ASSERT_REFS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_ADD;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_MUL;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_SIZE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_UDIV;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_BV_UREM;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_EAGER_REFINE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_EQUAL;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_INC_BITBLAST;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_INITIAL_LEMMAS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_ITE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_VALUE_LIMIT;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.ABSTRACTION_VALUE_ONLY;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.BV_SOLVER;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_MODEL;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.DBG_CHECK_UNSAT_CORE;
Expand All @@ -18,10 +33,10 @@
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.NUM_OPTS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_CONTRADICTING_ANDS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_ELIM_BV_EXTRACTS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_ELIM_BV_UDIV;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_EMBEDDED_CONSTR;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_FLATTEN_AND;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_NORMALIZE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_NORMALIZE_SHARE_AWARE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_SKELETON_PREPROC;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_VARIABLE_SUBST;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PP_VARIABLE_SUBST_NORM_BV_INEQ;
Expand All @@ -41,6 +56,7 @@
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_PROB_RANDOM_INPUT;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_PROB_USE_INV_VALUE;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.PROP_SEXT;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.RELEVANT_TERMS;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.REWRITE_LEVEL;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.SAT_SOLVER;
import static org.sosy_lab.java_smt.solvers.bitwuzla.api.Option.SEED;
Expand Down Expand Up @@ -206,7 +222,7 @@ private static Options setFurtherOptions(Options pOptions, String pFurtherOption
String optionValue = option.getValue();
Option bitwuzlaOption = getBitwuzlaOptByString(optionName);
try {
if (pOptions.is_numeric(bitwuzlaOption)) {
if (pOptions.is_numeric(bitwuzlaOption) || pOptions.is_bool(bitwuzlaOption)) {
pOptions.set(bitwuzlaOption, Integer.parseInt(optionValue));
} else {
pOptions.set(bitwuzlaOption, option.getValue());
Expand Down Expand Up @@ -330,6 +346,8 @@ public static Option getBitwuzlaOptByString(String optionName) {
return TIME_LIMIT_PER;
case "MEMORY_LIMIT":
return MEMORY_LIMIT;
case "RELEVANT_TERMS":
return RELEVANT_TERMS;
case "BV_SOLVER":
return BV_SOLVER;
case "REWRITE_LEVEL":
Expand All @@ -356,20 +374,50 @@ public static Option getBitwuzlaOptByString(String optionName) {
return PROP_SEXT;
case "PROP_NORMALIZE":
return PROP_NORMALIZE;
case "ABSTRACTION":
return ABSTRACTION;
case "ABSTRACTION_BV_SIZE":
return ABSTRACTION_BV_SIZE;
case "ABSTRACTION_EAGER_REFINE":
return ABSTRACTION_EAGER_REFINE;
case "ABSTRACTION_VALUE_LIMIT":
return ABSTRACTION_VALUE_LIMIT;
case "ABSTRACTION_VALUE_ONLY":
return ABSTRACTION_VALUE_ONLY;
case "ABSTRACTION_ASSERT":
return ABSTRACTION_ASSERT;
case "ABSTRACTION_ASSERT_REFS":
return ABSTRACTION_ASSERT_REFS;
case "ABSTRACTION_INITIAL_LEMMAS":
return ABSTRACTION_INITIAL_LEMMAS;
case "ABSTRACTION_INC_BITBLAST":
return ABSTRACTION_INC_BITBLAST;
case "ABSTRACTION_BV_ADD":
return ABSTRACTION_BV_ADD;
case "ABSTRACTION_BV_MUL":
return ABSTRACTION_BV_MUL;
case "ABSTRACTION_BV_UDIV":
return ABSTRACTION_BV_UDIV;
case "ABSTRACTION_BV_UREM":
return ABSTRACTION_BV_UREM;
case "ABSTRACTION_EQUAL":
return ABSTRACTION_EQUAL;
case "ABSTRACTION_ITE":
return ABSTRACTION_ITE;
case "PREPROCESS":
return PREPROCESS;
case "PP_CONTRADICTING_ANDS":
return PP_CONTRADICTING_ANDS;
case "PP_ELIM_BV_EXTRACTS":
return PP_ELIM_BV_EXTRACTS;
case "PP_ELIM_BV_UDIV":
return PP_ELIM_BV_UDIV;
case "PP_EMBEDDED_CONSTR":
return PP_EMBEDDED_CONSTR;
case "PP_FLATTEN_AND":
return PP_FLATTEN_AND;
case "PP_NORMALIZE":
return PP_NORMALIZE;
case "PP_NORMALIZE_SHARE_AWARE":
return PP_NORMALIZE_SHARE_AWARE;
case "PP_SKELETON_PREPROC":
return PP_SKELETON_PREPROC;
case "PP_VARIABLE_SUBST":
Expand Down