diff --git a/counting-examples/counting-with-ites.smt2 b/counting-examples/counting-with-ites.smt2 new file mode 100644 index 000000000..c172f5743 --- /dev/null +++ b/counting-examples/counting-with-ites.smt2 @@ -0,0 +1,14 @@ +;if (b1) { x = rho_1; } else if (b2) { x = rho_2; } else {x = rho_3; } +(set-option :count-models true) +(set-logic QF_BV) + +(declare-fun b1 () (_ BitVec 1)) +(declare-fun b2 () (_ BitVec 1)) +(declare-fun rho_1 () (_ BitVec 32)) +(declare-fun rho_2 () (_ BitVec 32)) +(declare-fun rho_3 () (_ BitVec 32)) +(declare-fun x () (_ BitVec 32)) + +(assert (= (! x :named v1) (ite (= b1 #b1) rho_1 (ite (= b2 #b1) rho_2 rho_3)))) +(count-models v1) + diff --git a/counting-examples/format-suggestion.smt2 b/counting-examples/format-suggestion.smt2 new file mode 100644 index 000000000..06042ab51 --- /dev/null +++ b/counting-examples/format-suggestion.smt2 @@ -0,0 +1,30 @@ +(set-option :count-models true) +(set-option :print-clauses-file "./counts.cnf") +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) + +(declare-fun rho_1 () (_ BitVec 32)) +(declare-fun rho_2 () (_ BitVec 32)) + +(declare-fun phi_1 () Bool) +(declare-fun phi_2 () Bool) + +(declare-fun warehouseid () (_ BitVec 32)) +(declare-fun warehouseidGV () (_ BitVec 32)) + +(assert (= rho_1 (! warehouseid :named v))) +(assert (= rho_2 warehouseidGV)) + +; 0 <= warehouseid <= 9 +(assert + (= phi_1 (bvult warehouseid #b00000000000000000000000000001010))) + +; 0 <= warehouseidGV <= 9 +(assert + (= phi_2 (bvult warehouseidGV #b00000000000000000000000000001010))) + +(assert (and (= rho_1 rho_2) (and phi_1 phi_2))) + +(count-models v) +;(check-sat) +(exit) diff --git a/counting-examples/union-example.smt2 b/counting-examples/union-example.smt2 new file mode 100644 index 000000000..e0c5bfa1b --- /dev/null +++ b/counting-examples/union-example.smt2 @@ -0,0 +1,27 @@ +; Has 3'000'000 models + +(set-option :count-models true) +(set-option :print-clauses-file "./counts.cnf") + +(set-logic QF_BV) +(declare-fun rho_1 () (_ BitVec 32)) +(declare-fun rho_2 () (_ BitVec 32)) +(declare-fun phi_1 () Bool) +(declare-fun phi_2 () Bool) +(declare-fun fromId () (_ BitVec 32)) +(declare-fun toId () (_ BitVec 32)) + +(declare-fun test () (_ BitVec 32)) + +(assert (= rho_1 fromId)) +(assert (and (bvult #b00000000001011011100011010111111 rho_1) (bvult rho_1 #b00000000010110111000110110000001))) +(assert (= rho_2 toId)) +(assert (and (bvult #b00000000001011011100011010111111 rho_2) (bvult rho_2 #b00000000010110111000110110000001))) +(assert (= phi_1 (bvult fromId #b00000000010110111000110110000000))) +(assert (= phi_2 (bvult toId #b00000000010110111000110110000000))) +(assert (and phi_1 phi_2)) + +(assert (or (= (! test :named v1) rho_1) (= test rho_2))) + +(count-models v1) +(exit) diff --git a/examples/test-bv.cc b/examples/test-bv.cc index c0054052f..57cef3783 100644 --- a/examples/test-bv.cc +++ b/examples/test-bv.cc @@ -107,10 +107,8 @@ int main(int argc, char** argv) bbb.computeModel(); PTRef v = bbb.getValue(d); auto val = logic.pp(v); - char* bin; - opensmt::wordToBinary(atoi(val.c_str()), bin, bw); - printf("%s (%s)\n", val.c_str(), bin); - free(bin); + std::string bin = opensmt::wordToBinary(atoi(val.c_str()), bw); + printf("%s (%s)\n", val.c_str(), bin.c_str()); } else if (r == s_False) printf("unsat\n"); diff --git a/regression/QF_BV/bar.smt2.expected.out b/regression/QF_BV/bar.smt2.expected.out index a4cf0f18f..d05c536c0 100644 --- a/regression/QF_BV/bar.smt2.expected.out +++ b/regression/QF_BV/bar.smt2.expected.out @@ -1 +1 @@ -At line 4: syntax error, unexpected TK_SYM, expecting TK_NUM or ')' +At line 4: syntax error, unexpected TK_NUM, expecting ')' diff --git a/regression/QF_BV/bvnor.smt2.expected.out b/regression/QF_BV/bvnor.smt2.expected.out index 1d5d6d798..08bc2390f 100644 --- a/regression/QF_BV/bvnor.smt2.expected.out +++ b/regression/QF_BV/bvnor.smt2.expected.out @@ -1,8 +1 @@ -(error "unknown logic QF_BV") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: assert") - -(error "Illegal command before set-logic: check-sat") - +At line 9: syntax error, unexpected TK_NUM, expecting ')' diff --git a/regression/QF_BV/edit.smt2.expected.out b/regression/QF_BV/edit.smt2.expected.out index 1d5d6d798..3f65111b0 100644 --- a/regression/QF_BV/edit.smt2.expected.out +++ b/regression/QF_BV/edit.smt2.expected.out @@ -1,8 +1 @@ -(error "unknown logic QF_BV") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: assert") - -(error "Illegal command before set-logic: check-sat") - +unsat diff --git a/regression/QF_BV/setlogic.smt2.expected.out b/regression/QF_BV/setlogic.smt2.expected.out index 4e3bfccf7..e69de29bb 100644 --- a/regression/QF_BV/setlogic.smt2.expected.out +++ b/regression/QF_BV/setlogic.smt2.expected.out @@ -1,2 +0,0 @@ -(error "unknown logic QF_BV") - diff --git a/regression/generic/define-fun.smt2.expected.out b/regression/generic/define-fun.smt2.expected.out index e3ed1dd7d..f6cd39048 100644 --- a/regression/generic/define-fun.smt2.expected.out +++ b/regression/generic/define-fun.smt2.expected.out @@ -1,2 +1 @@ -(error "Illegal command before set-logic: define-fun") - +At line 1: syntax error, unexpected TK_NUM, expecting ')' diff --git a/regression/generic/simple.smt2.expected.out b/regression/generic/simple.smt2.expected.out index 9bacc2199..09cae7127 100644 --- a/regression/generic/simple.smt2.expected.out +++ b/regression/generic/simple.smt2.expected.out @@ -1,14 +1 @@ -(error "unknown logic AB_CD") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: declare-fun") - -(error "Illegal command before set-logic: declare-fun") - +At line 22: syntax error, unexpected TK_NUM, expecting ')' diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index dafc4afd8..8113cae65 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -22,11 +22,13 @@ set(PRIVATE_SOURCES_TO_ADD "${CMAKE_CURRENT_SOURCE_DIR}/MainSolver.cc" "${CMAKE_CURRENT_SOURCE_DIR}/PartitionManager.cc" "${CMAKE_CURRENT_SOURCE_DIR}/Interpret.cc" + "${CMAKE_CURRENT_SOURCE_DIR}/MainCounter.cc" ) set(PUBLIC_SOURCES_TO_ADD "${CMAKE_CURRENT_SOURCE_DIR}/MainSolver.h" "${CMAKE_CURRENT_SOURCE_DIR}/PartitionManager.h" + "${CMAKE_CURRENT_SOURCE_DIR}/MainCounter.h" "${CMAKE_CURRENT_SOURCE_DIR}/smt2tokens.h" "${CMAKE_CURRENT_SOURCE_DIR}/Interpret.h" "${CMAKE_CURRENT_SOURCE_DIR}/Opensmt.cc" diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc index b9af8f4c3..5ffa8479f 100644 --- a/src/api/Interpret.cc +++ b/src/api/Interpret.cc @@ -29,6 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include "ArithLogic.h" #include "LogicFactory.h" #include "Substitutor.h" +#include "MainCounter.h" #include #include @@ -285,6 +286,19 @@ void Interpret::interp(ASTNode& n) { } break; } + case t_countmodels: { + if (config.count_models()) { + if (isInitialized()) { + countModels(n); + } else { + notify_formatted(true, "Illegal command before set-logic: count-models"); + } + } else { + notify_formatted(true, + "Option to count models not set. Ignoring command. "); + } + break; + } case t_getassignment: { if (isInitialized()) { getAssignment(); @@ -1194,8 +1208,8 @@ SRef Interpret::sortFromASTNode(ASTNode const & node) const { bool known = logic->peekSortSymbol(symbol, symRef); if (not known) { return SRef_Undef; } return logic->getSort(symRef, {}); - } else { - assert(type == LID_T and node.children and not node.children->empty()); + } else if (node.getType() == LID_T) { + assert(node.children and not node.children->empty()); ASTNode const & name = **(node.children->begin()); SortSymbol symbol(name.getValue(), node.children->size() - 1); SSymRef symRef; @@ -1208,20 +1222,48 @@ SRef Interpret::sortFromASTNode(ASTNode const & node) const { args.push(argSortRef); } return logic->getSort(symRef, std::move(args)); + } else if (node.getType() == IDX_T) { + assert(node.children and not node.children->empty()); + assert(node.children->size() == 2); + ASTNode const * symNode = (*node.children)[0]; + ASTNode const * idxNode = (*node.children)[1]; + assert(symNode->getType() == SYM_T); + assert(idxNode->getType() == NUM_T); + SRef typeSort = sortFromASTNode(*symNode); + return logic->getIndexedSort(typeSort, idxNode->getValue()); } - assert(type == LID_T and node.children and not node.children->empty()); - ASTNode const & name = **(node.children->begin()); - SortSymbol symbol(name.getValue(), node.children->size() - 1); - SSymRef symRef; - bool known = logic->peekSortSymbol(symbol, symRef); - if (not known) { return SRef_Undef; } - vec args; - for (auto it = node.children->begin() + 1; it != node.children->end(); ++it) { - SRef argSortRef = sortFromASTNode(**it); - if (argSortRef == SRef_Undef) { return SRef_Undef; } - args.push(argSortRef); + assert(false); + throw OsmtAstException("Unknown node type"); + return SRef_Undef; +} + +void Interpret::countModels(ASTNode const & n) +{ + MainCounter & counter = static_cast(*main_solver); + auto exps = *n.children; + vec modelTerms; + LetRecords letRecords; + letRecords.pushFrame(); + for (auto key : nameToTerm.getKeys()) { + letRecords.addBinding(key, nameToTerm[key]); + } + + for (auto e : exps) { + ASTNode const & c = *e; + modelTerms.push(parseTerm(c, letRecords)); + } + + letRecords.popFrame(); + + std::string printedTerms; + for (int i = 0; i < modelTerms.size(); i++) { + printedTerms += logic->pp(modelTerms[i]) + std::string(i == modelTerms.size()-1 ? "" : " "); } - return logic->getSort(symRef, std::move(args)); + std::string outString = "; Counting models for terms: " + printedTerms; + notify_formatted(false, outString.c_str()); + + counter.countModels(modelTerms); + } void Interpret::getInterpolants(const ASTNode& n) @@ -1315,8 +1357,44 @@ void Interpret::initializeLogic(opensmt::Logic_t logicType) { } std::unique_ptr Interpret::createMainSolver(const char* logic_name) { - return std::make_unique(*logic, config, std::string(logic_name) + " solver"); + /* if (config.sat_split_type() != spt_none) { + auto th = MainSolver::createTheory(*logic, config); + auto tm = std::make_unique(*logic); + auto thandler = new THandler(*th, *tm); + return std::make_unique(std::move(th), + std::move(tm), + std::unique_ptr(thandler), + MainSplitter::createInnerSolver(config, *thandler), + *logic, + config, + std::string(logic_name) + + " splitter"); + } else if (config.count_models()) { + auto theory = MainSolver::createTheory(*logic, config); + auto termMapper = std::unique_ptr(new TermMapper(*logic)); + auto thandler = new THandler(*theory, *termMapper); + return std::make_unique(std::move(theory), + std::move(termMapper), + std::unique_ptr(thandler), + MainCounter::createInnerSolver(config, *thandler), + *logic, + config, + std::string(logic_name) + " counter"); + } else { + return std::make_unique(*logic, config, std::string(logic_name) + " solver"); + } */ + if (config.count_models()) { + auto theory = MainSolver::createTheory(*logic, config); + auto termMapper = std::unique_ptr(new TermMapper(*logic)); + auto thandler = new THandler(*theory, *termMapper); + return std::make_unique(std::move(theory), + std::move(termMapper), + std::unique_ptr(thandler), + MainCounter::createInnerSolver(config, *thandler), + *logic, + config, + std::string(logic_name) + " counter"); + } else { + return std::make_unique(*logic, config, std::string(logic_name) + " solver"); + } } - - - diff --git a/src/api/Interpret.h b/src/api/Interpret.h index 05cdaf83e..bc22b0d63 100644 --- a/src/api/Interpret.h +++ b/src/api/Interpret.h @@ -128,6 +128,14 @@ class LetRecords { } }; + +class OsmtAstException : public std::runtime_error { +public: + OsmtAstException(const std::string & msg) : std::runtime_error(msg) {} + OsmtAstException(const char * msg) : std::runtime_error(msg) {} +}; + + class Interpret { protected: SMTConfig & config; @@ -174,6 +182,8 @@ class Interpret { void getInterpolants(const ASTNode& n); void interp (ASTNode& n); + void countModels(ASTNode const & n); + void notify_formatted(bool error, const char* s, ...); void notify_success(); void comment_formatted(const char* s, ...) const; diff --git a/src/api/MainCounter.cc b/src/api/MainCounter.cc new file mode 100644 index 000000000..d5f37c6e6 --- /dev/null +++ b/src/api/MainCounter.cc @@ -0,0 +1,16 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#include "MainCounter.h" + +void MainCounter::countModels(vec const & terms) { + initialize(); + sstat rval = MainSolver::simplifyFormulas(); + assert(rval == s_Undef); + (void)rval; + auto & modelCounter = dynamic_cast(*smt_solver); + modelCounter.count(terms); +} diff --git a/src/api/MainCounter.h b/src/api/MainCounter.h new file mode 100644 index 000000000..d998f6c6a --- /dev/null +++ b/src/api/MainCounter.h @@ -0,0 +1,31 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#ifndef OPENSMT_MAINCOUNTER_H +#define OPENSMT_MAINCOUNTER_H + +#include "MainSolver.h" +#include "ClausePrinter.h" + +class MainCounter : public MainSolver { +public: + MainCounter(std::unique_ptr t, std::unique_ptr tm, std::unique_ptr th, + std::unique_ptr ss, Logic & logic, SMTConfig & config, std::string && name) + : MainSolver(std::move(t), + std::move(tm), + std::move(th), + std::move(ss), + logic, + config, + std::move(name)) + {} + static std::unique_ptr createInnerSolver(SMTConfig & config, THandler & thandler) { return std::make_unique(config, thandler); } + + void countModels(vec const & terms); +}; + + +#endif //OPENSMT_MAINCOUNTER_H diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 2d1fd082b..8ce04a59d 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -37,6 +37,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include "IteHandler.h" #include "RDLTHandler.h" #include "IDLTHandler.h" +#include "FSBVTheory.h" + #include #include @@ -311,13 +313,13 @@ sstat MainSolver::solve() return status; } -std::unique_ptr MainSolver::createInnerSolver(SMTConfig & config, THandler & thandler) { +std::unique_ptr MainSolver::createInnerSolver(SMTConfig & config, THandler & thandler) { if (config.sat_pure_lookahead()) { return std::make_unique(config, thandler); } else if (config.use_ghost_vars()) { return std::make_unique(config, thandler); } else if (config.sat_picky()) { - return std::make_unique(config, thandler); + return std::make_unique(config, thandler); } else { return std::make_unique(config, thandler); } @@ -340,12 +342,18 @@ std::unique_ptr MainSolver::createTheory(Logic & logic, SMTConfig & conf break; } case Logic_t::QF_CUF: - case Logic_t::QF_BV: { BVLogic & bvLogic = dynamic_cast(logic); theory = new CUFTheory(config, bvLogic); break; } + case Logic_t::QF_BV: + { + FSBVLogic & bvLogic = dynamic_cast(logic); + theory = new FSBVTheory(config, bvLogic); + break; + } + case Logic_t::QF_LRA: { ArithLogic & lraLogic = dynamic_cast(logic); diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 87de795f0..0b27dbcda 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -100,7 +100,7 @@ class MainSolver std::unique_ptr theory; std::unique_ptr term_mapper; std::unique_ptr thandler; - std::unique_ptr smt_solver; + std::unique_ptr smt_solver; Logic& logic; PartitionManager pmanager; SMTConfig& config; @@ -149,8 +149,7 @@ class MainSolver } } - static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); - + static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); public: @@ -164,7 +163,7 @@ class MainSolver pmanager(logic), config(conf), pfstore(getTheory().pfstore), - ts( config, logic, pmanager, *term_mapper, *smt_solver ), + ts(config, logic, pmanager, *term_mapper, *smt_solver), solver_name {std::move(name)}, check_called(0), status(s_Undef), @@ -177,7 +176,7 @@ class MainSolver } MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, - std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name) + std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name) : theory(std::move(th)), term_mapper(std::move(tm)), @@ -187,7 +186,7 @@ class MainSolver pmanager(logic), config(conf), pfstore(getTheory().pfstore), - ts( config, logic, pmanager, *term_mapper, *smt_solver ), + ts(config, logic, pmanager, *term_mapper, *smt_solver), solver_name {std::move(name)}, check_called(0), status(s_Undef), @@ -202,8 +201,8 @@ class MainSolver virtual ~MainSolver() = default; SMTConfig& getConfig() { return config; } - SimpSMTSolver& getSMTSolver() { return *smt_solver; } - SimpSMTSolver const & getSMTSolver() const { return *smt_solver; } + SMTSolver& getSMTSolver() { return *smt_solver; } + SMTSolver const & getSMTSolver() const { return *smt_solver; } THandler &getTHandler() { return *thandler; } Logic &getLogic() { return logic; } @@ -216,7 +215,7 @@ class MainSolver sstat insertFormula(PTRef root, char** msg); void insertFormula(PTRef fla); - void initialize() { ts.solver.initialize(); ts.initialize(); } + void initialize() { smt_solver->initialize(); ts.initialize(); } virtual sstat check(); // A wrapper for solve which simplifies the loaded formulas and initializes the solvers // Simplify frames (not yet simplified) until all are simplified or the instance is detected unsatisfiable. @@ -233,7 +232,7 @@ class MainSolver // Returns model of the last query (must be in satisfiable state) std::unique_ptr getModel(); - void stop() { ts.solver.stop = true; } + void stop() { smt_solver->setStop(); } // Returns interpolation context for the last query (must be in UNSAT state) std::unique_ptr getInterpolationContext(); diff --git a/src/api/Opensmt.h b/src/api/Opensmt.h index d4b2e05b4..09b6e36d7 100644 --- a/src/api/Opensmt.h +++ b/src/api/Opensmt.h @@ -54,7 +54,7 @@ class Opensmt return dynamic_cast(*logic); } MainSolver& getMainSolver() { return *mainSolver; } - SimpSMTSolver& getSolver() { return getMainSolver().getSMTSolver(); } + SMTSolver& getSolver() { return getMainSolver().getSMTSolver(); } private: std::unique_ptr config; std::unique_ptr logic; diff --git a/src/api/smt2tokens.h b/src/api/smt2tokens.h index 42aa1e683..39dbbf16d 100644 --- a/src/api/smt2tokens.h +++ b/src/api/smt2tokens.h @@ -66,12 +66,14 @@ namespace osmttokens { t_push, t_setlogic, t_getinterpolants, + t_countmodels, t_theory, t_writestate, t_readstate, t_simplify, t_let, - t_echo + t_echo, + t_idx, }; inline const std::unordered_set tokenNames = { "none", @@ -84,6 +86,7 @@ namespace osmttokens { "forall", "assert", "check-sat", + "count-models", "declare-sort", "define-sort", "declare-fun", @@ -143,12 +146,14 @@ namespace osmttokens { {t_push, "push"}, {t_setlogic, "set-logic"}, {t_getinterpolants, "get-interpolants"}, + {t_countmodels, "count-models"}, {t_theory, "theory"}, {t_writestate, "write-state"}, {t_readstate, "read-state"}, {t_simplify, "simplify"}, {t_let, "let"}, - {t_echo, "echo"} + {t_echo, "echo"}, + {t_idx, "_"}, }; struct smt2token { diff --git a/src/cnfizers/Cnfizer.cc b/src/cnfizers/Cnfizer.cc index 221679ba8..aa8ac8f5f 100644 --- a/src/cnfizers/Cnfizer.cc +++ b/src/cnfizers/Cnfizer.cc @@ -47,7 +47,7 @@ Cnfizer::Cnfizer ( SMTConfig &config_ , Logic &logic_ , PartitionManager &pmanager_ , TermMapper &tmap - , SimpSMTSolver &solver_ + , SMTSolver &solver_ ) : solver (solver_) , config (config_ ) @@ -102,7 +102,7 @@ Cnfizer::solve(vec& en_frames) assumps[j++] = assumps[i]; } assumps.shrink(i-j); - return solver.solve(assumps, !config.isIncremental(), config.isIncremental()); + return solver.solve(assumps); } diff --git a/src/cnfizers/Cnfizer.h b/src/cnfizers/Cnfizer.h index 0141f4c1b..905bee82c 100644 --- a/src/cnfizers/Cnfizer.h +++ b/src/cnfizers/Cnfizer.h @@ -34,7 +34,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include -class SimpSMTSolver; +class SMTSolver; class THandler; struct SMTConfig; @@ -44,7 +44,7 @@ struct SMTConfig; class Cnfizer { public: - SimpSMTSolver& solver; + SMTSolver& solver; protected: SMTConfig& config; Logic& logic; @@ -70,7 +70,7 @@ class Cnfizer , Logic& logic_ , PartitionManager& pmanager_ , TermMapper& tmap_ - , SimpSMTSolver& solver_ + , SMTSolver& solver_ ); diff --git a/src/cnfizers/Tseitin.h b/src/cnfizers/Tseitin.h index 14c3edbcb..4682eada2 100644 --- a/src/cnfizers/Tseitin.h +++ b/src/cnfizers/Tseitin.h @@ -38,7 +38,7 @@ class Tseitin : public Cnfizer , Logic& logic_ , PartitionManager &pmanager_ , TermMapper& tmap_ - , SimpSMTSolver& solver_ + , SMTSolver& solver_ ) : Cnfizer( config_ , logic_ diff --git a/src/common/NumberUtils.h b/src/common/NumberUtils.h index d56b98db0..8c4269d08 100644 --- a/src/common/NumberUtils.h +++ b/src/common/NumberUtils.h @@ -14,24 +14,15 @@ namespace opensmt { typedef mpz_class Integer; //PS. related to BV logic - void static inline wordToBinary(const opensmt::Integer x, char *&bin, const int width) { - bin = (char *) malloc(width + 1); - - int p = 0; - opensmt::Integer one = 1; - for (opensmt::Integer i = (one << (width - 1)); i > 0; i >>= 1) - bin[p++] = ((x & i) == i) ? '1' : '0'; - bin[p] = '\0'; - } - - void static inline wordToBinary(const unsigned x, char *&bin, const int width) { - bin = (char *) malloc(width + 1); - + template + static inline std::string wordToBinary(I const & x, int width) { + std::string bin; + bin.resize(width); int p = 0; - opensmt::Integer one = 1; + I one = 1; for (opensmt::Integer i = (one << (width - 1)); i > 0; i >>= 1) bin[p++] = ((x & i) == i) ? '1' : '0'; - bin[p] = '\0'; + return bin; } void static inline normalize(char *&rat, const char *flo, bool is_neg) { @@ -58,5 +49,7 @@ namespace opensmt { while ((2 << (n++)) != l); return n; } + + static inline bool isNumber(std::string const & n) { return not n.empty() and std::for_each(n.begin(), n.end(), [](char c) { return std::isdigit(c); }); } } #endif //OPENSMT_NUMBERUTILS_H diff --git a/src/logics/BVLogic.h b/src/logics/BVLogic.h index d4c310693..e818b3434 100644 --- a/src/logics/BVLogic.h +++ b/src/logics/BVLogic.h @@ -102,8 +102,8 @@ class BVLogic: public CUFLogic virtual std::string const getName() const override { return "QF_BV"; } // virtual PTRef insertTerm(SymRef sym, vec& terms, char** msg); - PTRef mkBVConst (const int c) { char* num; opensmt::wordToBinary(c, num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the int c to binary - PTRef mkBVConst (const char* c) { char* num; opensmt::wordToBinary(opensmt::Integer(c), num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the string c to binary + PTRef mkBVConst (const int c) { return Logic::mkConst(sort_BVNUM, opensmt::wordToBinary(c, getBitWidth()).c_str()); } // Convert the int c to binary + PTRef mkBVConst (const char* c) { return Logic::mkConst(sort_BVNUM, opensmt::wordToBinary(opensmt::Integer(c), getBitWidth()).c_str()); } // Convert the string c to binary virtual PTRef mkBVNumVar (const char* name) { return mkVar(sort_BVNUM, name); } virtual bool isBuiltinSortSym(SSymRef ssr) const override { return (ssr == sort_store.getSortSym(sort_BVNUM)) || CUFLogic::isBuiltinSortSym(ssr); } virtual bool isBuiltinSort(SRef sr) const override { return (sr == sort_BVNUM) /*|| (sr == sort_BVSTR)*/ || CUFLogic::isBuiltinSort(sr); } diff --git a/src/logics/BitBlasterRewriter.cc b/src/logics/BitBlasterRewriter.cc new file mode 100644 index 000000000..2be3b9657 --- /dev/null +++ b/src/logics/BitBlasterRewriter.cc @@ -0,0 +1,578 @@ +/* + * Copyright (c) 2008 - 2012, Roberto Bruttomesso + * Copyright (c) 2012 - 2022, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#include "BitBlasterRewriter.h" +#include + +PTRef BitBlasterConfig::bbEquality(PTRef eq_tr) { + Pterm & eq = logic.getPterm(eq_tr); + BVRef lhs = store[eq[0]]; + BVRef rhs = store[eq[1]]; + + assert(store[lhs].size() == store[rhs].size()); + int size = store[lhs].size(); + // Produce the result + vec result_args; + result_args.capacity(size); + + for (int i = 0; i < size; ++ i) { + result_args.push(logic.mkEq(store[lhs][i], store[rhs][i])); + } + PTRef res = logic.mkAnd(result_args); + return res; +} + +PTRef BitBlasterConfig::bbDisequality(PTRef diseq_tr) { + Pterm & diseq = logic.getPterm(diseq_tr); + vec args; + args.capacity((diseq.size() + (diseq.size()-1))/2); + for (int i = 0; i < diseq.size(); i++) { + for (int j = i+1; j < diseq.size(); j++) { + args.push(logic.mkNot(bbEquality(logic.mkEq(diseq[i], diseq[j])))); + } + } + return logic.mkAnd(args); +} + +PTRef BitBlasterConfig::bbUlt(PTRef ult_tr) { + Pterm const & ult = logic.getPterm(ult_tr); + BVRef lhs = store[ult[0]]; + BVRef rhs = store[ult[1]]; + assert(store[lhs].size() == store[rhs].size() and store[lhs].size() > 0); + PTRef isLessThanUpToHere = PTRef_Undef; + for (int i = 0; i < store[lhs].size(); i++) { + // ~lhs[i] & rhs[i] + PTRef bitLessThan = logic.mkAnd(logic.mkNot(store[lhs][i]), store[rhs][i]); + // Produce l[i] <-> r[i] + PTRef bitEq = logic.mkEq(store[lhs][i], store[rhs][i]); + isLessThanUpToHere = (i > 0) ? logic.mkOr(bitLessThan, logic.mkAnd(bitEq, isLessThanUpToHere)) : bitLessThan; + } + return isLessThanUpToHere; +} + +void BitBlasterConfig::bbConstant(PTRef tr) { + auto bw = logic.getRetSortBitWidth(tr); + + vec asgns; + asgns.growTo(bw, logic.getTerm_false()); + + if (logic.isTrue(tr)) { + asgns[0] = logic.getTerm_true(); + } else if (logic.isFalse(tr)) { + ; // Already ok + } else { + const std::string value = logic.getSymName(tr); + assert((value.length()-2) == static_cast(bw)); // in binary + for (unsigned int i = 0 ; i < bw; ++i) { + unsigned int idx = bw - i + 1; + assert(value[idx] == '1' or value[idx] == '0'); + asgns[i] = value[idx] == '1' ? logic.getTerm_true() : logic.getTerm_false(); + } + } + store.newBvector(asgns, tr); +} + +void BitBlasterConfig::bbMul(PTRef mul_tr) { + + Pterm const & mul = logic.getPterm(mul_tr); + BVRef a = store[mul[0]]; + BVRef b = store[mul[1]]; + assert(store[a].size() == store[b].size()); + int size = store[a].size(); + + // Allocate new result + vec acc; + acc.capacity(size); + vec result; + result.capacity(size); + + // Compute term a_{i-1}*b_{j-1} ... a_0*b_0 + for (int i = 0; i < size; ++ i) { + acc[i] = logic.mkAnd(store[b][0], store[a][i]); + } + // Multi-arity adder + for (int i = 1; i < size; i ++) { + vec addend; + addend.capacity(size); + // Push trailing 0s + for (int j = 0; j < i; ++ j) { + addend.push(logic.getTerm_false()); + } + // Compute term a_{i-1}*b_i ... a_0*b_i 0 ... 0 + for (int j = 0; j < size - i; j++) { + addend.push(logic.mkAnd(store[b][i], store[a][j])); + } + + // Accumulate computed term + PTRef carry = PTRef_Undef; + + for (int k = 0; k < size ; k++) { + PTRef bit_1 = acc[k]; + PTRef bit_2 = addend[k]; + assert(bit_1 != PTRef_Undef); + assert(bit_2 != PTRef_Undef); + + PTRef xor_1 = logic.mkXor(bit_1, bit_2); + PTRef and_1 = logic.mkAnd(bit_1, bit_2); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + if (i == size - 1) + result.push(xor_2); + else + acc[k] = xor_2; + } else { + carry = and_1; + if (i == size - 1) + result.push(xor_1); + else + acc[k] = xor_1; + } + } + } + store.newBvector(result, mul_tr); +} + +void BitBlasterConfig::bbVar(PTRef var_tr) { + // Allocate new result + auto size = static_cast(logic.getRetSortBitWidth(var_tr)); + vec vars; + vars.capacity(size); + + int targetLength = static_cast(std::log10(size))+1; + auto zeroPadNumber = [](int number, unsigned long targetLength) { + std::string s = std::to_string(number); + return std::string(targetLength - std::min(targetLength, s.length()), '0') + s; + }; + + for (int i = 0; i < size; ++i) { + std::string bitName = BitVectorVarPrefix + std::to_string(var_tr.x) + '_' + zeroPadNumber(i, targetLength); + vars.push(logic.mkBoolVar(bitName.c_str())); + } + store.newBvector(vars, var_tr); +} + +void BitBlasterConfig::bbAdd(PTRef add_tr) { + Pterm const & add = logic.getPterm(add_tr); + BVRef a = store[add[0]]; + BVRef b = store[add[1]]; + + assert(store[a].size() == store[b].size()); + int size = store[a].size(); // the bit width + + // Allocate new result + vec result; + + PTRef carry = PTRef_Undef; + + for (int i = 0 ; i < size; i++) { + PTRef bit_1 = store[a][i]; + PTRef bit_2 = store[b][i]; + assert(bit_1 != PTRef_Undef); + assert(bit_2 != PTRef_Undef); + + PTRef xor_1 = logic.mkXor(bit_1, bit_2); + PTRef and_1 = logic.mkAnd(bit_1, bit_2); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + result.push(xor_2); + } else { + carry = and_1; + result.push(xor_1); + } + } + + // Save result and return + store.newBvector(result, add_tr); +} + +void BitBlasterConfig::bbConcat(PTRef concat_tr) { + Pterm const & concat = logic.getPterm(concat_tr); + BVRef a = store[concat[0]]; + BVRef b = store[concat[1]]; + auto size = store[a].size() + store[b].size(); + assert(logic.getRetSortBitWidth(concat_tr) == static_cast(size)); + vec result; + result.capacity(size); + for (PTRef tr : store[b]) { + result.push(tr); + } + for (PTRef tr : store[a]) { + result.push(tr); + } + // Save result and return + store.newBvector(result, concat_tr); +} + +void BitBlasterConfig::bbFlip(PTRef flip_tr) { + BVRef a = store[logic.getPterm(flip_tr)[0]]; + auto size = store[a].size(); + vec result; + result.capacity(size); + for (PTRef tr : store[a]) { + result.push(logic.mkNot(tr)); + } + // Save result and return + store.newBvector(result, flip_tr); +} + +void BitBlasterConfig::bbNot(PTRef not_tr) { + BVRef a = store[logic.getPterm(not_tr)[0]]; + auto size = store[a].size(); + vec result; + result.growTo(size, logic.getTerm_false()); + vec args; + for (PTRef tr : store[a]) { + args.push(tr); + } + result[0] = logic.mkNot(logic.mkOr(args)); + // Save result and return + store.newBvector(result, not_tr); +} + +void BitBlasterConfig::bbAnd(PTRef and_tr) { + Pterm const & and_ = logic.getPterm(and_tr); + BVRef a = store[and_[0]]; + BVRef b = store[and_[1]]; + assert(store[a].size() == store[b].size()); + auto size = store[a].size(); + vec result; + result.capacity(size); + for (auto i = 0; i < size; i++) { + result.push(logic.mkAnd(store[a][i], store[b][i])); + } + store.newBvector(result, and_tr); +} + +void BitBlasterConfig::bbOr(PTRef and_tr) { + Pterm const & and_ = logic.getPterm(and_tr); + BVRef a = store[and_[0]]; + BVRef b = store[and_[1]]; + assert(store[a].size() == store[b].size()); + auto size = store[a].size(); + vec result; + result.capacity(size); + for (auto i = 0; i < size; i++) { + result.push(logic.mkOr(store[a][i], store[b][i])); + } + store.newBvector(result, and_tr); +} + +void BitBlasterConfig::bbUdiv(PTRef div_tr) { + Pterm const & div = logic.getPterm(div_tr); + BVRef dividend = store[div[0]]; + BVRef divisor = store[div[1]]; + assert(store[divisor].size() == store[dividend].size()); + + auto size = store[divisor].size(); + vec result; + result.growTo(size); + + vec minuend; + minuend.capacity(size); + + // Initialize minuend as 0..0 q[n-1] + minuend.push(store[dividend][size - 1]); + for (int i = 1; i < size; i ++) { + minuend.push(logic.getTerm_false()); + } + + // Main loop + for (int i = size - 1; i >= 0; i --) { + // Compute result[ i ] = !(minuend < divisor); + PTRef lt_prev = PTRef_Undef; + for (int j = 0; j < size; j ++) { + // Produce ~l[j] & r[j] + PTRef not_l = logic.mkNot(minuend[j]); + PTRef lt_this = logic.mkAnd(not_l, store[divisor][j]); + // Produce l[j] <-> r[j] + PTRef eq_this = logic.mkEq(minuend[j], store[divisor][j]); + if (lt_prev != PTRef_Undef) { + lt_prev = logic.mkOr(lt_this, logic.mkAnd(eq_this, lt_prev)); + } else { + lt_prev = lt_this; + } + } + + assert( lt_prev != PTRef_Undef); + + result[i] = logic.mkNot(lt_prev); + PTRef bit_i = result[i]; + + // Construct subtrahend + vec subtrahend; + subtrahend.capacity(size); + for (int j = 0; j < size; j ++) { + subtrahend.push(logic.mkAnd(bit_i, store[divisor][j])); + } + + // Subtract and store in minuend + PTRef carry = PTRef_Undef; + for (int j = 0; j < minuend.size(); j++) { + PTRef bit_1 = minuend[j]; + PTRef bit_2 = subtrahend[j]; + + PTRef bit_2_neg = logic.mkNot(bit_2); + PTRef xor_1 = logic.mkXor(bit_1, bit_2_neg); + PTRef and_1 = logic.mkAnd(bit_1, bit_2_neg); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + minuend[j] = xor_2; + } else { + carry = and_1; + minuend[j] = xor_1; + } + } + + carry = PTRef_Undef; + + // Adds one, if bit_i is one + for (int j = 0; j < minuend.size(); j++) { + PTRef bit_1 = minuend[j]; + PTRef bit_2 = j == 0 ? logic.getTerm_true() : logic.getTerm_false(); + + PTRef xor_1 = logic.mkXor(bit_1, bit_2); + PTRef and_1 = logic.mkAnd(bit_1, bit_2); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + minuend[j] = xor_2; + } else { + carry = and_1; + minuend[j] = xor_1; + } + } + + if (i > 0) { + // Prepare new minuend + // + // M[i-1] + // + // O[2] O[1] O[0] + // N[2] N[1] N[0] + // + for (int j = size - 1 ; j >= 1 ; j --) { + minuend[j] = minuend[j - 1]; + } + minuend[0] = store[dividend][i - 1]; + } + } + + // Save result and return + store.newBvector(result, div_tr); +} + +void BitBlasterConfig::bbUrem(PTRef rem_tr) { + Pterm const & rem = logic.getPterm(rem_tr); + + vec minuend; + BVRef dividend = store[rem[0]]; + BVRef divisor = store[rem[1]]; + + assert(store[divisor].size() == store[dividend].size()); + + auto size = store[divisor].size(); + + vec result; + result.growTo(size); + + // Initialize minuend as 0..0 q[n-1] + minuend.push(store[dividend][size-1]); + for (int i = 1; i < size; i ++) { + minuend.push(logic.getTerm_false()); + } + + // Main loop + for (int i = size - 1; i >= 0; i --) { + // Compute result[i] = !(minuend < divisor); + PTRef lt_prev = PTRef_Undef; + for (int j = 0; j < size; j ++) { + // Produce ~l[j] & r[j] + PTRef not_l = logic.mkNot(minuend[j]); + PTRef lt_this = logic.mkAnd(not_l, store[divisor][j]); + // Produce l[j] <-> r[j] + PTRef eq_this = logic.mkEq(minuend[j], store[divisor][j]); + if (lt_prev != PTRef_Undef) { + lt_prev = logic.mkOr(lt_this, logic.mkAnd(eq_this, lt_prev)); + } else { + lt_prev = lt_this; + } + } + + PTRef bit_i = logic.mkNot(lt_prev); + + // Construct subtrahend + vec subtrahend; + for (int j = 0; j < size; j ++) { + subtrahend.push(logic.mkAnd(bit_i, store[divisor][j])); + } + + // Subtract and store in minuend + PTRef carry = PTRef_Undef; + + for (int j = 0; j < minuend.size(); j++) { + PTRef bit_1 = minuend[j]; + PTRef bit_2 = subtrahend[j]; + + PTRef bit_2_neg = logic.mkNot(bit_2); + PTRef xor_1 = logic.mkXor(bit_1, bit_2_neg); + PTRef and_1 = logic.mkAnd(bit_1, bit_2_neg); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + minuend[j] = xor_2; + } else { + carry = and_1; + minuend[j] = xor_1; + } + } + + carry = PTRef_Undef; + + // Adds one, if bit_i is one + for (int j = 0; j < minuend.size(); j++) { + PTRef bit_1 = minuend[j]; + PTRef bit_2 = j == 0 ? logic.getTerm_true() : logic.getTerm_false(); + + PTRef xor_1 = logic.mkXor(bit_1, bit_2); + PTRef and_1 = logic.mkAnd(bit_1, bit_2); + + if (carry != PTRef_Undef) { + PTRef xor_2 = logic.mkXor(xor_1, carry); + PTRef and_2 = logic.mkAnd(xor_1, carry); + carry = logic.mkOr(and_1, and_2); + minuend[j] = xor_2; + } else { + carry = and_1; + minuend[j] = xor_1; + } + } + + if (i > 0) { + // Prepare new minuend + // M[i-1] + // + // O[2] O[1] O[0] + // N[2] N[1] N[0] + // + for (int j = size - 1; j >= 1; j --) { + minuend[j] = minuend[j - 1]; + } + minuend[0] = store[dividend][i - 1]; + } else { + for (int j = 0 ; j < size; j ++) { + result[j] = minuend[j]; + } + } + } + + // Save result + store.newBvector(result, rem_tr); +} + +auto ls_read = [](int s, int i, std::vector> const & table) { return table[s+1][i]; }; +auto ls_write = [](int s, int i, PTRef tr, std::vector> & table) { table[s+1][i] = tr; }; + +void BitBlasterConfig::bbShl(PTRef shl_tr) { + Pterm const & shl = logic.getPterm(shl_tr); + // Allocate new result + vec result; + + vec acc; + + BVRef a = store[shl[0]]; + BVRef b = store[shl[1]]; + + assert(store[a].size() == store[b].size()); + int size = store[a].size(); + if (not opensmt::isPowOfTwo(size)) { + throw OsmtApiException("shl not supported for non-power-of-two bit widths currently"); + } + + int l = size; + int n = opensmt::getLogFromPowOfTwo(size); + + std::vector> ls; + for (int s = -1; s <= n-1; s++) { + ls.emplace_back(); + for (int i = 0; i < l; i++) { + ls.back().push(PTRef_Undef); + } + } + + + for (int i = 0; i < l; i++) { + ls_write(-1, i, store[a][i], ls); + } + + for (int s = 0; s <= n-1; s++) { + for (int i = 0; i < l; i++) { + if (i >= (1 << s)) {// i >= 2^s + ls_write(s, i, logic.mkIte(store[b][s], ls_read(s - 1, i - (1 << s), ls), ls_read(s - 1, i, ls)), ls); + } else { + ls_write(s, i, logic.mkIte(store[b][s], logic.getTerm_false(), ls_read(s - 1, i, ls)), ls); + } + } + } + store.newBvector(ls.back(), shl_tr); +} + +void BitBlasterConfig::bbLshr(PTRef lshr_tr) { + bool arith = false; + Pterm const & lshr = logic.getPterm(lshr_tr); + // Allocate new result + vec result; + + vec acc; + + BVRef a = store[lshr[0]]; + BVRef b = store[lshr[1]]; + + assert(store[a].size() == store[b].size()); + auto size = store[a].size(); + if (not opensmt::isPowOfTwo(size)) { + throw OsmtApiException("lshr not supported for non-power-of-two bit widths currently"); + } + + int l = size; + int n = opensmt::getLogFromPowOfTwo(size); + + std::vector> ls; + for (int s = -1; s <= n-1; s++) { + ls.emplace_back(); + for (int i = 0; i < l; i++) + ls.back().push(PTRef_Undef); + } + + for (int i = 0; i < l; i++) + ls_write(-1, i, store[a][i], ls); + + PTRef fill = arith ? store[a].msb() : logic.getTerm_false(); + for (int s = 0; s <= n-1; s++) { + for (int i = 0; i < l; i++) { + if (i + (1 << s) <= l-1) {// i + 2^s <= l-1 + ls_write(s, i, logic.mkIte(store[b][s], ls_read(s - 1, i + (1 << s), ls), ls_read(s - 1, i, ls)), ls); + } else { + ls_write(s, i, logic.mkIte(store[b][s], fill, ls_read(s - 1, i, ls)), ls); + } + } + } + + store.newBvector(ls.back(), lshr_tr); +} diff --git a/src/logics/BitBlasterRewriter.h b/src/logics/BitBlasterRewriter.h new file mode 100644 index 000000000..ec259a206 --- /dev/null +++ b/src/logics/BitBlasterRewriter.h @@ -0,0 +1,105 @@ +/* + * Copyright (c) 2008 - 2012, Roberto Bruttomesso + * Copyright (c) 2012 - 2022, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#ifndef OPENSMT_BITBLASTERREWRITER_H +#define OPENSMT_BITBLASTERREWRITER_H + +#include "Rewriter.h" +#include "FSBVLogic.h" +#include "bvsolver/BVStore.h" +#include "OsmtInternalException.h" + +class BitBlasterConfig : public DefaultRewriterConfig { + FSBVLogic & logic; + BVStore & store; + + static inline const std::string BitVectorVarPrefix = ".bv"; + + PTRef bbEquality(PTRef eq_tr); + PTRef bbDisequality(PTRef diseq_tr); + PTRef bbUlt(PTRef ult_tr); + void bbConstant(PTRef tr); + void bbMul(PTRef mul_tr); + void bbVar(PTRef var_tr); + void bbAdd(PTRef add_tr); + void bbConcat(PTRef tr); + void bbNot(PTRef tr); + void bbFlip(PTRef tr); + void bbAnd(PTRef tr); + void bbOr(PTRef tr); + void bbUdiv(PTRef tr); + void bbUrem(PTRef tr); + void bbShl(PTRef tr); + void bbLshr(PTRef tr); + + void notImplemented(PTRef tr) { throw OsmtInternalException(std::string("Not implemented: ") + logic.getSymName(tr)); } + + void bbNeg(PTRef tr) { notImplemented(tr); } + +public: + BitBlasterConfig(FSBVLogic & logic, BVStore & bvStore) : logic(logic), store(bvStore) {} + + PTRef rewrite(PTRef tr) override { + SymRef sr = logic.getSymRef(tr); + if (logic.isEquality(sr) and logic.isBitVectorSort(logic.getUniqueArgSort(sr))) { + return bbEquality(tr); + } else if (logic.isDisequality(sr) and logic.isBitVectorSort(logic.getUniqueArgSort(sr))) { + return bbDisequality(tr); + } else if (logic.isBVUlt(sr)) { + return bbUlt(tr); + } else if (logic.isBVConst(sr)) { + bbConstant(tr); + } else if (logic.isBVMul(sr)) { + bbMul(tr); + } else if (logic.isBVVar(sr)) { + bbVar(tr); + } else if (logic.isBVAdd(sr)) { + bbAdd(tr); + } else if (logic.isBVConcat(sr)) { + bbConcat(tr); + } else if (logic.isBVNot(sr)) { + bbNot(tr); + } else if (logic.isBVNeg(sr)) { + bbNeg(tr); + } else if (logic.isBVFlip(sr)) { + bbFlip(tr); + } else if (logic.isBVAnd(sr)) { + bbAnd(tr); + } else if (logic.isBVOr(sr)) { + bbOr(tr); + } else if (logic.isBVUdiv(sr)) { + bbUdiv(tr); + } else if (logic.isBVUrem(sr)) { + bbUrem(tr); + } else if (logic.isBVShl(sr)) { + bbShl(tr); + } else if (logic.isBVLshr(sr)) { + bbLshr(tr); + } + return tr; + } +}; + +class BitBlasterRewriter : Rewriter { + BitBlasterConfig config; + BVStore store; +public: + BitBlasterRewriter(FSBVLogic & logic) : Rewriter(logic, config), config(logic, store) {} + PTRef rewrite(PTRef tr) override { return Rewriter::rewrite(tr); } + std::unordered_map getBitBlastedTermToBitVectorTermMap() const { + std::unordered_map map; + for (PTRef tr : store.getBitVectorTerms()) { + BVRef br = store.getFromPTRef(tr); + for (PTRef bitBlastedTerm : store[br]) { + map.insert({bitBlastedTerm, tr}); + } + } + return map; + } +}; + +#endif //OPENSMT_BITBLASTERREWRITER_H diff --git a/src/logics/CMakeLists.txt b/src/logics/CMakeLists.txt index b37c95d92..6ba9d5cf7 100644 --- a/src/logics/CMakeLists.txt +++ b/src/logics/CMakeLists.txt @@ -7,6 +7,8 @@ target_sources(logics PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/CUFLogic.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/CUFLogic.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/CUFTheory.cc" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVLogic.cc" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVLogic.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Logic.cc" PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Logic.h" PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/LATheory.h" @@ -16,14 +18,18 @@ target_sources(logics PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Theory.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Theory.h" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVTheory.h" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVTheory.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFTheory.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.h" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.cc" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/BitBlasterRewriter.h" + PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/BitBlasterRewriter.cc" ) -install(FILES LogicFactory.h Theory.h Logic.h ArithLogic.h CUFLogic.h BVLogic.h FunctionTools.h +install(FILES LogicFactory.h Theory.h Logic.h ArithLogic.h CUFLogic.h BVLogic.h FunctionTools.h FSBVLogic.h DESTINATION ${INSTALL_HEADERS_DIR}) diff --git a/src/logics/FSBVLogic.cc b/src/logics/FSBVLogic.cc new file mode 100644 index 000000000..44189ba63 --- /dev/null +++ b/src/logics/FSBVLogic.cc @@ -0,0 +1,405 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * Copyright (c) 2021, Martin Blicha + * + * SPDX-License-Identifier: MIT + */ + +#include "FSBVLogic.h" + +FSBVLogic::FSBVLogic(opensmt::Logic_t type) + : Logic(type) + , sym_BVBaseSort(sort_store.newSortSymbol(SortSymbol(tk_bvbasesort, 0, SortSymbol::INTERNAL))) + , BVBaseSort(sort_store.getOrCreateSort(sym_BVBaseSort, {}).first) +{ } + +SRef FSBVLogic::getIndexedSort(SRef indexedSort, std::string const & idx) { + if (BVBaseSort == indexedSort) { + assert(opensmt::isNumber(idx)); + return makeBitVectorSortForBW(std::stoi(idx)); + } else { + return Logic::getIndexedSort(indexedSort, idx); + } +} + +opensmt::pair FSBVLogic::makeBitWidthSortForBW(BitWidth_t m) { + + std::string const bw_string = std::to_string(m); + SSymRef bwSortSym; + SortSymbol bw_sortSymbol(bw_string, 0, SortSymbol::INTERNAL); + if (not sort_store.peek(bw_sortSymbol, bwSortSym)) { + bwSortSym = sort_store.newSortSymbol(SortSymbol(bw_string, 0, SortSymbol::INTERNAL)); + } + // Do not create core predicates for bit width sorts + return sort_store.getOrCreateSort(bwSortSym, {}); +} + +SRef FSBVLogic::makeBitVectorSortForBW(BitWidth_t m) { + auto [bwSort, isNew] = makeBitWidthSortForBW(m); + // Create core predicates for bit vector sorts + SRef bvSort = getSort(sym_IndexedSort, {BVBaseSort, bwSort}); + if (isNew) { + defaultValueForSort.insert(bvSort, mkBVConst(m, 0)); + } + return bvSort; +} + +PTRef FSBVLogic::mkBVConstFromHex(std::string const & hex) { + return mkConst(makeBitVectorSortForBW((hex.length()-2)*4), hex.c_str()); // TODO: convert hex to binary +} + +PTRef FSBVLogic::mkBVConstFromBin(std::string const & bin) { + return mkConst(makeBitVectorSortForBW(bin.length()-2), bin.c_str()); +} + +PTRef FSBVLogic::mkBVConst(BitWidth_t m, unsigned c) { + std::string bitString = "#b" + opensmt::wordToBinary(c, m); + return mkConst(makeBitVectorSortForBW(m), bitString.c_str()); +} + +PTRef FSBVLogic::mkBVConst(SymRef sym) { + return mkConst(getSortRef(sym), sym_store.getName(sym)); +} + +SymRef FSBVLogic::mkBVAddSym(SRef a) { + + if (not isBitVectorSort(a)) { + throw OsmtApiException("mkBVAdd called for non-bitvector sort " + printSort(a)); + } + SymRef addSym; + if (not add_syms.peek(a, addSym)) { + addSym = declareFun_NoScoping_LeftAssoc(tk_bvadd, a, {a, a}); + } + return addSym; +} + +PTRef FSBVLogic::mkBVAdd(PTRef a1, PTRef a2) { + SymRef addSym = mkBVAddSym(getSortRef(a1)); + std::string why; + if (not typeCheck(addSym, {a1, a2}, why)) { + throw OsmtApiException(why); + } + return mkFun(addSym, {a1, a2}); +} + +PTRef FSBVLogic::mkBVAdd(vec const & args) { + if (args.size() < 2) { + throw OsmtApiException(std::string(tk_bvadd) + " requires at least two arguments"); + } + PTRef tr = mkBVAdd(args[0], args[1]); + for (int i = 2; i < args.size(); i++) { + tr = mkBVAdd(tr, args[i]); + } + return tr; +} + +SymRef FSBVLogic::mkBVConcatSym(SRef lhsSort, SRef rhsSort) { + if (not isBitVectorSort(lhsSort) or not isBitVectorSort(rhsSort)) { + throw OsmtApiException("mkBVConcat called for incompatible sorts " + printSort(lhsSort) \ + + " and " + printSort(rhsSort)); + } + BitWidth_t lhsbw = getBitWidth(lhsSort); + BitWidth_t rhsbw = getBitWidth(rhsSort); + BitWidth_t returnBitWidth = lhsbw + rhsbw; + + SRef returnBitVectorSort = makeBitVectorSortForBW(returnBitWidth); + return declareFun_NoScoping(tk_bvconcat, returnBitVectorSort, {lhsSort, rhsSort}); +} + +PTRef FSBVLogic::mkBVConcat(PTRef lhs, PTRef rhs) { + SymRef BVConcatSym = mkBVConcatSym(getSortRef(lhs), getSortRef(rhs)); + return mkFun(BVConcatSym, {lhs, rhs}); +} + +SymRef FSBVLogic::mkBVNegSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVNeg called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping(tk_bvneg, sr, {sr}); +} + +PTRef FSBVLogic::mkBVNeg(PTRef a) { + return mkBVAdd(mkBVFlip(a), mkBVConst(getRetSortBitWidth(a), 1)); +} + +SymRef FSBVLogic::mkBVFlipSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVFlip called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping(tk_bvflip, sr, {sr}); +} + +PTRef FSBVLogic::mkBVFlip(PTRef a) { + SymRef BVFlip = mkBVFlipSym(getSortRef(a)); + return mkFun(BVFlip, {a}); +} + +SymRef FSBVLogic::mkBVNotSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVNoot called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping(tk_bvnot, sr, {sr}); +} + +PTRef FSBVLogic::mkBVNot(PTRef a) { + SymRef BVNot = mkBVNotSym(getSortRef(a)); + return mkFun(BVNot, {a}); +} + +SymRef FSBVLogic::mkBVAndSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVAnd called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvand, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVAnd(PTRef a1, PTRef a2) { + SymRef BVAnd = mkBVAndSym(getSortRef(a1)); + std::string why; + if (not typeCheck(BVAnd, {a1, a2}, why)) { + throw OsmtApiException(why); + } + return mkFun(BVAnd, {a1, a2}); +} + +PTRef FSBVLogic::mkBVAnd(vec const & args) { + if (args.size() < 2) { + throw OsmtApiException(std::string(tk_bvand) + " requires at least two arguments"); + } + PTRef tr = mkBVAnd(args[0], args[1]); + for (int i = 2; i < args.size(); i++) { + tr = mkBVAnd(tr, args[i]); + } + return tr; +} + +SymRef FSBVLogic::mkBVOrSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVOr called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvor, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVOr(PTRef a1, PTRef a2) { + SymRef BVOr = mkBVOrSym(getSortRef(a1)); + std::string why; + if (not typeCheck(BVOr, {a1, a2}, why)) { + throw OsmtApiException(why); + } + return mkFun(BVOr, {a1, a2}); +} + +PTRef FSBVLogic::mkBVOr(vec const & args) { + if (args.size() < 2) { + throw OsmtApiException(std::string(tk_bvor) + " requires at least two arguments"); + } + PTRef tr = mkBVOr(args[0], args[1]); + for (int i = 2; i < args.size(); i++) { + tr = mkBVOr(tr, args[i]); + } + return tr; +} + +SymRef FSBVLogic::mkBVMulSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVMul called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvmul, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVMul(PTRef a1, PTRef a2) { + SymRef BVMul = mkBVMulSym(getSortRef(a1)); + std::string why; + if (not typeCheck(BVMul, {a1, a2}, why)) { + throw OsmtApiException(why); + } + + return mkFun(BVMul, {a1, a2}); +} + +PTRef FSBVLogic::mkBVMul(vec const & args) { + if (args.size() < 2) { + throw OsmtApiException(std::string(tk_bvmul) + " requires at least two arguments"); + } + PTRef tr = mkBVMul(args[0], args[1]); + for (int i = 2; i < args.size(); i++) { + tr = mkBVMul(tr, args[i]); + } + return tr; +} + +SymRef FSBVLogic::mkBVUdivSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVUdiv called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvudiv, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVUdiv(PTRef a1, PTRef a2) { + SymRef BVUdiv = mkBVUdivSym(getSortRef(a1)); + std::string why; + if (not typeCheck(BVUdiv, {a1, a2}, why)) { + throw OsmtApiException(why); + } + PTRef divFun = mkFun(BVUdiv, {a1, a2}); + auto bitWidth = getRetSortBitWidth(a1); + return mkIte(mkEq(a2, mkBVConst(bitWidth, 0)), mkBVConst(bitWidth, 1), divFun); +} + +SymRef FSBVLogic::mkBVUremSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVUrem called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvurem, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVUrem(PTRef a1, PTRef a2) { + SymRef BVUrem = mkBVUremSym(getSortRef(a1)); + std::string why; + if (not typeCheck(BVUrem, {a1, a2}, why)) { + throw OsmtApiException(why); + } + PTRef rem = mkFun(BVUrem, {a1, a2}); + auto bitWidth = getRetSortBitWidth(a1); + return mkIte(mkEq(a2, mkBVConst(bitWidth, 0)), a1, rem); +} + +SymRef FSBVLogic::mkBVShlSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVSHL called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvshl, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVShl(PTRef a, PTRef shift) { + SymRef BVSHL = mkBVShlSym(getSortRef(a)); + std::string why; + if (not typeCheck(BVSHL, {a, shift}, why)) { + throw OsmtApiException(why); + } + return mkFun(BVSHL, {a, shift}); +} + +SymRef FSBVLogic::mkBVLshrSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVLSHR called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvlshr, sr, {sr, sr}); +} + +PTRef FSBVLogic::mkBVLshr(PTRef a, PTRef shift) { + SymRef BVLSHR = mkBVLshrSym(getSortRef(a)); + std::string why; + if (not typeCheck(BVLSHR, {a, shift}, why)) { + throw OsmtApiException(why); + } + return mkFun(BVLSHR, {a, shift}); +} + +SymRef FSBVLogic::mkBVUltSym(SRef sr) { + if (not isBitVectorSort(sr)) { + throw OsmtApiException("mkBVULT called for unrelated sort " + printSort(sr)); + } + return declareFun_NoScoping_LeftAssoc(tk_bvult, sort_BOOL, {sr, sr}); +} + +PTRef FSBVLogic::mkBVUlt(PTRef lhs, PTRef rhs) { + SymRef BVULT = mkBVUltSym(getSortRef(lhs)); + std::string why; + if (not typeCheck(BVULT, {lhs, rhs}, why)) { + throw OsmtApiException(why); + } + return mkFun(BVULT, {lhs, rhs}); +} + + +PTRef FSBVLogic::insertTerm(SymRef sym, vec && args) { + if (isBVConcat(sym)) { + return mkBVConcat(args[0], args[1]); + } else if (isBVAdd(sym)) { + return mkBVAdd(std::move(args)); + } else if (isBVNeg(sym)) { + return mkBVNeg(args[0]); + } else if (isBVNot(sym)) { + return mkBVNot(args[0]); + } else if (isBVAnd(sym)) { + return mkBVAnd(std::move(args)); + } else if (isBVOr(sym)) { + return mkBVOr(std::move(args)); + } else if (isBVMul(sym)) { + return mkBVMul(std::move(args)); + } else if (isBVUdiv(sym)) { + return mkBVUdiv(args[0], args[1]); + } else if (isBVUrem(sym)) { + return mkBVUrem(args[0], args[1]); + } else if (isBVShl(sym)) { + return mkBVShl(args[0], args[1]); + } else if (isBVLshr(sym)) { + return mkBVLshr(args[0], args[1]); + } else if (isBVUlt(sym)) { + return mkBVUlt(args[0], args[1]); + } else if (isBVConst(sym)) { + return mkBVConst(sym); + } else { + return Logic::insertTerm(sym, std::move(args)); + } +} + +PTRef FSBVLogic::resolveTerm(char const * s, vec && args, SRef returnSort, SymbolMatcher symbolMatcher) { + if (s == std::string(tk_bvconcat)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvconcat) + " requires exactly two arguments"); + } + return mkBVConcat(args[0], args[1]); + } else if (s == std::string(tk_bvadd)) { + return mkBVAdd(std::move(args)); + } else if (s == std::string(tk_bvneg)) { + if (args.size() != 1) { + throw OsmtApiException(std::string(tk_bvneg) + " requires exactly one argument"); + } + return mkBVNeg(args[0]); + } else if (s == std::string(tk_bvnot)) { + if (args.size() != 1) { + throw OsmtApiException(std::string(tk_bvnot) + " require exactly one argument"); + } + return mkBVNot(args[0]); + } else if (s == std::string(tk_bvand)) { + return mkBVAnd(std::move(args)); + } else if (s == std::string(tk_bvor)) { + return mkBVOr(std::move(args)); + } else if (s == std::string(tk_bvmul)) { + return mkBVMul(std::move(args)); + } else if (s == std::string(tk_bvudiv)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvudiv) + " requires exactly two arguments"); + } + return mkBVUdiv(args[0], args[1]); + } else if (s == std::string(tk_bvurem)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvurem) + " requires exactly two arguments"); + } + return mkBVUrem(args[0], args[1]); + } else if (s == std::string(tk_bvshl)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvshl) + " requires exactly two arguments"); + } + return mkBVShl(args[0], args[1]); + } else if (s == std::string(tk_bvlshr)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvlshr) + " requires exactly two arguments"); + } + return mkBVLshr(args[0], args[1]); + } else if (s == std::string(tk_bvult)) { + if (args.size() != 2) { + throw OsmtApiException(std::string(tk_bvult) + " requires exactly two arguments"); + } + return mkBVUlt(args[0], args[1]); + } else if (std::string(s).rfind(BVHexPrefix, 0) == 0) { + return mkBVConstFromHex(s); + } else if (std::string(s).rfind(BVBinPrefix, 0) == 0) { + return mkBVConstFromBin(s); + } + else { + return Logic::resolveTerm(s, std::move(args), returnSort, symbolMatcher); + } +} diff --git a/src/logics/FSBVLogic.h b/src/logics/FSBVLogic.h new file mode 100644 index 000000000..9bcc2ee22 --- /dev/null +++ b/src/logics/FSBVLogic.h @@ -0,0 +1,148 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + + +#ifndef OPENSMT_FSBVLOGIC_H +#define OPENSMT_FSBVLOGIC_H +#include "Logic.h" +#include "NumberUtils.h" + +using BitWidth_t = uint32_t; + +class FSBVLogic : public Logic { + + static constexpr const char *BVHexPrefix = "#x"; + static constexpr const char *BVBinPrefix = "#b"; + + static constexpr const char *tk_bvconcat = "concat"; + static constexpr const char *tk_bvbasesort = "BitVec"; + static constexpr const char *tk_bvnot = "bvnot"; + static constexpr const char *tk_bvflip = "bvflip"; + static constexpr const char *tk_bvneg = "bvneg"; + static constexpr const char *tk_bvand = "bvand"; + static constexpr const char *tk_bvor = "bvor"; + static constexpr const char *tk_bvadd = "bvadd"; + static constexpr const char *tk_bvmul = "bvmul"; + static constexpr const char *tk_bvudiv = "bvudiv"; + static constexpr const char *tk_bvurem = "bvurem"; + static constexpr const char *tk_bvshl = "bvshl"; + static constexpr const char *tk_bvlshr = "bvlshr"; + static constexpr const char *tk_bvult ="bvult"; + + static constexpr const char *tk_extract = "extract"; + static constexpr const char *tk_div = "div"; + static constexpr const char *tk_rem = "rem"; + + SSymRef sym_BVBaseSort; + SRef BVBaseSort; + +// Map concatenation_syms; + Map not_syms; + Map neg_syms; + Map and_syms; + Map or_syms; + Map add_syms; + Map mul_syms; + Map udiv_syms; + Map urem_syms; + Map shl_syms; + Map lshr_syms; + Map ult_syms; + + opensmt::pair makeBitWidthSortForBW(BitWidth_t m); + + + SymRef mkBVConcatSym(SRef lhs, SRef rhs); + SymRef mkBVNegSym(SRef a); + SymRef mkBVNotSym(SRef a); + SymRef mkBVFlipSym(SRef a); + SymRef mkBVAndSym(SRef a); + SymRef mkBVOrSym(SRef a); + SymRef mkBVAddSym(SRef a); + SymRef mkBVMulSym(SRef a); + SymRef mkBVUdivSym(SRef a); + SymRef mkBVUremSym(SRef a); + SymRef mkBVShlSym(SRef a); + SymRef mkBVLshrSym(SRef a); + SymRef mkBVUltSym(SRef a); + + Map defaultValueForSort; +public: + FSBVLogic(opensmt::Logic_t type); + + virtual bool isBuiltinSort(SRef sr) const override { return (sort_store[sr].getSymRef() == sym_IndexedSort and sort_store[sr][0] == BVBaseSort) or Logic::isBuiltinSort(sr); } + virtual bool isBuiltinConstant(SymRef sr) const override { return isBVConst(sr) || Logic::isBuiltinConstant(sr); } + + bool isBitVectorSort(SRef sr) const { return sort_store[sr].getSymRef() == sym_IndexedSort and sort_store[sr].getSize() == 2 and sort_store[sort_store[sr][0]].getSymRef() == sym_BVBaseSort; } + SRef getIndexedSort(SRef indexedSort, std::string const & idx) override; + SRef makeBitVectorSortForBW(BitWidth_t m); + BitWidth_t getBitWidth(SRef sr) const { assert(isBitVectorSort(sr)); return std::stoi(sort_store.getSortSymName(sort_store[sr][1])); } + BitWidth_t getRetSortBitWidth(PTRef tr) const { SRef sr = getSortRef(tr); assert(isBitVectorSort(sr)); return getBitWidth(sr); } + + PTRef getDefaultValuePTRef(const SRef sref) const override { + if (isBitVectorSort(sref)) { + return defaultValueForSort[sref]; + } else { + return Logic::getDefaultValuePTRef(sref); + } + } + + bool yieldsSortBV(SymRef sr) const { return isBitVectorSort(getSortRef(sr)); } + bool yieldsSortBV(PTRef tr) const { return yieldsSortBV(getSymRef(tr)); } + + PTRef mkBVConstFromHex(std::string const & hexString); + PTRef mkBVConstFromBin(std::string const & binString); + PTRef mkBVConst(BitWidth_t m, unsigned c); + PTRef mkBVConst(SymRef sym); + PTRef mkBVVar(BitWidth_t m, std::string const & name) { return mkVar(makeBitVectorSortForBW(m), name.c_str()); } + + PTRef mkBVConcat(PTRef lhs, PTRef rhs); + + PTRef mkBVNeg(PTRef a); + PTRef mkBVNot(PTRef a); + PTRef mkBVFlip(PTRef a); + + PTRef mkBVAnd(vec const & args); + PTRef mkBVAnd(PTRef a1, PTRef a2); + + PTRef mkBVOr(PTRef a1, PTRef a2); + PTRef mkBVOr(vec const & args); + + PTRef mkBVAdd(vec const & args); + PTRef mkBVAdd(PTRef a1, PTRef a2); + + PTRef mkBVMul(vec const & args); + PTRef mkBVMul(PTRef a1, PTRef a2); + PTRef mkBVUdiv(PTRef dividend, PTRef divisor); + PTRef mkBVUrem(PTRef dividend, PTRef divisor); + PTRef mkBVShl(PTRef a, PTRef shift); + PTRef mkBVLshr(PTRef a, PTRef shift); + PTRef mkBVUlt(PTRef lhs, PTRef rhs); + + bool isBVConst(SymRef sr) const { return isConstant(sr) and yieldsSortBV(sr); } + bool isBVVar(SymRef sr) const { return isVar(sr) and yieldsSortBV(sr); } + + bool isEqualAsString(char const * x, char const * y) const { return std::string(x) == y; } + bool isBVConcat(SymRef sr) const { return isEqualAsString(tk_bvconcat, getSymName(sr)); } + bool isBVNeg(SymRef sr) const { return isEqualAsString(tk_bvneg, getSymName(sr)); } + bool isBVFlip(SymRef sr) const { return isEqualAsString(tk_bvflip, getSymName(sr)); } + bool isBVNot(SymRef sr) const { return isEqualAsString(tk_bvnot, getSymName(sr)); } + bool isBVAnd(SymRef sr) const { return isEqualAsString(tk_bvand, getSymName(sr)); } + bool isBVOr(SymRef sr) const { return isEqualAsString(tk_bvor, getSymName(sr)); } + bool isBVAdd(SymRef sr) const { return isEqualAsString(tk_bvadd, getSymName(sr)); } + bool isBVMul(SymRef sr) const { return isEqualAsString(tk_bvmul, getSymName(sr)); } + bool isBVUdiv(SymRef sr) const { return isEqualAsString(tk_bvudiv, getSymName(sr)); } + bool isBVUrem(SymRef sr) const { return isEqualAsString(tk_bvurem, getSymName(sr)); } + bool isBVShl(SymRef sr) const { return isEqualAsString(tk_bvshl, getSymName(sr)); } + bool isBVLshr(SymRef sr) const { return isEqualAsString(tk_bvlshr, getSymName(sr)); } + bool isBVUlt(SymRef sr) const { return isEqualAsString(tk_bvult, getSymName(sr)); } + + PTRef resolveTerm(char const * s, vec && args, SRef, SymbolMatcher) override; + PTRef insertTerm (SymRef sym, vec && args) override; + std::string printSym(SymRef sr) const override { return isBVConst(sr) ? getSymName(sr) : Logic::printSym(sr); } +}; + +#endif //OPENSMT_FSBVLOGIC_H diff --git a/src/logics/FSBVTheory.cc b/src/logics/FSBVTheory.cc new file mode 100644 index 000000000..c514427c9 --- /dev/null +++ b/src/logics/FSBVTheory.cc @@ -0,0 +1,37 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#include "FSBVTheory.h" +#include "OsmtInternalException.h" +#include "TreeOps.h" +#include "BitBlasterRewriter.h" + +static SolverDescr descr_bb_solver("BitBlaster", "BitBlaster for counting models?"); + +bool FSBVTheory::simplify(vec const & formulas, PartitionManager &, int curr) { + if (keepPartitions()) { + throw OsmtInternalException("Mode not supported for QF_BV yet"); + } else { + + PTRef coll_f = getCollateFunction(formulas, curr); + PTRef trans = getLogic().learnEqTransitivity(coll_f); + coll_f = getLogic().mkAnd(coll_f, trans); + auto subs_res = computeSubstitutions(coll_f); + PTRef fla = flaFromSubstitutionResult(subs_res); + + vec bvFormulas; + topLevelConjuncts(logic, fla, bvFormulas); + + BitBlasterRewriter bitBlasterRewriter(logic); + PTRef out = bitBlasterRewriter.rewrite(logic.mkAnd(bvFormulas)); + bbTermToBVTerm = bitBlasterRewriter.getBitBlastedTermToBitVectorTermMap(); + + subs_res = computeSubstitutions(out); + fla = flaFromSubstitutionResult(subs_res); + pfstore[formulas[curr]].root = fla; + return false; + } +} \ No newline at end of file diff --git a/src/logics/FSBVTheory.h b/src/logics/FSBVTheory.h new file mode 100644 index 000000000..f360db66f --- /dev/null +++ b/src/logics/FSBVTheory.h @@ -0,0 +1,33 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#ifndef OPENSMT_FSBVTHEORY_H +#define OPENSMT_FSBVTHEORY_H + +#include "Theory.h" +#include "FSBVLogic.h" +#include "FSBVTHandler.h" + +class FSBVTheory : public Theory +{ +private: + FSBVLogic & logic; + FSBVTHandler fsbvtshandler; + std::unordered_map bbTermToBVTerm; +public: + FSBVTheory(SMTConfig & c, FSBVLogic & logic) + : Theory(c) + , logic(logic) + , fsbvtshandler(c, logic) + { } + FSBVLogic & getLogic() override { return logic; } + const FSBVLogic & getLogic() const override { return logic; } + FSBVTHandler & getTSolverHandler() override { return fsbvtshandler; } + bool simplify(const vec&, PartitionManager&, int) override; + std::unordered_map const & getBBTermToBVTerm() const { return bbTermToBVTerm; } +}; + +#endif //OPENSMT_FSBVTHEORY_H diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 8363b935a..5e069c38f 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -330,6 +330,17 @@ SSymRef Logic::declareSortSymbol(SortSymbol symbol) { return sort_store.newSortSymbol(std::move(symbol)); } +SRef Logic::getIndexedSort(SRef indexedSort, std::string const & idx) { + SortSymbol s(idx, 0, SortSymbol::INTERNAL); + SSymRef idxSortSym; + if (not peekSortSymbol(s, idxSortSym)) { + idxSortSym = sort_store.newSortSymbol(SortSymbol(idx, 0, SortSymbol::INTERNAL)); + } + SRef idxSortIdx = sort_store.getOrCreateSort(idxSortSym, {}).first; + return getSort(sym_IndexedSort, {indexedSort, idxSortIdx}); +} + + SRef Logic::getSort(SSymRef symbolRef, vec && args) { auto [sr,created] = sort_store.getOrCreateSort(symbolRef, std::move(args)); if (created) { @@ -569,7 +580,9 @@ PTRef Logic::mkImpl(vec && args) { } PTRef Logic::mkBinaryEq(PTRef lhs, PTRef rhs) { - assert(getSortRef(lhs) == getSortRef(rhs)); + if (getSortRef(lhs) != getSortRef(rhs)) { + throw OsmtApiException("Sort mismatch in equality: " + printSort(getSortRef(lhs)) + " != " + printSort(getSortRef(rhs))); + } if (lhs == rhs) return getTerm_true(); if (isConstant(lhs) && isConstant(rhs)) return getTerm_false(); diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 2edf68ddc..955da7484 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -264,6 +264,7 @@ class Logic { bool peekSortSymbol(SortSymbol const &, SSymRef&); SSymRef declareSortSymbol(SortSymbol symbol); SRef getSort(SSymRef, vec && args); + virtual SRef getIndexedSort(SRef indexedSort, std::string const & idx); PTRef mkBoolVar (const char* name); @@ -368,7 +369,8 @@ class Logic { // args is sorted before lookup, but not simplified otherwise PTRef hasEquality (vec& args); - PTRef resolveTerm(const char* s, vec&& args, SRef sortRef = SRef_Undef, SymbolMatcher symbolMatcher = SymbolMatcher::Any); + virtual PTRef resolveTerm(const char* s, vec&& args, SRef sortRef = SRef_Undef, SymbolMatcher symbolMatcher = SymbolMatcher::Any); + virtual PTRef insertTerm (SymRef sym, vec && args); PTRef insertTerm(SymRef sym, vec const & args) { vec tmp; args.copyTo(tmp); return insertTerm(sym, std::move(tmp)); } @@ -395,7 +397,7 @@ class Logic { std::string printTerm (PTRef tr, bool l, bool s) const { return printTerm_(tr, l, s); } std::string pp(PTRef tr) const; // A pretty printer - std::string printSym (SymRef sr) const; + virtual std::string printSym (SymRef sr) const; virtual void termSort(vec& v) const;// { sort(v, LessThan_PTRef()); } void purify (PTRef r, PTRef& p, lbool& sgn) const;//{p = r; sgn = l_True; while (isNot(p)) { sgn = sgn^1; p = getPterm(p)[0]; }} diff --git a/src/logics/LogicFactory.cc b/src/logics/LogicFactory.cc index 275f6cddd..e9c1fd40c 100644 --- a/src/logics/LogicFactory.cc +++ b/src/logics/LogicFactory.cc @@ -6,6 +6,7 @@ #include "ArithLogic.h" #include "BVLogic.h" +#include "FSBVLogic.h" #include "OsmtApiException.h" #include @@ -17,6 +18,7 @@ std::array logicToName = {{"Undef", "Empty", "QF_UF", "QF_CUF", opensmt::Logic_t opensmt::getLogicFromString(const std::string& name) { if (name == "QF_UF") return opensmt::Logic_t::QF_UF; + if (name == "QF_BV") return opensmt::Logic_t::QF_BV; if (name == "QF_LRA") return opensmt::Logic_t::QF_LRA; if (name == "QF_RDL") return opensmt::Logic_t::QF_RDL; if (name == "QF_LIA") return opensmt::Logic_t::QF_LIA; @@ -68,6 +70,11 @@ Logic * opensmt::LogicFactory::getInstance(Logic_t logicType) { l = new BVLogic(logicType); break; } + case Logic_t::QF_BV: + { + l = new FSBVLogic(logicType); + break; + } default: assert(false); throw OsmtApiException{"No logic or unsupported logic specified"}; diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc index 63a759ffd..2a9cd961d 100644 --- a/src/options/SMTConfig.cc +++ b/src/options/SMTConfig.cc @@ -493,6 +493,8 @@ const char* SMTConfig::o_dump_state = ":dump-state"; const char* SMTConfig::o_time_queries = ":time-queries"; const char* SMTConfig::o_output_dir = ":output-dir"; const char* SMTConfig::o_ghost_vars = ":ghost-vars"; +const char* SMTConfig::o_print_clauses_only = ":print-clauses-only"; +const char* SMTConfig::o_print_clauses_file = ":print-clauses-file"; const char* SMTConfig::o_dump_query = ":dump-query"; const char* SMTConfig::o_dump_query_name = ":dump-query-name"; const char* SMTConfig::o_inst_name = ":instance-name"; @@ -510,6 +512,7 @@ const char* SMTConfig::o_sat_split_test_cube_and_conquer = ":test-cube-and-conqu const char* SMTConfig::o_sat_split_randomize_lookahead = ":randomize-lookahead"; const char* SMTConfig::o_sat_split_randomize_lookahead_buf = ":randomize-lookahead-buf"; // The n best found literals const char* SMTConfig::o_sat_remove_symmetries = ":remove-symmetries"; +const char* SMTConfig::o_count_models = ":count-models"; const char* SMTConfig::o_dryrun = ":dryrun"; const char* SMTConfig::o_do_substitutions = ":do-substitutions"; const char* SMTConfig::o_respect_logic_partitioning_hints = ":respect-logic-partitioning-hints"; // Logic can have a say whether a var is good for partitioning diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h index d284a099a..442bf8fd6 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -77,6 +77,7 @@ enum ASTType { , OPTION_T , OPTIONL_T , INFO_T , INFOL_T , CONST_T , CONSTL_T + , IDX_T , IDXL_T }; class ASTNode { @@ -304,6 +305,7 @@ struct SMTConfig static const char* o_sat_split_randomize_lookahead; static const char* o_sat_split_randomize_lookahead_buf; static const char* o_produce_models; + static const char* o_count_models; static const char* o_sat_remove_symmetries; static const char* o_dryrun; static const char* o_do_substitutions; @@ -312,6 +314,8 @@ struct SMTConfig static const char* o_ghost_vars; static const char* o_sat_solver_limit; static const char* o_global_declarations; + static const char* o_print_clauses_only; + static const char* o_print_clauses_file; static const char* o_sat_split_mode; private: @@ -780,6 +784,10 @@ struct SMTConfig optionTable[o_sat_split_randomize_lookahead_buf]->getValue().numval : 1; } + bool count_models() const { + return optionTable.has(o_count_models) ? optionTable[o_count_models]->getValue().numval : false; + } + int remove_symmetries() const { return optionTable.has(o_sat_remove_symmetries) ? optionTable[o_sat_remove_symmetries]->getValue().numval : 0; } @@ -812,6 +820,21 @@ struct SMTConfig return false; } + bool print_clauses_only() const { + if (optionTable.has(o_print_clauses_only)) { + return optionTable[o_print_clauses_only]->getValue().numval != 0; + } + return false; + } + + std::string get_counting_output_file() const { + if (optionTable.has(o_print_clauses_file)) { + return optionTable[o_print_clauses_file]->getValue().strval; + } else { + return "/dev/stdout"; + } + } + int do_substitutions() const { return optionTable.has(o_do_substitutions) ? optionTable[o_do_substitutions]->getValue().numval : 1; } diff --git a/src/parallel/MainSplitter.cc b/src/parallel/MainSplitter.cc index 52554699d..055b90d9f 100644 --- a/src/parallel/MainSplitter.cc +++ b/src/parallel/MainSplitter.cc @@ -81,7 +81,7 @@ void MainSplitter::writeSplits(std::string const & baseName) const { } } -std::unique_ptr MainSplitter::createInnerSolver(SMTConfig & config, THandler & thandler, PTPLib::net::Channel & ch) { +std::unique_ptr MainSplitter::createInnerSolver(SMTConfig & config, THandler & thandler, PTPLib::net::Channel & ch) { if (config.sat_split_type() == spt_scatter) { return std::make_unique(config, thandler, ch); } else if (config.sat_split_type() == spt_lookahead) { @@ -165,4 +165,4 @@ vec MainSplitter::addToConjunction(std::vector> const & in) c out.push(logic.mkOr(std::move(disj_vec))); } return out; -} \ No newline at end of file +} diff --git a/src/parallel/MainSplitter.h b/src/parallel/MainSplitter.h index c583bb983..43f451fb7 100644 --- a/src/parallel/MainSplitter.h +++ b/src/parallel/MainSplitter.h @@ -47,7 +47,7 @@ class MainSplitter : public MainSolver { public: MainSplitter(std::unique_ptr t,std::unique_ptr tm, std::unique_ptr th, - std::unique_ptr ss, Logic & logic, SMTConfig & config, std::string name) + std::unique_ptr ss, Logic & logic, SMTConfig & config, std::string name) : MainSolver(std::move(t), std::move(tm), std::move(th), std::move(ss),logic,config, std::move(name)) {} @@ -57,7 +57,7 @@ class MainSplitter : public MainSolver { void writeSplits(std::string const &) const; - static std::unique_ptr createInnerSolver(SMTConfig &, THandler &, PTPLib::net::Channel &); + static std::unique_ptr createInnerSolver(SMTConfig &, THandler &, PTPLib::net::Channel &); inline TermMapper& getTermMapper() const { return *term_mapper;} }; diff --git a/src/parsers/smt2new/smt2newlexer.ll b/src/parsers/smt2new/smt2newlexer.ll index bcbc7851f..7c2d0d690 100644 --- a/src/parsers/smt2new/smt2newlexer.ll +++ b/src/parsers/smt2new/smt2newlexer.ll @@ -94,6 +94,7 @@ using namespace osmttokens; "set-info" { yyget_lval(yyscanner)->tok = { t_setinfo }; return TK_SETINFO; } "set-option" { yyget_lval(yyscanner)->tok = { t_setoption }; return TK_SETOPTION; } "get-interpolants" { yyget_lval(yyscanner)->tok = { t_getinterpolants }; return TK_GETITPS; } +"count-models" { yyget_lval(yyscanner)->tok = { t_countmodels }; return TK_COUNTMODELS; } "theory" { yyget_lval(yyscanner)->tok = { t_theory }; return TK_THEORY; } "write-state" { yyget_lval(yyscanner)->tok = { t_writestate }; return TK_WRSTATE; } "read-state" { yyget_lval(yyscanner)->tok = { t_readstate }; return TK_RDSTATE; } diff --git a/src/parsers/smt2new/smt2newparser.yy b/src/parsers/smt2new/smt2newparser.yy index b9dd3bd6d..8b3eaea5c 100644 --- a/src/parsers/smt2new/smt2newparser.yy +++ b/src/parsers/smt2new/smt2newparser.yy @@ -76,17 +76,17 @@ void smt2newerror( YYLTYPE* locp, Smt2newContext* context, const char * s ) %token TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING -%token TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO +%token TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_COUNTMODELS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO %token TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN %token KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS %type TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING -%type TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO +%type TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_COUNTMODELS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO %type TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN %type KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS predef_key %type symbol identifier sort command attribute attribute_value s_expr spec_const qual_identifier var_binding sorted_var term const_val -%type sort_list command_list s_expr_list numeral_list term_list var_binding_list attribute_list sorted_var_list symbol_list +%type sort_list command_list s_expr_list term_list var_binding_list attribute_list sorted_var_list symbol_list %type b_value option info_flag %start script @@ -217,6 +217,11 @@ command: '(' TK_SETLOGIC symbol ')' $$ = new ASTNode(CMD_T, $2); $$->children = $3; } + | '(' TK_COUNTMODELS term_list ')' + { + $$ = new ASTNode(CMD_T, $2); + $$->children = $3; + } | '(' TK_WRSTATE TK_STR ')' { $$ = new ASTNode(CMD_T, $2); @@ -316,8 +321,13 @@ attribute_value: spec_const identifier: symbol { $$ = $1; } - | '(' '_' symbol numeral_list ')' - { $$ = $3; $$->children = $4; } + | '(' '_' symbol TK_NUM ')' + { + $$ = new ASTNode(IDX_T, NULL); + $$->children = new std::vector(); + $$->children->insert($$->children->begin(), new ASTNode(NUM_T, $4)); + $$->children->insert($$->children->begin(), $3); + } ; sort: identifier @@ -388,12 +398,6 @@ const_val: symbol { $$ = $1; } ; -numeral_list: numeral_list TK_NUM - { $1->push_back(new ASTNode(NUM_T, $2)); $$ = $1; } - | TK_NUM - { $$ = new std::vector(); $$->push_back(new ASTNode(NUM_T, $1)); } - ; - qual_identifier: identifier { $$ = $1; } | '(' TK_AS identifier sort ')' diff --git a/src/smtsolvers/CMakeLists.txt b/src/smtsolvers/CMakeLists.txt index d86041ede..41686d92e 100644 --- a/src/smtsolvers/CMakeLists.txt +++ b/src/smtsolvers/CMakeLists.txt @@ -1,8 +1,20 @@ -add_library(smtsolvers OBJECT "") +#add_library(smtsolvers OBJECT "") +add_library(smtsolvers OBJECT "" + LookaheadSMTSolver.cc + LookaheadSMTSolver.h + ClausePrinter.cc + ClausePrinter.h + LAScore.h + LAScore.cc + SMTSolver.h + Proof.h + ) + list(APPEND PRIVATE_SOURCES_TO_ADD "${CMAKE_CURRENT_SOURCE_DIR}/SimpSMTSolver.cc" +# "${CMAKE_CURRENT_SOURCE_DIR}/ScatterSplitter.h" "${CMAKE_CURRENT_SOURCE_DIR}/CoreSMTSolver.cc" "${CMAKE_CURRENT_SOURCE_DIR}/GhostSMTSolver.cc" "${CMAKE_CURRENT_SOURCE_DIR}/TheoryIF.cc" @@ -12,11 +24,16 @@ list(APPEND PRIVATE_SOURCES_TO_ADD "${CMAKE_CURRENT_SOURCE_DIR}/LookaheadSMTSolver.h" "${CMAKE_CURRENT_SOURCE_DIR}/LAScore.h" "${CMAKE_CURRENT_SOURCE_DIR}/LAScore.cc" + "${CMAKE_CURRENT_SOURCE_DIR}/ClausePrinter.h" + "${CMAKE_CURRENT_SOURCE_DIR}/ClausePrinter.cc" + "${CMAKE_CURRENT_SOURCE_DIR}/SMTSolver.h" + "${CMAKE_CURRENT_SOURCE_DIR}/Proof.cc" ) list(APPEND PUBLIC_SOURCES_TO_ADD "${CMAKE_CURRENT_SOURCE_DIR}/SimpSMTSolver.h" "${CMAKE_CURRENT_SOURCE_DIR}/GhostSMTSolver.h" "${CMAKE_CURRENT_SOURCE_DIR}/CoreSMTSolver.h" + "${CMAKE_CURRENT_SOURCE_DIR}/Proof.h" ) target_sources(smtsolvers PRIVATE ${PRIVATE_SOURCES_TO_ADD} PUBLIC ${PUBLIC_SOURCES_TO_ADD} ) @@ -33,13 +50,14 @@ if(PRINT_UNITS) target_compile_definitions(smtsolvers PRIVATE -DREPORT_DL1_THLITS) endif() -target_sources(proof - PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Proof.h" - PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Proof.cc") +#target_sources(proof +# PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Proof.h" +# PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Proof.cc") -install(FILES TheoryInterpolator.h +install(FILES TheoryInterpolator.h DESTINATION ${INSTALL_HEADERS_DIR}) -install(FILES SimpSMTSolver.h CoreSMTSolver.h + +install(FILES SimpSMTSolver.h CoreSMTSolver.h SMTSolver.h Proof.h DESTINATION ${INSTALL_HEADERS_DIR}) diff --git a/src/smtsolvers/ClausePrinter.cc b/src/smtsolvers/ClausePrinter.cc new file mode 100644 index 000000000..923619c37 --- /dev/null +++ b/src/smtsolvers/ClausePrinter.cc @@ -0,0 +1,88 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#include "ClausePrinter.h" +#include "Proof.h" + +#include "FSBVTheory.h" + +void ModelCounter::count(vec const & terms) const { + // print all clauses + auto & theory = dynamic_cast(theory_handler.getTheory()); + + std::ofstream out; + out.open(config.get_counting_output_file()); + + unsigned int numOfDisappearedAtoms = 0; + + // Include the vars that need to be counted but were optimised away in simplification to total var count + for (PTRef countTerm : terms) { + BitWidth_t bitWidth = theory.getLogic().getRetSortBitWidth(countTerm); + if (bvTermToVars.find(countTerm) != bvTermToVars.end()) { + auto const & varSet = bvTermToVars.at(countTerm); + assert(varSet.size() <= bitWidth); + numOfDisappearedAtoms += (bitWidth - varSet.size()); + } else { + numOfDisappearedAtoms += bitWidth; + } + } + + std::string bbVarString("c ind "); + + for (PTRef tr : terms) { + if (bvTermToVars.find(tr) != bvTermToVars.end()) { + for (auto v: bvTermToVars.at(tr)) { + bbVarString += std::to_string(v + 1) + " "; + } + } + } + // Add phony vars for correct counting also to ind + for (unsigned int i = 0; i < numOfDisappearedAtoms; i++) { + bbVarString += std::to_string(nVars()+i+1) + " "; + } + + out << bbVarString + "0\n"; + + out << "p cnf " + std::to_string(nVars() + numOfDisappearedAtoms) + " " + std::to_string(nClauses()) << std::endl; + for (vec const & smtClause : clauses) { + for (Lit l: smtClause) { + Var v = var(l); + out << (sign(l) ? -(v + 1) : (v + 1)) << " "; + } + out << "0" << std::endl; + } +} + +void ModelCounter::addVar(Var v) { + if (not vars.has(v)) { + vars.insert(v, true); + ++ numberOfVarsSeen; + } +} + +bool ModelCounter::addOriginalSMTClause(vec const & smtClause, opensmt::pair &) { + auto & theory = dynamic_cast(theory_handler.getTheory()); + auto const & bbTermToBVTerm = theory.getBBTermToBVTerm(); + for (Lit l : smtClause) { + Var v = var(l); + if (not vars.has(v)) { + // A new variable + addVar(v); + + PTRef bbTerm = theory_handler.varToTerm(v); + if (bbTermToBVTerm.find(bbTerm) != bbTermToBVTerm.end()) { + // The variable originates from bit-blasted gate + // Update the bits of the gate + PTRef bvTerm = bbTermToBVTerm.at(bbTerm); + bvTermToVars[bvTerm].insert(v); + } + } + } + vec outClause; + smtClause.copyTo(outClause); + clauses.push_back(std::move(outClause)); + return true; +} diff --git a/src/smtsolvers/ClausePrinter.h b/src/smtsolvers/ClausePrinter.h new file mode 100644 index 000000000..8658802ea --- /dev/null +++ b/src/smtsolvers/ClausePrinter.h @@ -0,0 +1,34 @@ +// +// Created by prova on 08.03.22. +// + +#ifndef OPENSMT_CLAUSEPRINTER_H +#define OPENSMT_CLAUSEPRINTER_H + +#include "SMTSolver.h" + +class ModelCounter : public SMTSolver { + std::vector> clauses; + void addVar(Var v) override; + Map vars; + int numberOfVarsSeen; + std::unordered_map, PTRefHash> bvTermToVars; + SMTConfig & config; +public: + ModelCounter(SMTConfig &c, THandler & tHandler) : SMTSolver(tHandler), numberOfVarsSeen(0), config(c) {} + int nVars() const override { return numberOfVarsSeen; } + int nClauses() const override { return clauses.size(); } + bool isOK() const override { return true; } + void restoreOK() override { } + lbool solve(vec const &) override { throw OsmtApiException("ModelCounter does not support satisfiability checking"); }; + bool addOriginalSMTClause(vec const & smtClause, opensmt::pair & inOutCRefs) override; + lbool modelValue(Lit) const override { return l_Undef; } + void fillBooleanVars(ModelBuilder &) override { throw OsmtApiException("ModelCounter does not support model building"); } + void initialize() override {} + void clearSearch() override {} + Proof const & getProof() const override { throw OsmtApiException("ModelCounter does not support proof production"); } + int getConflictFrame() const override { throw OsmtApiException("ModelCounter does not support satisfiability checking"); } + void count(vec const & terms) const; +}; + +#endif //OPENSMT_CLAUSEPRINTER_H diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 9ce70dc75..49fcb89da 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -70,11 +70,10 @@ namespace opensmt { // Constructor/Destructor: CoreSMTSolver::CoreSMTSolver(SMTConfig & c, THandler& t ) - : config (c) - , theory_handler (t) + : SMTSolver(t) + , config (c) , verbosity (c.verbosity()) , init (false) - , stop (false) // Parameters: (formerly in 'SearchParams') , var_decay (c.sat_var_decay()) , clause_decay (c.sat_clause_decay()) @@ -1248,103 +1247,6 @@ bool CoreSMTSolver::simplify() return true; } -void -CoreSMTSolver::pushBacktrackPoint() -{ - assert( config.isIncremental() ); - // - // Save undo stack size - // - undo_stack_size.push(undo_stack.size( )); - undo_trail_size.push(trail.size( )); -} - -void CoreSMTSolver::popBacktrackPoint() -{ - assert( config.isIncremental() ); - // - // Force restart, but retain assumptions - // - cancelUntil(0); - // - // Shrink back trail - // - int new_trail_size = undo_trail_size.last(); - undo_trail_size.pop(); - for ( int i = trail.size( ) - 1 ; i >= new_trail_size ; i -- ) - { - Var x = var(trail[i]); - assigns[x] = l_Undef; - vardata[x].reason = CRef_Undef; - insertVarOrder(x); - } - trail.shrink(trail.size( ) - new_trail_size); - assert( trail_lim.size( ) == 0 ); - qhead = trail.size( ); - // - // Undo operations - // - size_t new_stack_size = undo_stack_size.last(); - undo_stack_size.pop(); - while (static_cast(undo_stack.size()) > new_stack_size ) - { - const undo_stack_el op = undo_stack.last(); - - if (op.getType() == undo_stack_el::NEWVAR) - { - const Var x = op.getVar(); - - // Undoes insertVarOrder( ) - assert( order_heap.inHeap(x) ); - order_heap .remove(x); - // Undoes decision_var ... watches - decision .pop(); - seen .pop(); - activity .pop(); - vardata .pop(); - assigns .pop(); - watches.clean(mkLit(x, true)); - watches.clean(mkLit(x, false)); - // Remove variable from translation tables -// theory_handler->clearVar( x ); - } - else if (op.getType() == undo_stack_el::NEWUNIT) ; // Do nothing - else if (op.getType() == undo_stack_el::NEWCLAUSE) - { - CRef cr = op.getClause(); - assert( clauses.last() == cr ); - clauses.pop(); - removeClause(cr); - } - else if (op.getType() == undo_stack_el::NEWLEARNT) - { - CRef cr = op.getClause(); - detachClause(cr); - } - else - { - throw OsmtInternalException("unknown undo operation in CoreSMTSolver" + std::to_string(op.getType())); - } - - undo_stack.pop(); - } - // - // Clear all learnts - // - while( learnts.size( ) > 0 ) - { - CRef cr = learnts.last(); - learnts.pop( ); - removeClause(cr); - } - assert( learnts.size( ) == 0 ); - // Backtrack theory solvers - theory_handler.backtrack(trail.size()); - // Restore OK - restoreOK( ); - assert( isOK( ) ); -} - bool CoreSMTSolver::okContinue() const { return not opensmt::stop; diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h index d82505b13..571512d73 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -46,6 +46,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef MINISATSMTSOLVER_H #define MINISATSMTSOLVER_H +#define CACHE_POLARITY 0 + +#include "SMTSolver.h" #include "THandler.h" #include @@ -62,9 +65,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "SolverTypes.h" #include "Timer.h" +#include "Proof.h" -class Proof; -class ModelBuilder; // Helper method to print Literal to a stream std::ostream& operator <<(std::ostream& out, Lit l); // MB: Feel free to find a better place for this method. @@ -78,26 +80,24 @@ struct Pair { A first; B second; }; //================================================================================================= // Solver -- the main class: -class CoreSMTSolver +class CoreSMTSolver : public SMTSolver { friend class LookaheadScoreClassic; friend class LookaheadScoreDeep; protected: SMTConfig & config; // Stores Config - THandler & theory_handler; // Handles theory - bool verbosity; - bool init; + bool verbosity; + bool init; enum class ConsistencyAction { BacktrackToZero, ReturnUndef, SkipToSearchBegin, NoOp }; int search_counter; public: - bool stop = false; // Constructor/Destructor: // CoreSMTSolver(SMTConfig&, THandler&); - virtual ~CoreSMTSolver(); - void initialize ( ); - void clearSearch (); // Backtrack SAT solver and theories to decision level 0 + ~CoreSMTSolver() override; + void initialize () override; + void clearSearch () override; // Backtrack SAT solver and theories to decision level 0 // Problem specification: // @@ -105,7 +105,7 @@ class CoreSMTSolver void addVar_ (Var v); // Ensure that var v exists in the solver virtual Var newVar(bool dvar); // Add a new variable with parameters specifying variable mode. public: - void addVar(Var v); // Anounce the existence of a variable to the solver + void addVar(Var v) override; // Anounce the existence of a variable to the solver bool addOriginalClause(const vec & ps); bool addEmptyClause(); // Add the empty clause, making the solver contradictory. bool addOriginalClause(Lit p); // Add a unit clause to the solver. @@ -119,7 +119,8 @@ class CoreSMTSolver // bool simplify (); // Removes already satisfied clauses. void declareVarsToTheories(); // Declare the seen variables to the theories - bool solve ( const vec< Lit > & assumps ); // Search for a model that respects a given set of assumptions. + lbool solve (const vec< Lit > & assumps) override; // Search for a model that respects a given set of assumptions. + void crashTest (int, Var, Var); // Stress test the theory solver void toDimacs (FILE* f, const vec& assumps); // Write CNF to file in DIMACS-format. @@ -143,16 +144,16 @@ class CoreSMTSolver lbool safeValue (Var x) const; // The current value of a variable. l_Undef if the variable does not exist. lbool safeValue (Lit p) const; // The current value of a literal. l_Undef if the literal does not exist. - lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable. + lbool modelValue (Lit p) const override; // The value of a literal in the last model. The last call to solve must have been satisfiable. int nAssigns () const; // The current number of assigned literals. - int nClauses () const; // The current number of original clauses. + int nClauses () const override; // The current number of original clauses. int nLearnts () const; // The current number of learnt clauses. - int nVars () const; // The current number of variables. + int nVars () const override; // The current number of variables. int nFreeVars () const; - void fillBooleanVars(ModelBuilder & modelBuilder); + void fillBooleanVars(ModelBuilder & modelBuilder) override; - Proof const & getProof() const { assert(proof); return *proof; } + Proof const & getProof() const override { assert(proof); return *proof; } // Resource contraints: // @@ -170,12 +171,10 @@ class CoreSMTSolver // External support incremental and backtrackable APIs // MB: This is used (and needed) by BitBlaster; can be removed if BitBlaster is re-worked - void pushBacktrackPoint ( ); - void popBacktrackPoint ( ); void reset ( ); - inline void restoreOK ( ) { ok = true; conflict_frame = 0; } - inline bool isOK ( ) const { return ok; } // FALSE means solver is in a conflicting state - inline int getConflictFrame ( ) const { assert(not isOK()); return conflict_frame; } + inline void restoreOK ( ) override { ok = true; conflict_frame = 0; } + inline bool isOK ( ) const override { return ok; } // FALSE means solver is in a conflicting state + inline int getConflictFrame ( ) const override { assert(not isOK()); return conflict_frame; } template void printSMTClause (std::ostream &, const C& ); @@ -456,7 +455,7 @@ class CoreSMTSolver protected: #ifdef STATISTICS - void printStatistics ( ostream & ); // Prints statistics + void printStatistics ( std::ostream & ); // Prints statistics #endif void printTrail ( ); // Prints the trail (debugging) TPropRes checkTheory (bool, int&); // Checks consistency in theory. The second arg is conflictC @@ -763,11 +762,11 @@ uint32_t CoreSMTSolver::computeGlue(T const & ps) { // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer. -inline bool CoreSMTSolver::solve (const vec& assumps) +inline lbool CoreSMTSolver::solve (const vec& assumps) { budgetOff(); setAssumptions(assumps); - return solve_() == l_True; + return solve_(); } inline void CoreSMTSolver::toDimacs(const char* file) diff --git a/src/smtsolvers/SMTSolver.h b/src/smtsolvers/SMTSolver.h new file mode 100644 index 000000000..308a03c22 --- /dev/null +++ b/src/smtsolvers/SMTSolver.h @@ -0,0 +1,40 @@ +/* + * Copyright (c) 2022, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#ifndef OPENSMT_SMTSOLVER_H +#define OPENSMT_SMTSOLVER_H + +#include "SolverTypes.h" +#include "THandler.h" +#include "Proof.h" + +class SMTSolver { +protected: + THandler & theory_handler; + bool stop = false; +public: + SMTSolver(THandler & tHandler) : theory_handler(tHandler) {} + virtual ~SMTSolver() {}; + virtual int nVars() const = 0; + virtual int nClauses() const = 0; + virtual bool isOK() const = 0; + virtual void restoreOK() = 0; + virtual lbool solve(vec const & assumps) = 0; + virtual void addVar(Var) = 0; + virtual bool addOriginalSMTClause(vec const & clause, opensmt::pair & iorefs) = 0; + virtual lbool modelValue(Lit l) const = 0; + virtual void fillBooleanVars(ModelBuilder & modelBuilder) = 0; + virtual void initialize() = 0; + virtual void clearSearch() = 0; // Backtrack SAT solver and theories to decision level 0 + virtual Proof const & getProof() const = 0; + virtual int getConflictFrame() const = 0; + void setStop() { stop = true; } + virtual void mapEnabledFrameIdToVar(Var, uint32_t, uint32_t &) { return; } + virtual void addAssumptionVar(Var) { return; } +}; + + +#endif //OPENSMT_SMTSOLVER_H diff --git a/src/smtsolvers/SimpSMTSolver.cc b/src/smtsolvers/SimpSMTSolver.cc index ec4e4f941..7b2dbfa3f 100644 --- a/src/smtsolvers/SimpSMTSolver.cc +++ b/src/smtsolvers/SimpSMTSolver.cc @@ -119,68 +119,6 @@ Var SimpSMTSolver::newVar(bool dvar) return v; } - - -lbool SimpSMTSolver::solve_(bool do_simp, bool turn_off_simp) -{ - vec extra_frozen; - lbool result = l_True; - - if (config.sat_preprocess_theory != 0) { - throw OsmtApiException("preprocess theory has been temporairly disabled in this version"); - } - - // Added Code - //================================================================================================= - - do_simp &= use_simplification; - - if (do_simp) - { - // Assumptions must be temporarily frozen to run variable elimination: - for (int i = 0; i < assumptions.size(); i++) - { - Var v = var(assumptions[i]); - - // If an assumption has been eliminated, remember it. - assert(!isEliminated(v)); - - if (!frozen[v]) - { - // Freeze and store. - setFrozen(v, true); - extra_frozen.push(v); - } - } - - result = lbool(eliminate(turn_off_simp)); - } - -#ifdef STATISTICS - CoreSMTSolver::preproc_time = cpuTime( ); -#endif - - if (result == l_True) - result = solve_(); - - if (result == l_True) - { - extendModel(); - // Previous line - // #ifndef NDEBUG - verifyModel(); - } - - if (do_simp) - // Unfreeze the assumptions that were frozen: - for (int i = 0; i < extra_frozen.size(); i++) - setFrozen(extra_frozen[i], false); - - return result; -} - - - //================================================================================================= // Added code diff --git a/src/smtsolvers/SimpSMTSolver.h b/src/smtsolvers/SimpSMTSolver.h index d71c080d1..e59f3eb08 100644 --- a/src/smtsolvers/SimpSMTSolver.h +++ b/src/smtsolvers/SimpSMTSolver.h @@ -57,13 +57,13 @@ class SimpSMTSolver : public CoreSMTSolver SimpSMTSolver (SMTConfig &, THandler&); ~SimpSMTSolver( ); - void initialize ( ); + void initialize() override; // Problem specification: // Var newVar (bool dvar = true) override; - bool addOriginalSMTClause(const vec & smt_clause, opensmt::pair & inOutCRefs); + bool addOriginalSMTClause(const vec & smt_clause, opensmt::pair & inOutCRefs) override; public: bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). @@ -75,12 +75,9 @@ class SimpSMTSolver : public CoreSMTSolver // Solving: // - lbool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solve ( bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + lbool solve (vec const & assumps) override; + lbool solveLimited(vec const & assumps); + bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. // Memory managment: @@ -160,7 +157,6 @@ class SimpSMTSolver : public CoreSMTSolver // Main internal methods: // using CoreSMTSolver::solve_; - lbool solve_ (bool do_simp, bool turn_off_simp); bool asymm (Var v, CRef cr); bool asymmVar (Var v); void updateElimHeap (Var v); @@ -179,8 +175,8 @@ class SimpSMTSolver : public CoreSMTSolver bool implied (const vec& c); void relocAll (ClauseAllocator& to); - virtual void mapEnabledFrameIdToVar(Var, uint32_t, uint32_t &) { return; } - virtual void addAssumptionVar(Var) { return; } +// virtual void mapEnabledFrameIdToVar(Var, uint32_t, uint32_t &) { return; } +// virtual void addAssumptionVar(Var) { return; } }; @@ -196,15 +192,10 @@ inline void SimpSMTSolver::updateElimHeap(Var v) { elim_heap.update(v); } inline void SimpSMTSolver::setFrozen (Var v, bool b) { if ( !use_simplification ) return; frozen[v] = (char)b; if (b) { updateElimHeap(v); } } -inline lbool SimpSMTSolver::solve ( bool do_simp, bool turn_off_simp) { return solve(vec{}, do_simp, turn_off_simp); } -inline lbool SimpSMTSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { return solve(vec{p}, do_simp, turn_off_simp); } -inline lbool SimpSMTSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { return solve(vec{p,q}, do_simp, turn_off_simp); } -inline lbool SimpSMTSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { return solve(vec{p,q,r}, do_simp, turn_off_simp); } -inline lbool SimpSMTSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ - budgetOff(); setAssumptions(assumps); return solve_(do_simp, turn_off_simp); } -inline lbool SimpSMTSolver::solveLimited (const vec& assumps, bool do_simp, bool turn_off_simp){ - setAssumptions(assumps); return solve_(do_simp, turn_off_simp); } -//inline bool CoreSMTSolver::smtSolve () { return solve(); } +inline lbool SimpSMTSolver::solve (const vec& assumps) { + budgetOff(); setAssumptions(assumps); return solve_(); } +inline lbool SimpSMTSolver::solveLimited (const vec& assumps) { + setAssumptions(assumps); return solve_(); } //================================================================================================= #endif diff --git a/src/tsolvers/CMakeLists.txt b/src/tsolvers/CMakeLists.txt index eb12404c5..6a276615b 100644 --- a/src/tsolvers/CMakeLists.txt +++ b/src/tsolvers/CMakeLists.txt @@ -14,6 +14,8 @@ PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/THandler.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/TSolverHandler.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATHandler.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFTHandler.cc" +PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVTHandler.h" +PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/FSBVTHandler.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/TSolver.cc" PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTHandler.cc" ) diff --git a/src/tsolvers/FSBVTHandler.cc b/src/tsolvers/FSBVTHandler.cc new file mode 100644 index 000000000..03984ebaf --- /dev/null +++ b/src/tsolvers/FSBVTHandler.cc @@ -0,0 +1,13 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#include "FSBVTHandler.h" + +FSBVTHandler::FSBVTHandler(SMTConfig & c, FSBVLogic & l) + : TSolverHandler(c) + , logic(l) +{ +} \ No newline at end of file diff --git a/src/tsolvers/FSBVTHandler.h b/src/tsolvers/FSBVTHandler.h new file mode 100644 index 000000000..1ddc4ae7a --- /dev/null +++ b/src/tsolvers/FSBVTHandler.h @@ -0,0 +1,28 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + +#ifndef OPENSMT_FSBVTHANDLER_H +#define OPENSMT_FSBVTHANDLER_H + +#include "TSolverHandler.h" +#include "FSBVLogic.h" +#include "OsmtInternalException.h" + +class FSBVTHandler : public TSolverHandler +{ +private: + FSBVLogic & logic; +public: + FSBVTHandler(SMTConfig & c, FSBVLogic & l); + ~FSBVTHandler() override = default; + Logic & getLogic() override { return logic; } + Logic const & getLogic() const override { return logic; } + + PTRef getInterpolant(const ipartitions_t &, std::map *, PartitionManager &) override { throw OsmtInternalException("Operation not supported for FSBVLoogic"); }; + + lbool getPolaritySuggestion(PTRef) const override { return l_True; }; +}; +#endif //OPENSMT_FSBVTHANDLER_H diff --git a/src/tsolvers/bvsolver/BVStore.h b/src/tsolvers/bvsolver/BVStore.h index 58d86e0c9..4522a0bad 100644 --- a/src/tsolvers/bvsolver/BVStore.h +++ b/src/tsolvers/bvsolver/BVStore.h @@ -35,14 +35,21 @@ class BVStore vec idToBVRef; Map bv_map; // Mapping of a BV variable to the bit vector (automatic) Map carryonly; // A cache mapping sum PTRefs to their carry bit + vec bitVectorTerms; public: BVStore(); - BVRef newBvector(const vec& var_names, const vec& asgn, PTRef act_var, PTRef tr) { - BVRef br = bva.alloc(var_names, asgn, act_var); idToBVRef.push(br); + BVRef newBvector(vec const & asgn, PTRef act_var, PTRef tr) { + BVRef br = bva.alloc(asgn, act_var); idToBVRef.push(br); bv_map.insert(tr, br); + bitVectorTerms.push(tr); return br; } + + BVRef newBvector(vec const & asgn, PTRef tr) { + return newBvector(asgn, PTRef_Undef, tr); + } + void free(BVRef r) { bva.free(r); } Bvector& operator[] (BVRef br) { return bva[br]; } const Bvector& operator[] (BVRef br) const { return bva[br]; } @@ -52,11 +59,10 @@ class BVStore bool has_carryonly(PTRef tr) { return carryonly.has(tr); } PTRef getCarryOnly(PTRef tr) { return carryonly[tr]; } void insertCarryOnly(PTRef tr_sum, PTRef tr_carry) { carryonly.insert(tr_sum, tr_carry); } - BVRef getFromPTRef(PTRef r) { assert(bv_map.has(r)); return bv_map[r]; } + BVRef getFromPTRef(PTRef r) const { assert(bv_map.has(r)); return bv_map[r]; } void copyAsgnTo(BVRef bv, vec& tr_vec) { for (int i = 0; i < operator[](bv).size(); i++) tr_vec.push(operator[](bv)[i]); } - void copyNamesTo(BVRef bv, vec& tr_vec) { for (int i = 0; i < operator[](bv).size(); i++) tr_vec.push(operator[](bv).namebit(i)); } - void copyBVTo(BVRef bv, vec& na_vec) { for (int i = 0; i < operator[](bv).size(); i++) na_vec.push(operator[](bv).nameasgn(i)); } + vec const & getBitVectorTerms() const { return bitVectorTerms; } int size() const { return idToBVRef.size(); } }; diff --git a/src/tsolvers/bvsolver/BitBlaster.cc b/src/tsolvers/bvsolver/BitBlaster.cc index c298e4b00..5c735ade8 100644 --- a/src/tsolvers/bvsolver/BitBlaster.cc +++ b/src/tsolvers/bvsolver/BitBlaster.cc @@ -163,7 +163,7 @@ BitBlaster::assertLit (PtAsgn pta) lbool BitBlaster::check( ) { - const lbool res = solverP.solve( ); + const lbool res = solverP.solve({}); // assert( res || (explanation.size() != 0) ); return res; } @@ -171,14 +171,12 @@ BitBlaster::check( ) void BitBlaster::pushBacktrackPoint ( ) { - solverP.pushBacktrackPoint( ); } void BitBlaster::popBacktrackPoint ( ) { // Pop solver - solverP.popBacktrackPoint( ); solverP.restoreOK( ); has_model = false; } @@ -280,9 +278,6 @@ BitBlaster::bbEq(PTRef tr) if (bs.has(tr)) return bs.getFromPTRef(tr); - vec names; - getBVVars("eq", names, bitwidth); - Pterm& t = logic.getPterm(tr); assert( t.size() == 2 ); PTRef lhs = t[0]; @@ -305,7 +300,7 @@ BitBlaster::bbEq(PTRef tr) PTRef res = simplify( logic.mkAnd( result_args ) ); vec tmp(bitwidth, logic.getTerm_false()); tmp[0] = res; - return bs.newBvector(names, tmp, mkActVar(s_bbEq), tr); + return bs.newBvector(tmp, mkActVar(s_bbEq), tr); } // @@ -322,10 +317,6 @@ BitBlaster::bbBvslt(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("sle", names, bitwidth); - assert( t.size() == 2 ); PTRef lhs = t[0]; PTRef rhs = t[1]; @@ -344,7 +335,7 @@ BitBlaster::bbBvslt(PTRef tr) vec asgns; asgns.growTo(bitwidth, logic.getTerm_false()); asgns[0] = tr_out; - return bs.newBvector(names, asgns, mkActVar(s_bbBvslt), tr); + return bs.newBvector(asgns, mkActVar(s_bbBvslt), tr); } // @@ -366,10 +357,6 @@ BitBlaster::bbBvule(PTRef tr) // Return previous result if computed if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("ule", names, bitwidth); - assert(logic.getPterm(tr).size() == 2 ); PTRef lhs = logic.getPterm(tr)[0]; PTRef rhs = logic.getPterm(tr)[1]; @@ -406,7 +393,7 @@ BitBlaster::bbBvule(PTRef tr) asgns[0] = res; // Save result and return - return bs.newBvector(names, asgns, mkActVar(s_bbBvule), tr); + return bs.newBvector(asgns, mkActVar(s_bbBvule), tr); } // @@ -420,10 +407,6 @@ BitBlaster::bbConcat(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("con", names, bitwidth); - vec result; // Retrieve arguments and put on the stack for (int i = logic.getPterm(tr).size()-1; i >= 0; i--) { @@ -434,7 +417,7 @@ BitBlaster::bbConcat(PTRef tr) } // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbConcat), tr); + return bs.newBvector(result, mkActVar(s_bbConcat), tr); } // @@ -448,10 +431,6 @@ BitBlaster::bbExtract(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("ex", names, bitwidth); - int lsb = 0, msb = 0; assert(logic.getPterm(tr).size() == 1 ); @@ -465,7 +444,7 @@ BitBlaster::bbExtract(PTRef tr) result[j++] = bs[bb_arg][i]; // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbExtract), tr); + return bs.newBvector(result, mkActVar(s_bbExtract), tr); } // @@ -478,10 +457,6 @@ BitBlaster::bbBvand(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("and", names, bitwidth); - vec bb_args; // Bit-blast the arguments, and put the corresponding vectors @@ -502,7 +477,7 @@ BitBlaster::bbBvand(PTRef tr) result.push(logic.mkAnd(and_args)); } - return bs.newBvector(names, result, mkActVar(s_bbBvand), tr); + return bs.newBvector(result, mkActVar(s_bbBvand), tr); } // @@ -519,10 +494,6 @@ BitBlaster::bbBvland(PTRef tr) assert(logic.getPterm(tr).size() == 2); - // Allocate new result - vec names; - getBVVars("lan", names, bitwidth); - // Bit-blast the arguments, and put the corresponding vectors // into bb_args. PTRef arg1 = logic.getPterm(tr)[0]; @@ -546,7 +517,7 @@ BitBlaster::bbBvland(PTRef tr) // for (int i = 1; i < result.size(); i++) // result[i] = logic.getTerm_false(); - return bs.newBvector(names, result, mkActVar(s_bbBvland), tr); + return bs.newBvector(result, mkActVar(s_bbBvland), tr); } @@ -560,12 +531,6 @@ BitBlaster::bbBvor(PTRef tr) if (bs.has(tr)) return bs[tr]; - - // Allocate new result - vec names; - getBVVars("or", names, bitwidth); - - vec result; vec bb_args; @@ -588,7 +553,7 @@ BitBlaster::bbBvor(PTRef tr) } // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbBvor), tr); + return bs.newBvector(result, mkActVar(s_bbBvor), tr); } // @@ -602,11 +567,6 @@ BitBlaster::bbBvlor(PTRef tr) if (bs.has(tr)) return bs[tr]; - - // Allocate new result - vec names; - getBVVars("lor", names, bitwidth); - vec result; result.growTo(bitwidth, logic.getTerm_false()); @@ -626,7 +586,7 @@ BitBlaster::bbBvlor(PTRef tr) // result[i] = logic.getTerm_false(); // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbBvlor), tr); + return bs.newBvector(result, mkActVar(s_bbBvlor), tr); } @@ -642,10 +602,6 @@ BitBlaster::bbBvxor(PTRef tr) assert( logic.getPterm(tr).size() == 2 ); - // Allocate new result - vec names; - getBVVars("xor", names, bitwidth); - // Allocate new result vec result; @@ -659,7 +615,7 @@ BitBlaster::bbBvxor(PTRef tr) for ( int i = 0 ; i < bs[bb_lhs].size() ; i ++ ) result.push( logic.mkXor(bs[bb_lhs][i], bs[bb_rhs][i])); - return bs.newBvector(names, result, mkActVar(s_bbBvxor), tr); + return bs.newBvector(result, mkActVar(s_bbBvxor), tr); } // @@ -673,11 +629,6 @@ BitBlaster::bbBvcompl(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("not", names, bitwidth); - - // Allocate new result vec result; @@ -688,7 +639,7 @@ BitBlaster::bbBvcompl(PTRef tr) result.push(logic.mkNot(bs[bb_arg][i])); // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbBvcompl), tr); + return bs.newBvector(result, mkActVar(s_bbBvcompl), tr); } // @@ -703,11 +654,6 @@ BitBlaster::bbBvlnot(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("lnot", names, bitwidth); - - // Allocate new result vec result; result.growTo(bitwidth, logic.getTerm_false()); @@ -722,7 +668,7 @@ BitBlaster::bbBvlnot(PTRef tr) // result[i] = logic.getTerm_false(); // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbBvlnot), tr); + return bs.newBvector(result, mkActVar(s_bbBvlnot), tr); } BVRef @@ -733,10 +679,6 @@ BitBlaster::bbBvadd(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("add", names, bitwidth); - // Allocate new result vec result; @@ -774,7 +716,7 @@ BitBlaster::bbBvadd(PTRef tr) } // Save result and return - return bs.newBvector(names, result, mkActVar(s_bbBvadd), tr); + return bs.newBvector(result, mkActVar(s_bbBvadd), tr); } PTRef @@ -826,10 +768,6 @@ BitBlaster::bbBvudiv(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("udi", names, bitwidth); - // // Allocate new result // @@ -967,7 +905,7 @@ BitBlaster::bbBvudiv(PTRef tr) // // Save result and return // - return bs.newBvector(names, result, mkActVar(s_bbBvudiv), tr); + return bs.newBvector(result, mkActVar(s_bbBvudiv), tr); } BVRef @@ -978,10 +916,6 @@ BitBlaster::bbBvurem(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("ure", names, bitwidth); - // // Allocate new result // @@ -1122,7 +1056,7 @@ BitBlaster::bbBvurem(PTRef tr) // // Save result and return // - return bs.newBvector(names, result, mkActVar(s_bbBvurem), tr); + return bs.newBvector(result, mkActVar(s_bbBvurem), tr); } void @@ -1145,10 +1079,6 @@ BitBlaster::bbBvlshift(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("lsh", names, bitwidth); - // Allocate new result vec result; @@ -1182,7 +1112,7 @@ BitBlaster::bbBvlshift(PTRef tr) ls_write(s, i, logic.mkIte(bs[b][s], logic.getTerm_false(), ls_read(s-1, i, ls)), ls); } } - return bs.newBvector(names, ls.back(), mkActVar(s_bbBvlsh), tr); + return bs.newBvector(ls.back(), mkActVar(s_bbBvlsh), tr); } BVRef @@ -1205,11 +1135,6 @@ BitBlaster::bbBvrshift(PTRef tr, bool arith) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - const char* name_str = arith ? "arsh" : "lrsh"; - getBVVars(name_str, names, bitwidth); - // Allocate new result vec result; @@ -1245,7 +1170,7 @@ BitBlaster::bbBvrshift(PTRef tr, bool arith) } } PTRef actVar = arith ? mkActVar(s_bbBvarsh) : mkActVar(s_bbBvlrsh); - return bs.newBvector(names, ls.back(), actVar, tr); + return bs.newBvector(ls.back(), actVar, tr); } @@ -1257,10 +1182,6 @@ BitBlaster::bbBvmul(PTRef tr) if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("mul", names, bitwidth); - // Allocate new result vec result; @@ -1320,7 +1241,7 @@ BitBlaster::bbBvmul(PTRef tr) } } - return bs.newBvector(names, result, mkActVar(s_bbBvmul), tr); + return bs.newBvector(result, mkActVar(s_bbBvmul), tr); } BVRef @@ -1332,10 +1253,6 @@ BitBlaster::bbSignExtend(PTRef tr) // Return previous result if computed if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("se", names, bitwidth); - vec result; PTRef x = logic.getPterm(tr)[0]; @@ -1348,7 +1265,7 @@ BitBlaster::bbSignExtend(PTRef tr) for ( ; i < bitwidth; i ++ ) // Should be bit width of what? result.push(bs[bb_x].lsb()); - return bs.newBvector(names, result, mkActVar(s_bbSignExtend), tr); + return bs.newBvector(result, mkActVar(s_bbSignExtend), tr); } BVRef @@ -1360,17 +1277,14 @@ BitBlaster::bbVar(PTRef tr) if (bs.has(tr)) return bs[tr]; // Allocate new result - vec names; - getBVVars("bv", names, bitwidth); - vec result; - names.copyTo(result); + getBVVars("bv", result, bitwidth); // Save variable variables.push(tr); - BVRef rval = bs.newBvector(names, result, mkActVar(s_bbVar), tr); + BVRef rval = bs.newBvector(result, mkActVar(s_bbVar), tr); return rval; } @@ -1382,9 +1296,6 @@ BitBlaster::bbConstant(PTRef tr) assert(logic.isConstant(tr)); if (bs.has(tr)) return bs[tr]; - // Allocate new result - vec names; - getBVVars("c", names, bitwidth); vec asgns; asgns.growTo(bitwidth, logic.getTerm_false()); @@ -1407,7 +1318,7 @@ BitBlaster::bbConstant(PTRef tr) } } // Save result and return - return bs.newBvector(names, asgns, mkActVar(s_bbConstant), tr); + return bs.newBvector(asgns, mkActVar(s_bbConstant), tr); } /* @@ -1432,9 +1343,6 @@ BitBlaster::bbDistinct(PTRef tr) if (bs.has(tr)) return bs[tr]; - vec vars; - getBVVars("d", vars, bitwidth); - vec result; result.growTo(bitwidth, logic.getTerm_false()); vec args; @@ -1458,13 +1366,14 @@ BitBlaster::bbDistinct(PTRef tr) result[0] = logic.mkAnd(res_args); - return bs.newBvector(vars, result, mkActVar(s_bbDistinct), tr); + return bs.newBvector(result, mkActVar(s_bbDistinct), tr); } bool BitBlaster::addClause(vec & c) { - return solverP.addOriginalClause(c); + opensmt::pair tmp; + return solverP.addOriginalSMTClause(c, tmp); } //============================================================================= diff --git a/src/tsolvers/bvsolver/BitBlaster.h b/src/tsolvers/bvsolver/BitBlaster.h index c111962b8..0fb3a1ebb 100644 --- a/src/tsolvers/bvsolver/BitBlaster.h +++ b/src/tsolvers/bvsolver/BitBlaster.h @@ -78,7 +78,7 @@ class BitBlaster MainSolver& mainSolver; BVLogic& logic; // Egraph store THandler& thandler; - SimpSMTSolver& solverP; // Solver with proof logger + SMTSolver& solverP; // Solver with proof logger bool addClause(vec & c); diff --git a/src/tsolvers/bvsolver/Bvector.h b/src/tsolvers/bvsolver/Bvector.h index d4fb006ec..aa1f84b65 100644 --- a/src/tsolvers/bvsolver/Bvector.h +++ b/src/tsolvers/bvsolver/Bvector.h @@ -66,7 +66,7 @@ class Bvector { BVId id; PTRef actVar; // This has to be the last - NameAsgn args[0]; // Either the terms or the relocation reference + PTRef args[0]; // Either the terms or the relocation reference friend class BvectorAllocator; friend class BVStore; @@ -74,7 +74,7 @@ class Bvector { public: - Bvector(const vec& ps, PTRef actVar) : actVar(actVar) { + Bvector(const vec& ps, PTRef actVar) : actVar(actVar) { header.is_signed = 0; header.has_extra = 0; header.reloced = 0; @@ -82,6 +82,9 @@ class Bvector { for (int i = 0; i < ps.size(); i++) args[i] = ps[i]; } + + Bvector(vec const & ps) : Bvector(ps, PTRef_Undef) {} + Bvector() : actVar(PTRef_Undef) { header.is_signed = 0; header.has_extra = 0; @@ -94,20 +97,25 @@ class Bvector { int size () const { return header.size; } PTRef getActVar () const { return actVar; } - const PTRef& operator [] (int i) const { assert(i < size()); return args[i].asgn; } - PTRef& operator [] (int i) { assert(i < size()); return args[i].asgn; } + const PTRef& operator [] (int i) const { assert(i < size()); return args[i]; } + PTRef& operator [] (int i) { assert(i < size()); return args[i]; } const PTRef& lsb () const { return operator[](0); } const PTRef& msb () const { return operator[](size()-1); } - const PTRef& namebit(int i) const { assert(i < size()); return args[i].name; } - PTRef& namebit(int i) { assert(i < size()); return args[i].name; } - - const NameAsgn& nameasgn(int i) const { assert(i < size()); return args[i]; } - NameAsgn& nameasgn(int i) { assert(i < size()); return args[i]; } + /** + * @note The function is unsafe: if used in a loop, the loop should in *absolutely no case* build new terms in the same Pterm allocator + * @return A pointer to the first child of the term + */ + const PTRef* begin() const { return args; } + /** + * @note The function is unsafe: if used in a loop, the loop should in *absolutely no case* build new terms in the same Pterm allocator + * @return A pointer to right past the last child of the term + */ + const PTRef* end() const { return args + size(); } bool reloced () const { return header.reloced; } - BVRef relocation () const { return { args[0].name.x }; } - void relocate (BVRef t) { header.reloced = 1; args[0] = { {t.x}, {0} }; } + BVRef relocation () const { return { args[0].x }; } + void relocate (BVRef t) { header.reloced = 1; args[0] = {t.x}; } bool is_signed () const { return header.is_signed; } void set_signed (bool m) { header.is_signed = m; } @@ -135,19 +143,12 @@ class BvectorAllocator : public RegionAllocator to.n_terms = n_terms; RegionAllocator::moveTo(to); } - BVRef alloc(const vec & names, const vec & asgn, PTRef act_var) - { + BVRef alloc(vec const & asgn, PTRef act_var) { assert(sizeof(PTRef) == sizeof(uint32_t)); - assert(names.size() == asgn.size()); - uint32_t v = RegionAllocator::alloc(ptermWord32Size(2*names.size())); + uint32_t v = RegionAllocator::alloc(ptermWord32Size(asgn.size())); BVRef tid = {v}; - vec args; - args.growTo(names.size()); - for (int i = 0; i < args.size(); i++) - args[i] = {names[i], asgn[i]}; - new (lea(tid)) Bvector(args, act_var); + new (lea(tid)) Bvector(asgn, act_var); operator[](tid).setId(n_terms++); - return tid; } @@ -158,26 +159,12 @@ class BvectorAllocator : public RegionAllocator const Bvector& operator[](BVRef r) const { return (Bvector&)RegionAllocator::operator[](r.x); } Bvector* lea (BVRef r) { return (Bvector*)RegionAllocator::lea(r.x); } const Bvector* lea (BVRef r) const { return (Bvector*)RegionAllocator::lea(r.x); } - BVRef ael (const Bvector* t) { RegionAllocator::Ref r = RegionAllocator::ael((uint32_t*)t); BVRef rf; rf.x = r; return rf; } + BVRef ael (const Bvector* t) { RegionAllocator::Ref r = RegionAllocator::ael((uint32_t*)t); BVRef rf{r}; return rf; } - void free(BVRef tid) - { + void free(BVRef tid) { Bvector& t = operator[](tid); RegionAllocator::free(ptermWord32Size(t.size())); } - -// void reloc(BVRef& tr, BvectorAllocator& to) -// { -// Bvector& t = operator[](tr); -// -// if (t.reloced()) { tr = t.relocation(); return; } -// -// tr = to.alloc(t, false); -// t.relocate(tr); -// -// // Copy extra data-fields: -// to[tr].set_signed(t.is_signed()); -// } friend class BVStore; }; #endif diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 9d54259b0..1e8e47516 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -245,3 +245,11 @@ PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_SATSolverTypes.cc" target_link_libraries(SATSolverTypesTest OpenSMT gtest gtest_main) gtest_add_tests(TARGET SATSolverTypesTest) + +add_executable(FSBVTest) +target_sources(FSBVTest + PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_FSBV.cc" + ) + +target_link_libraries(FSBVTest OpenSMT gtest gtest_main) +gtest_add_tests(TARGET FSBVTest) diff --git a/test/unit/test_FSBV.cc b/test/unit/test_FSBV.cc new file mode 100644 index 000000000..7750886a4 --- /dev/null +++ b/test/unit/test_FSBV.cc @@ -0,0 +1,255 @@ +/* + * Copyright (c) 2021, Antti Hyvarinen + * + * SPDX-License-Identifier: MIT + */ + + +#include +#include + +#include +#include "BitBlasterRewriter.h" + +class FSBVTest : public ::testing::Test { +protected: + FSBVTest(): logic{opensmt::Logic_t::QF_BV} {} + + FSBVLogic logic; +}; + +TEST_F(FSBVTest, test_createConst) { + PTRef x = logic.mkBVConst(32, 123); + SRef xsort = logic.getSortRef(x); + std::string binaryRepresentation = logic.pp(x); + std::cout << binaryRepresentation << std::endl; + ASSERT_EQ(binaryRepresentation, "#b00000000000000000000000001111011"); + std::cout << logic.printSort(xsort) << std::endl; + ASSERT_NE(x, PTRef_Undef); + + PTRef y = logic.mkBVConst(16, 123); + SRef ysort = logic.getSortRef(y); + binaryRepresentation = logic.pp(y); + std::cout << binaryRepresentation << std::endl; + ASSERT_EQ(binaryRepresentation, "#b0000000001111011"); + std::cout << logic.printSort(ysort) << std::endl; + + PTRef z = logic.mkBVConst(16, 124); + SRef zsort = logic.getSortRef(z); + binaryRepresentation = logic.pp(z); + std::cout << binaryRepresentation << std::endl; + ASSERT_EQ(binaryRepresentation, "#b0000000001111100"); + std::cout << logic.printSort(zsort) << std::endl; + ASSERT_NE(y, z); + ASSERT_EQ(ysort, zsort); + + PTRef char1 = logic.mkBVConst(8, 1); + PTRef char257 = logic.mkBVConst(8, 257); + binaryRepresentation = logic.pp(char1); + ASSERT_EQ(binaryRepresentation, "#b00000001"); + std::cout << binaryRepresentation << std::endl; + binaryRepresentation = logic.pp(char257); + ASSERT_EQ(binaryRepresentation, "#b00000001"); + std::cout << binaryRepresentation << std::endl; + +// x = logic.mkBVConstFromHex("#0000007B"); +} + +TEST_F(FSBVTest, test_createVar) { + PTRef c8 = logic.mkBVVar(8, "v8"); + PTRef c9 = logic.mkBVVar(9, "v9"); + ASSERT_THROW(logic.mkEq(c8, c9), OsmtApiException); + PTRef c9_ = logic.mkBVVar(9, "w9"); + ASSERT_NO_THROW(logic.mkEq(c9, c9_)); +} + +TEST_F(FSBVTest, test_mkAdd) { + PTRef a8 = logic.mkBVVar(8, "a8"); + PTRef a9 = logic.mkBVVar(9, "a9"); + ASSERT_THROW(logic.mkBVAdd(a8, a9), OsmtApiException); + PTRef b8 = logic.mkBVVar(8, "b8"); + PTRef add8 = logic.mkBVAdd(a8, b8); + ASSERT_EQ(logic.getSortRef(add8), logic.getSortRef(b8)); + + BitBlasterRewriter bitBlaster(logic); + PTRef sum = logic.mkBVAdd(logic.mkBVConst(8, 10), logic.mkBVConst(8, 10)); + PTRef res = bitBlaster.rewrite(logic.mkEq(sum, logic.mkBVConst(8, 20))); + ASSERT_EQ(res, logic.getTerm_true()); + res = bitBlaster.rewrite(logic.mkEq(sum, logic.mkBVConst(8, 21))); + ASSERT_EQ(res, logic.getTerm_false()); +} + +TEST_F(FSBVTest, test_mkConcat) { + PTRef a4 = logic.mkBVVar(4, "a4"); + PTRef a5 = logic.mkBVVar(5, "a5"); + PTRef conc = logic.mkBVConcat(a4, a5); + std::cout << logic.pp(conc) << std::endl; + ASSERT_NE(conc, PTRef_Undef); + BitBlasterRewriter bitBlaster(logic); + PTRef c1 = logic.mkBVConst(4, 0); + PTRef c2 = logic.mkBVConst(3, 7); + conc = logic.mkBVConcat(c1, c2); + PTRef eq = logic.mkEq(conc, logic.mkBVConst(7, 7)); + std::cout << logic.pp(eq) << std::endl; + PTRef res = bitBlaster.rewrite(logic.mkEq(conc, logic.mkBVConst(7, 7))); + ASSERT_EQ(res, logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkNeg) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef neg_a = logic.mkBVNeg(a); + ASSERT_NE(a, PTRef_Undef); + std::cout << logic.pp(neg_a) << std::endl; + PTRef c = logic.mkBVConst(16, 1); + PTRef neg_c = logic.mkBVNeg(c); + PTRef eq = logic.mkEq(neg_c, logic.mkBVConst(16, 65535)); + std::cout << logic.pp(eq) << std::endl; + BitBlasterRewriter bitBlasterRewriter(logic); + ASSERT_EQ(logic.getTerm_true(), bitBlasterRewriter.rewrite(eq)); +} + +TEST_F(FSBVTest, test_mkNot) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef not_a = logic.mkBVNot(a); + ASSERT_NE(a, PTRef_Undef); + std::cout << logic.pp(not_a) << std::endl; + PTRef c = logic.mkBVConst(4, 0); + PTRef not_c = logic.mkBVNot(c); + PTRef eq = logic.mkEq(not_c, logic.mkBVConst(4, 1)); + std::cout << logic.pp(eq) << std::endl; + BitBlasterRewriter bitBlasterRewriter(logic); + ASSERT_EQ(bitBlasterRewriter.rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkFlip) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef not_a = logic.mkBVNot(a); + ASSERT_NE(a, PTRef_Undef); + std::cout << logic.pp(not_a) << std::endl; + PTRef c = logic.mkBVConst(4, 0); + PTRef not_c = logic.mkBVFlip(c); + PTRef eq = logic.mkEq(not_c, logic.mkBVConst(4, 15)); + std::cout << logic.pp(eq) << std::endl; + BitBlasterRewriter bitBlasterRewriter(logic); + ASSERT_EQ(bitBlasterRewriter.rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkAnd) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef and_a_b = logic.mkBVAnd(a, b); + ASSERT_NE(and_a_b, PTRef_Undef); + std::cout << logic.pp(and_a_b) << std::endl; + PTRef c1 = logic.mkBVConst(4, 15); + PTRef c2 = logic.mkBVConst(4, 14); + PTRef and_ = logic.mkBVAnd(c1, c2); + PTRef eq = logic.mkEq(and_, c2); + BitBlasterRewriter bitBlasterRewriter(logic); + ASSERT_EQ(bitBlasterRewriter.rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkOr) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef or_a_b = logic.mkBVOr(a, b); + ASSERT_NE(or_a_b, PTRef_Undef); + std::cout << logic.pp(or_a_b) << std::endl; + PTRef c1 = logic.mkBVConst(4, 15); + PTRef c2 = logic.mkBVConst(4, 14); + PTRef or_ = logic.mkBVOr(c1, c2); + PTRef eq = logic.mkEq(or_, c1); + BitBlasterRewriter bitBlasterRewriter(logic); + ASSERT_EQ(bitBlasterRewriter.rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkMul) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef mul_a_b = logic.mkBVMul(a, b); + ASSERT_NE(mul_a_b, PTRef_Undef); + std::cout << logic.pp(mul_a_b) << std::endl; + + BitBlasterRewriter bitBlaster(logic); + PTRef mul = logic.mkBVMul(logic.mkBVConst(8, 10), logic.mkBVConst(8, 2)); + PTRef res = bitBlaster.rewrite(logic.mkEq(mul, logic.mkBVConst(8, 20))); + ASSERT_EQ(res, logic.getTerm_true()); + res = bitBlaster.rewrite(logic.mkEq(mul, logic.mkBVConst(8, 21))); + ASSERT_EQ(res, logic.getTerm_false()); +} + +TEST_F(FSBVTest, test_mkUdiv) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef udiv_a_b = logic.mkBVUdiv(a, b); + ASSERT_NE(udiv_a_b, PTRef_Undef); + std::cout << logic.pp(udiv_a_b) << std::endl; + PTRef c1 = logic.mkBVConst(8, 3); + PTRef c2 = logic.mkBVConst(8, 2); + PTRef div = logic.mkBVUdiv(c1, c2); + PTRef eq = logic.mkEq(div, logic.mkBVConst(8, 1)); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); + div = logic.mkBVUdiv(c1, logic.mkBVConst(8, 0)); + std::cout << logic.pp(div) << std::endl; + eq = logic.mkEq(div, logic.mkBVConst(8, 1)); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkUrem) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef urem_a_b = logic.mkBVUrem(a, b); + ASSERT_NE(urem_a_b, PTRef_Undef); + std::cout << logic.pp(urem_a_b) << std::endl; + + PTRef c1 = logic.mkBVConst(8, 3); + PTRef c2 = logic.mkBVConst(8, 2); + PTRef rem = logic.mkBVUrem(c1, c2); + PTRef eq = logic.mkEq(rem, logic.mkBVConst(8, 1)); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); + rem = logic.mkBVUrem(c1, logic.mkBVConst(8, 0)); + eq = logic.mkEq(rem, c1); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); +} + + +TEST_F(FSBVTest, test_mkSHL) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef shl = logic.mkBVShl(a, b); + ASSERT_NE(shl, PTRef_Undef); + std::cout << logic.pp(shl) << std::endl; + + PTRef c1 = logic.mkBVConst(8, 1); + PTRef c2 = logic.mkBVConst(8, 2); + shl = logic.mkBVShl(c1, c2); + PTRef eq = logic.mkEq(shl, logic.mkBVConst(8, 4)); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkLSHR) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef lshr = logic.mkBVLshr(a, b); + ASSERT_NE(lshr, PTRef_Undef); + std::cout << logic.pp(lshr) << std::endl; + + PTRef c1 = logic.mkBVConst(8, 4); + PTRef c2 = logic.mkBVConst(8, 2); + lshr = logic.mkBVLshr(c1, c2); + PTRef eq = logic.mkEq(lshr, logic.mkBVConst(8, 1)); + ASSERT_EQ(BitBlasterRewriter(logic).rewrite(eq), logic.getTerm_true()); +} + +TEST_F(FSBVTest, test_mkULT) { + PTRef a = logic.mkBVVar(16, "a"); + PTRef b = logic.mkBVVar(16, "b"); + PTRef ult = logic.mkBVUlt(a, b); + ASSERT_NE(ult, PTRef_Undef); + std::cout << logic.pp(ult) << std::endl; + + BitBlasterRewriter bitBlaster(logic); + PTRef res = bitBlaster.rewrite(logic.mkBVUlt(logic.mkBVConst(8, 1), logic.mkBVConst(8, 2))); + ASSERT_EQ(res, logic.getTerm_true()); + res = bitBlaster.rewrite(logic.mkBVUlt(logic.mkBVConst(8, 2), logic.mkBVConst(8, 2))); + ASSERT_EQ(res, logic.getTerm_false()); +}