XX

Signed-off-by: Matthew Ballance <matt.ballance@gmail.com>

src/CompoundSolver.cpp

@@ -41,37 +41,52 @@ CompoundSolver::~CompoundSolver() {
 
 bool CompoundSolver::randomize(
 			IRandState								    *randstate,
-            const std::vector<dm::IModelFieldUP>        &root_fields,
+            dm::IModelField                             *root_field,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
             const RefPathSet                            &include_constraints,
             const RefPathSet                            &exclude_constraints,
 			SolveFlags								    flags) {
-    IFactory *factory = 0;
-    std::vector<SolveSetUP>     solvesets;
+    std::vector<ISolveSetUP>    solvesets;
     RefPathSet                  unconstrained;
 
     TaskBuildSolveSets(
-        factory->getDebugMgr(),
-        root_fields,
+        m_dmgr,
+        root_field,
         target_fields,
+        fixed_fields,
         include_constraints,
         exclude_constraints).build(solvesets, unconstrained);
 
+    // First, randomize any unconstrained fields
     if (!unconstrained.empty()) {
         RefPathSet fixed_fields;
         m_solver_unconstrained.randomize(
+            randstate,
+            root_field,
+            unconstrained);
+    }
+
+    // Now, move on
+    for (std::vector<ISolveSetUP>::const_iterator
+        it=solvesets.begin();
+        it!=solvesets.end(); it++) {
+        ISolverUP solver(m_solver_f->mkSolver(it->get()));
+        /*
+        if (!solver->randomize(
             randstate,
             root_fields,
-            unconstrained,
-            fixed_fields);
+            (*it)->getFields(),
+
+        ))
+         */
     }
 
     return true;
 }
 
 bool CompoundSolver::sat(
-            const std::vector<dm::IModelFieldUP>        &root_fields,
+            dm::IModelField                             *root_field,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
             const RefPathSet                            &include_constraints,

src/CompoundSolver.h

@@ -38,15 +38,15 @@ class CompoundSolver : public ICompoundSolver {
 
 	virtual bool randomize(
 			IRandState								    *randstate,
-            const std::vector<dm::IModelFieldUP>        &root_fields,
+            dm::IModelField                             *root_field,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
             const RefPathSet                            &include_constraints,
             const RefPathSet                            &exclude_constraints,
 			SolveFlags								    flags) override;
 
 	virtual bool sat(
-            const std::vector<dm::IModelFieldUP>        &root_fields,
+            dm::IModelField                             *root_field,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
             const RefPathSet                            &include_constraints,

src/Factory.cpp

@@ -1,11 +1,13 @@
 
+#include <unistd.h>
 #include "Factory.h"
 #include "CompoundSolver.h"
 #include "RandStateMt19937_64.h"
 #include "RandStateLehmer_64.h"
 #include "RandStateLehmer_64_dual.h"
 #include "RandStateLehmer_32.h"
 #include "vsc/solvers/FactoryExt.h"
+#include "SolverFactoryBoolector.h"
 
 namespace vsc {
 namespace solvers {
@@ -19,7 +21,7 @@ Factory::~Factory() {
 }
 
 ICompoundSolver *Factory::mkCompoundSolver() {
-    return new CompoundSolver(m_dmgr, m_solver_f.get());
+    return new CompoundSolver(m_dmgr, getSolverFactory());
 }
 
 IRandState *Factory::mkRandState(const std::string &seed) {
@@ -28,6 +30,18 @@ IRandState *Factory::mkRandState(const std::string &seed) {
 //    return new RandStateMt19937_64(seed);
 }
 
+ISolverFactory *Factory::getSolverFactory() {
+    if (!m_solver_f) {
+        const char *vsc_solver_strategy = getenv("VSC_SOLVER_STRATEGY");
+
+        if (vsc_solver_strategy && vsc_solver_strategy[0]) {
+
+        } else {
+            m_solver_f = ISolverFactoryUP(new SolverFactoryBoolector(m_dmgr));
+        }
+    }
+}
+
 IFactory *Factory::inst() {
     if (!m_inst) {
         m_inst = FactoryUP(new Factory());

src/Factory.h

@@ -23,6 +23,8 @@ class Factory : public virtual IFactory {
         return m_dmgr;
     }
 
+    virtual ISolverFactory *getSolverFactory() override;
+
 	virtual ICompoundSolver *mkCompoundSolver() override;
 
     virtual IRandState *mkRandState(const std::string &seed) override;

src/SolveSet.cpp

@@ -18,41 +18,62 @@
  * Created on:
  *     Author:
  */
+#include <string.h>
 #include "SolveSet.h"
 
 
 namespace vsc {
 namespace solvers {
 
 
-SolveSet::SolveSet() {
-
+SolveSet::SolveSet() : m_max_bits(0), m_num_bits(0) {
+    memset(m_size, 0, sizeof(m_size));
 }
 
 SolveSet::~SolveSet() {
 
 }
 
-void SolveSet::addField(const std::vector<int32_t> &path) {
-    m_field_s.add(path);
-    m_target_field_s.add(path);
+void SolveSet::setFlag(SolveSetFlags flags) {
+
+}
+
+void SolveSet::addField(
+    const std::vector<int32_t>  &path, 
+    SolveSetFieldType           type,
+    int32_t                     bits) {
+    if (m_field_s.add(path, type)) {
+        m_size[(uint32_t)type]++;
+    }
+    if (bits > 0) {
+        if (bits > m_max_bits) {
+            m_max_bits = bits;
+        }
+        m_num_bits += bits;
+    }
 }
 
 void SolveSet::addConstraint(const std::vector<int32_t> &path) {
     m_constraint_s.add(path);
 };
 
-int32_t SolveSet::size() const {
-    return m_field_s.size();
+int32_t SolveSet::size(SolveSetFieldType type) const {
+    return m_size[(uint32_t)type];
 }
 
 void SolveSet::merge(SolveSet *rhs) {
-    for (RefPathSet::iterator it=rhs->getFields().begin(); it.next(); ) {
-        addField(it.path());
+    for (RefPathMap<SolveSetFieldType>::iterator 
+        it=rhs->getFields().begin(); it.next(); ) {
+        addField(it.path(), it.value(), -1);
     }
-    for (RefPathSet::iterator it=rhs->getConstraints().begin(); it.next(); ) {
+    for (RefPathSet::iterator 
+        it=rhs->getConstraints().begin(); it.next(); ) {
         addConstraint(it.path());
     }
+    if (rhs->m_max_bits > m_max_bits) {
+        m_max_bits = rhs->m_max_bits;
+    }
+    m_num_bits += rhs->m_num_bits;
 }
 
 }

src/SolveSet.h

@@ -19,35 +19,48 @@
  *     Author: 
  */
 #pragma once
-#include "vsc/dm/impl/UP.h"
-#include "vsc/solvers/impl/RefPathSet.h"
+#include "vsc/solvers/ISolveSet.h"
 
 namespace vsc {
 namespace solvers {
 
+
 class SolveSet;
 using SolveSetUP=dm::UP<SolveSet>;
-class SolveSet {
+class SolveSet : public virtual ISolveSet {
 public:
     SolveSet();
 
     virtual ~SolveSet();
 
-    void addField(const std::vector<int32_t> &path);
+    virtual SolveSetFlags getFlags() const override { return m_flags; }
+
+    void setFlag(SolveSetFlags flags);
+
+    void addField(
+        const std::vector<int32_t>  &path,
+        SolveSetFieldType           type,
+        int32_t                     bits=-1);
 
     void addConstraint(const std::vector<int32_t> &path);
 
-    const RefPathSet &getFields() const { return m_field_s; }
+    virtual const RefPathMap<SolveSetFieldType> &getFields() const override {
+        return m_field_s;
+    }
 
     const RefPathSet &getConstraints() const { return m_constraint_s; }
 
-    int32_t size() const;
+    int32_t size(SolveSetFieldType type=SolveSetFieldType::Target) const;
 
     void merge(SolveSet *rhs);
 
 private:
-    RefPathSet                      m_field_s;
-    RefPathSet                      m_target_field_s;
+    SolveSetFlags                   m_flags;
+    uint32_t                        m_max_bits;
+    uint32_t                        m_num_bits;
+    uint32_t                        m_size[(uint32_t)SolveSetFieldType::NumTypes];
+
+    RefPathMap<SolveSetFieldType>   m_field_s;
     RefPathSet                      m_constraint_s;
 
 

src/SolverBoolector.cpp

@@ -0,0 +1,67 @@
+/*
+ * SolverBoolector.cpp
+ *
+ * Copyright 2023 Matthew Ballance and Contributors
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License"); you may 
+ * not use this file except in compliance with the License.  
+ * You may obtain a copy of the License at:
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software 
+ * distributed under the License is distributed on an "AS IS" BASIS, 
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ *
+ * Created on:
+ *     Author:
+ */
+#include "boolector/boolector.h"
+#include "dmgr/impl/DebugMacros.h"
+#include "SolverBoolector.h"
+
+
+namespace vsc {
+namespace solvers {
+
+
+SolverBoolector::SolverBoolector(dmgr::IDebugMgr *dmgr) {
+    DEBUG_INIT("vsc::solvers::SolverBoolector", dmgr);
+
+	m_btor = boolector_new();
+	boolector_set_opt(m_btor, BTOR_OPT_INCREMENTAL, 1);
+	boolector_set_opt(m_btor, BTOR_OPT_MODEL_GEN, 1);
+}
+
+SolverBoolector::~SolverBoolector() {
+	boolector_release_all(m_btor);
+	boolector_delete(m_btor);
+}
+
+bool SolverBoolector::randomize(
+        IRandState                              *randstate,
+        dm::IModelField                         *root_field,
+        ISolveSet                               *solveset) {
+    DEBUG_ENTER("randomize");
+
+    // Solve set will tell us what fields are:
+    // - target
+    // - have a fixed value
+
+    for (RefPathMap<SolveSetFieldType>::iterator
+        it=solveset->getFields().begin(); it.next(); ) {
+
+    }
+    // - Create variables for the target fields
+    // - Create constraints, opportunistically creating variables for non-target fields
+
+    DEBUG_LEAVE("randomize");
+    return true;
+}
+
+dmgr::IDebug *SolverBoolector::m_dbg = 0;
+
+}
+}

src/SolverBoolector.h

@@ -0,0 +1,52 @@
+/**
+ * SolverBoolector.h
+ *
+ * Copyright 2023 Matthew Ballance and Contributors
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License"); you may 
+ * not use this file except in compliance with the License.  
+ * You may obtain a copy of the License at:
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software 
+ * distributed under the License is distributed on an "AS IS" BASIS, 
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ *
+ * Created on:
+ *     Author: 
+ */
+#pragma once
+#include "dmgr/IDebugMgr.h"
+#include "vsc/solvers/ISolver.h"
+
+struct Btor;
+
+namespace vsc {
+namespace solvers {
+
+
+
+class SolverBoolector : public virtual ISolver {
+public:
+    SolverBoolector(dmgr::IDebugMgr *dmgr);
+
+    virtual ~SolverBoolector();
+
+    virtual bool randomize(
+        IRandState                              *randstate,
+        dm::IModelField                         *root_field,
+        ISolveSet                               *solveset) override;
+
+private:
+    static dmgr::IDebug             *m_dbg;
+    struct Btor                     *m_btor;
+
+};
+
+}
+}
+
+