Unconstrained solver up and running

Signed-off-by: Matthew Ballance <matt.ballance@gmail.com>
vsc-tools · Sep 7, 2023 · e09dec4 · e09dec4
1 parent d1f092f
commit e09dec4
Show file tree

Hide file tree

Showing 25 changed files with 993 additions and 56 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -58,6 +58,9 @@ add_dependencies(vsc-solvers Boolector Bitwuzla)
 #     DESTINATION lib
 #     EXPORT vsc-solvers-targets)
 
+set(CMAKE_CXX_FLAGS_RELEASE "-O3")
+set(CMAKE_CXX_FLAGS_DEBUG "-O0 -g")
+
 install(TARGETS vsc-solvers
     DESTINATION lib
     EXPORT vsc-solvers-targets)

diff --git a/src/CompoundSolver.cpp b/src/CompoundSolver.cpp
@@ -18,15 +18,20 @@
  * Created on:
  *     Author:
  */
+#include "dmgr/impl/DebugMacros.h"
+#include "vsc/solvers/impl/TaskBuildSolveSets.h"
 #include "CompoundSolver.h"
 
 
 namespace vsc {
 namespace solvers {
 
 
-CompoundSolver::CompoundSolver() {
-
+CompoundSolver::CompoundSolver(
+    dmgr::IDebugMgr         *dmgr,
+    ISolverFactory          *solver_f) : 
+        m_solver_f(solver_f), m_solver_unconstrained(dmgr) {
+    DEBUG_INIT("vsc::solvers::CompoundSolver", dmgr);
 }
 
 CompoundSolver::~CompoundSolver() {
@@ -38,17 +43,43 @@ bool CompoundSolver::randomize(
             const std::vector<dm::IModelFieldUP>        &root_fields,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
+            const RefPathSet                            &include_constraints,
+            const RefPathSet                            &exclude_constraints,
 			SolveFlags								    flags) {
+    IFactory *factory = 0;
+    std::vector<ISolveSetUP>    solvesets;
+    RefPathSet                  unconstrained;
+
+    TaskBuildSolveSets(
+        factory,
+        root_fields,
+        target_fields,
+        include_constraints,
+        exclude_constraints).build(solvesets, unconstrained);
+
+    if (!unconstrained.empty()) {
+        RefPathSet fixed_fields;
+        m_solver_unconstrained.randomize(
+            randstate,
+            root_fields,
+            unconstrained,
+            fixed_fields);
+    }
+
     return true;
 }
 
 bool CompoundSolver::sat(
             const std::vector<dm::IModelFieldUP>        &root_fields,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
+            const RefPathSet                            &include_constraints,
+            const RefPathSet                            &exclude_constraints,
 			SolveFlags								    flags) {
     return true;
 }
 
+dmgr::IDebug *CompoundSolver::m_dbg = 0;
+
 }
 }
diff --git a/src/CompoundSolver.h b/src/CompoundSolver.h
@@ -19,14 +19,20 @@
  *     Author: 
  */
 #pragma once
+#include "dmgr/IDebugMgr.h"
+#include "vsc/solvers/ISolverFactory.h"
 #include "vsc/solvers/ICompoundSolver.h"
+#include "SolverUnconstrained.h"
 
 namespace vsc {
 namespace solvers {
 
 class CompoundSolver : public ICompoundSolver {
 public:
-    CompoundSolver();
+    CompoundSolver(
+        dmgr::IDebugMgr     *dmgr,
+        ISolverFactory      *solver_f
+    );
 
     virtual ~CompoundSolver();
 
@@ -35,14 +41,23 @@ class CompoundSolver : public ICompoundSolver {
             const std::vector<dm::IModelFieldUP>        &root_fields,
             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,
             const RefPathSet                            &target_fields,
             const RefPathSet                            &fixed_fields,
+            const RefPathSet                            &include_constraints,
+            const RefPathSet                            &exclude_constraints,
 			SolveFlags								    flags) override;
 
+private:
+    static dmgr::IDebug                 *m_dbg;
+    ISolverFactory                      *m_solver_f;
+    SolverUnconstrained                 m_solver_unconstrained;
+
 };
 
 }

diff --git a/src/Factory.cpp b/src/Factory.cpp
@@ -1,7 +1,10 @@
 
 #include "Factory.h"
-//#include "CompoundSolverDefault.h"
-#include "RandState.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"
 
 namespace vsc {
@@ -15,14 +18,14 @@ Factory::~Factory() {
 
 }
 
-#ifdef UNDEFINED
-ICompoundSolver *Factory::mkCompoundSolver(dm::IContext *ctxt) {
-    return new CompoundSolverDefault(ctxt, &m_solver_factory);
+ICompoundSolver *Factory::mkCompoundSolver() {
+    return new CompoundSolver(m_dmgr, m_solver_f.get());
 }
-#endif
 
 IRandState *Factory::mkRandState(const std::string &seed) {
-    return new RandState(seed);
+    return new RandStateLehmer_64(seed);
+//    return new RandStateLehmer_32(seed);
+//    return new RandStateMt19937_64(seed);
 }
 
 IFactory *Factory::inst() {

diff --git a/src/Factory.h b/src/Factory.h
@@ -23,7 +23,7 @@ class Factory : public virtual IFactory {
         return m_dmgr;
     }
 
-//	virtual ICompoundSolver *mkCompoundSolver(dm::IContext *ctxt) override;
+	virtual ICompoundSolver *mkCompoundSolver() override;
 
     virtual IRandState *mkRandState(const std::string &seed) override;
 
@@ -33,6 +33,7 @@ class Factory : public virtual IFactory {
 private:
     static FactoryUP                    m_inst;
     dmgr::IDebugMgr                     *m_dmgr;
+    ISolverFactoryUP                    m_solver_f;
 
 };
 

diff --git a/src/RandStateLehmer_32.cpp b/src/RandStateLehmer_32.cpp
@@ -0,0 +1,105 @@
+/*
+ * RandStateLehmer_32.cpp
+ *
+ *  Created on: Oct 31, 2021
+ *      Author: mballance
+ */
+
+#include <random>
+#include "RandStateLehmer_32.h"
+
+namespace vsc {
+namespace solvers {
+
+
+RandStateLehmer_32::RandStateLehmer_32(const std::string &seed) : m_seed(seed) {
+    m_state = 1;
+    for (uint32_t i=0; i<seed.size(); i++) {
+        m_state += seed.at(i);
+        m_state ^= 25;
+    }
+}
+
+RandStateLehmer_32::RandStateLehmer_32(const RandStateLehmer_32 &rhs) {
+    m_state = rhs.m_state;
+}
+
+RandStateLehmer_32::~RandStateLehmer_32() {
+
+}
+
+int32_t RandStateLehmer_32::randint32(
+			int32_t		min,
+			int32_t		max) {
+	uint64_t next_v = next_ui64();
+	if (min == max) {
+		return min;
+	} else {
+		next_v = (next_v % (max-min+1)) + min;
+		return next_v;
+	}
+}
+
+uint64_t RandStateLehmer_32::rand_ui64() {
+	return next_ui64();
+}
+
+int64_t RandStateLehmer_32::rand_i64() {
+	return static_cast<int64_t>(next_ui64());
+}
+
+void RandStateLehmer_32::randbits(dm::IModelVal *val) {
+	if (val->bits() <= 64) {
+		uint64_t bits = next_ui64();
+		val->val_u(bits);
+	} else {
+		uint32_t n_words = (val->bits()-1)/64+1;
+		for (uint32_t i=0; i<n_words; i++) {
+			uint64_t rv = next_ui64();
+#ifdef UNDEFINED
+		val.set_word(i, rv);
+
+		if (i+1 < n_words) {
+			i++;
+			val.set_word(i, rv >> 32);
+		}
+
+		if (i+1 == n_words && (val.bits()%32) != 0) {
+			// Mask the last word
+			val.set_word(i,
+					(val.get_word(i) & (1 << (val.bits()%32))-1));
+		}
+#endif
+		}
+	}
+}
+
+uint64_t RandStateLehmer_32::next_ui64() {
+    uint64_t ret;
+    m_state *= 0xda942042e4dd58b5;
+    ret = (m_state >> 32);
+    /*
+    ret <<= 32;
+    m_state *= 0xda942042e4dd58b5;
+    ret |= (m_state >> 32);
+     */
+    return ret;
+}
+
+void RandStateLehmer_32::setState(IRandState *other) {
+	m_state = dynamic_cast<RandStateLehmer_32 *>(other)->m_state;
+}
+
+IRandState *RandStateLehmer_32::clone() const {
+	return new RandStateLehmer_32(*this);
+}
+
+IRandState *RandStateLehmer_32::next() {
+    rand_ui64(); // Mutate state
+
+	// Return a clone
+	return clone(); 
+}
+
+}
+}
diff --git a/src/RandState.h → src/RandStateLehmer_32.h b/src/RandState.h → src/RandStateLehmer_32.h
@@ -1,5 +1,5 @@
 /*
- * RandState.h
+ * RandStateLehmer_32.h
  *
  *  Created on: Oct 31, 2021
  *      Author: mballance
@@ -15,15 +15,13 @@ namespace vsc {
 namespace solvers {
 
 
-class RandState;
-using RandStateUP=std::unique_ptr<RandState>;
-class RandState : public IRandState {
+class RandStateLehmer_32 : public IRandState {
 public:
-	RandState(const std::string &seed);
+	RandStateLehmer_32(const std::string &seed);
 
-	RandState(const std::mt19937_64 &state);
+	RandStateLehmer_32(const RandStateLehmer_32 &rhs);
 
-	virtual ~RandState();
+	virtual ~RandStateLehmer_32();
 
 	virtual const std::string &seed() const override {
 		return m_seed;
@@ -53,7 +51,7 @@ class RandState : public IRandState {
 
 private:
 	std::string			m_seed;
-	std::mt19937_64 	m_state;
+    uint64_t            m_state;
 
 };