From 7b27f2db5d1fdd1bbb1b09cee6be7a6ff5abc4f4 Mon Sep 17 00:00:00 2001
From: Matthew Ballance <matt.ballance@gmail.com>
Date: Mon, 18 Sep 2023 19:08:59 -0700
Subject: [PATCH] XX

Signed-off-by: Matthew Ballance <matt.ballance@gmail.com>
---
 src/SolverBoolectorConstraintBuilder.cpp |  3 +-
 src/SolverBoolectorSetFieldValue.cpp     | 15 ++++++++
 tests/src/TestConstraintsLinear.cpp      | 45 ++++++++++++++++++++++--
 3 files changed, 60 insertions(+), 3 deletions(-)

diff --git a/src/SolverBoolectorConstraintBuilder.cpp b/src/SolverBoolectorConstraintBuilder.cpp
index 50a683a..2c1621d 100644
--- a/src/SolverBoolectorConstraintBuilder.cpp
+++ b/src/SolverBoolectorConstraintBuilder.cpp
@@ -102,7 +102,7 @@ void SolverBoolectorConstraintBuilder::visitDataTypeInt(dm::IDataTypeInt *t) {
 
         if (val.bits() <= 64) {
             char tmp[32];
-            sprintf(tmp, "0x%llx", val.get_val_u());
+            sprintf(tmp, "%llx", val.get_val_u());
             m_expr = {
                 boolector_consth(
                     m_btor,
@@ -358,6 +358,7 @@ void SolverBoolectorConstraintBuilder::visitTypeExprRangelist(dm::ITypeExprRange
 void SolverBoolectorConstraintBuilder::visitTypeExprVal(dm::ITypeExprVal *e) { 
     DEBUG_ENTER("visitTypeExprVal");
     m_val = e->val();
+    e->val().type()->accept(m_this);
 
     DEBUG_LEAVE("visitTypeExprVal");
 }
diff --git a/src/SolverBoolectorSetFieldValue.cpp b/src/SolverBoolectorSetFieldValue.cpp
index 0421443..c0869f2 100644
--- a/src/SolverBoolectorSetFieldValue.cpp
+++ b/src/SolverBoolectorSetFieldValue.cpp
@@ -20,6 +20,7 @@
  */
 #include "boolector/boolector.h"
 #include "dmgr/impl/DebugMacros.h"
+#include "vsc/dm/impl/ValRefInt.h"
 #include "vsc/solvers/impl/TaskPath2ValRef.h"
 #include "vsc/solvers/impl/TaskPath2Field.h"
 #include "SolverBoolectorSetFieldValue.h"
@@ -47,6 +48,7 @@ void SolverBoolectorSetFieldValue::set(
     DEBUG_ENTER("set");
     m_node = node;
     dm::ITypeField *field = TaskPath2Field(m_root_field).toField(path);
+    DEBUG("Field: %s", field->name().c_str());
     m_val = TaskPath2ValRef(m_root_field).toMutVal(path);
     field->getDataType()->accept(m_this);
     DEBUG_LEAVE("set");
@@ -71,6 +73,19 @@ void SolverBoolectorSetFieldValue::visitDataTypeInt(dm::IDataTypeInt *t) {
         m_btor, 
         boolector_get_value(m_btor, m_node));
     DEBUG("bits: %s\n", bits);
+    if (t->width() <= 64) {
+        uint64_t val = 0;
+        dm::ValRefInt val_i(m_val);
+
+        for (uint32_t i=0; i<t->width() && bits[i]; i++) {
+            val <<= 1;
+            val |= (bits[i] == '1');
+        }
+
+        val_i.set_val(val);
+    } else {
+        // TODO:
+    }
     boolector_free_bits(m_btor, bits);
 
     DEBUG_LEAVE("visitDataTypeInt");
diff --git a/tests/src/TestConstraintsLinear.cpp b/tests/src/TestConstraintsLinear.cpp
index a883c54..97be473 100644
--- a/tests/src/TestConstraintsLinear.cpp
+++ b/tests/src/TestConstraintsLinear.cpp
@@ -42,10 +42,12 @@ TEST_F(TestConstraintsLinear, ult_2var) {
 
             @vdc.constraint
             def ab_c(self):
+                self.a < 15
+                self.b < 15
                 self.a < self.b
     )");
     #include "TestConstraintsLinear_ult_2var.h"
-    enableDebug(true);
+    enableDebug(false);
 
     vsc::dm::IModelFieldUP field(mkRootField("abc", MyC_t));
 
@@ -54,7 +56,46 @@ TEST_F(TestConstraintsLinear, ult_2var) {
     RefPathSet target_fields, fixed_fields, include_constraints, exclude_constraints;
     SolveFlags flags = SolveFlags::NoFlags;
 
-    for (uint32_t i=0; i<10; i++) {
+    for (uint32_t i=0; i<3000; i++) {
+        solver->randomize(
+            randstate.get(),
+            field.get(),
+            target_fields,
+            fixed_fields,
+            include_constraints,
+            exclude_constraints,
+            flags);
+        dm::ValRefStruct field_v(field->getImmVal());
+        dm::ValRefInt val_a(field_v.getField(0));
+        dm::ValRefInt val_b(field_v.getField(1));
+        ASSERT_LT(val_a.get_val_u(), val_b.get_val_u());
+    }
+}
+
+TEST_F(TestConstraintsLinear, ult_2var_8bit) {
+    VSC_DATACLASSES(TestConstraintsLinear_ult_2var_8bit, MyC, R"(
+        @vdc.randclass
+        class MyC(object):
+            a : vdc.rand_uint8_t 
+            b : vdc.rand_uint8_t 
+
+            @vdc.constraint
+            def ab_c(self):
+                self.a < 15
+                self.b < 15
+                self.a < self.b
+    )");
+    #include "TestConstraintsLinear_ult_2var_8bit.h"
+    enableDebug(false);
+
+    vsc::dm::IModelFieldUP field(mkRootField("abc", MyC_t));
+
+    IRandStateUP randstate(m_factory->mkRandState("0"));
+    ICompoundSolverUP solver(m_factory->mkCompoundSolver());
+    RefPathSet target_fields, fixed_fields, include_constraints, exclude_constraints;
+    SolveFlags flags = SolveFlags::NoFlags;
+
+    for (uint32_t i=0; i<3000; i++) {
         solver->randomize(
             randstate.get(),
             field.get(),