diff --git a/lib/ivy.xml b/lib/ivy.xml index ac4c58e555..fb434116d5 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -167,7 +167,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/source/libbitwuzla/bitwuzla.i b/lib/native/source/libbitwuzla/bitwuzla.i index 2703b9f16e..7aea00a86d 100644 --- a/lib/native/source/libbitwuzla/bitwuzla.i +++ b/lib/native/source/libbitwuzla/bitwuzla.i @@ -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 () { @@ -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 { diff --git a/lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java b/lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java index 247301cb24..68a14d7aae 100644 --- a/lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java +++ b/lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Option.java @@ -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"); @@ -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"); @@ -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; diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 2c9b9aed23..5d46c9a7ef 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -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; @@ -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; @@ -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; @@ -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()); @@ -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": @@ -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":