Bvlogic

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)
+

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)

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)

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");

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 ')'

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 ')'

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

regression/QF_BV/setlogic.smt2.expected.out

@@ -1,2 +0,0 @@
-(error "unknown logic QF_BV")
-

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 ')'

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 ')'

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"

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 <string>
 #include <sstream>
@@ -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<SRef> 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<MainCounter&>(*main_solver);
+    auto exps = *n.children;
+    vec<PTRef> 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<MainSolver> Interpret::createMainSolver(const char* logic_name) {
-    return std::make_unique<MainSolver>(*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<TermMapper>(*logic);
+        auto thandler = new THandler(*th, *tm);
+        return std::make_unique<MainSplitter>(std::move(th),
+                                 std::move(tm),
+                                 std::unique_ptr<THandler>(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<TermMapper>(new TermMapper(*logic));
+        auto thandler = new THandler(*theory, *termMapper);
+        return std::make_unique<MainCounter>(std::move(theory),
+                                 std::move(termMapper),
+                                 std::unique_ptr<THandler>(thandler),
+                                 MainCounter::createInnerSolver(config, *thandler),
+                                 *logic,
+                                 config,
+                                 std::string(logic_name) + " counter");
+    } else {
+        return std::make_unique<MainSolver>(*logic, config, std::string(logic_name) + " solver");
+    } */
+    if (config.count_models()) {
+        auto theory = MainSolver::createTheory(*logic, config);
+        auto termMapper = std::unique_ptr<TermMapper>(new TermMapper(*logic));
+        auto thandler = new THandler(*theory, *termMapper);
+        return std::make_unique<MainCounter>(std::move(theory),
+                                 std::move(termMapper),
+                                 std::unique_ptr<THandler>(thandler),
+                                 MainCounter::createInnerSolver(config, *thandler),
+                                 *logic,
+                                 config,
+                                 std::string(logic_name) + " counter");
+    } else {
+        return std::make_unique<MainSolver>(*logic, config, std::string(logic_name) + " solver");
+    }
 }
-
-
-

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;

src/api/MainCounter.cc

@@ -0,0 +1,16 @@
+/*
+ * Copyright (c) 2021, Antti Hyvarinen <antti.hyvarinen@gmail.com>
+ *
+ * SPDX-License-Identifier: MIT
+ */
+
+#include "MainCounter.h"
+
+void MainCounter::countModels(vec<PTRef> const & terms) {
+    initialize();
+    sstat rval = MainSolver::simplifyFormulas();
+    assert(rval == s_Undef);
+    (void)rval;
+    auto & modelCounter = dynamic_cast<ModelCounter&>(*smt_solver);
+    modelCounter.count(terms);
+}

src/api/MainCounter.h

@@ -0,0 +1,31 @@
+/*
+ * Copyright (c) 2021, Antti Hyvarinen <antti.hyvarinen@gmail.com>
+ *
+ * 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<Theory> t, std::unique_ptr<TermMapper> tm, std::unique_ptr<THandler> th,
+                std::unique_ptr<ModelCounter> 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<ModelCounter> createInnerSolver(SMTConfig & config, THandler & thandler) { return std::make_unique<ModelCounter>(config, thandler); }
+
+    void countModels(vec<PTRef> const & terms);
+};
+
+
+#endif //OPENSMT_MAINCOUNTER_H