test to see the changes

CMakeLists.txt

@@ -112,6 +112,7 @@ option(ENABLE_PROFILING        "Enable support for gprof profiling")
 #    > for options where we don't need to detect if set by user (default: OFF)
 option(USE_CLN           "Use CLN instead of GMP")
 option(USE_COCOA         "Use CoCoALib for further polynomial operations")
+option(USE_SINGULAR      "Use Singular for further polynomial operations")
 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 option(USE_EDITLINE      "Use Editline for better interactive support")
 option(USE_GLPK          "Use GLPK simplex solver")
@@ -489,6 +490,11 @@ if(USE_COCOA)
   add_definitions(-DCVC5_USE_COCOA)
 endif()
 
+if(USE_SINGULAR)
+  find_package(SINGULAR REQUIRED)
+  add_definitions(-DCVC5_USE_SINGULAR)
+endif()
+
 if(USE_EDITLINE)
   find_package(Editline REQUIRED)
   set(HAVE_LIBEDITLINE 1)
@@ -690,6 +696,7 @@ print_config("GLPK                      " ${USE_GLPK})
 print_config("Kissat                    " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM})
 print_config("LibPoly                   " ${USE_POLY} FOUND_SYSTEM ${Poly_FOUND_SYSTEM})
 print_config("CoCoALib                  " ${USE_COCOA} FOUND_SYSTEM ${CoCoA_FOUND_SYSTEM})
+print_config("SingularLib               " ${USE_SINGULAR} FOUND_SYSTEM ${SINGULAR_FOUND_SYSTEM})
 
 if(CVC5_USE_CLN_IMP)
   print_config("MP library                " "cln" FOUND_SYSTEM ${CLN_FOUND_SYSTEM})

analyze.py

@@ -0,0 +1,21 @@
+import pandas as pd 
+import sys 
+
+
+
+if __name__ == "__main__":
+    if len(sys.argv) != 2:
+        print("Usage: python script.py <filename>")
+        sys.exit(1)
+    filename = sys.argv[1]
+    with open(filename, "r") as file:
+    # Read entire file contents
+        file_contents = file.read()
+    file_contents = file_contents.split("\n")[:-1]
+    print(file_contents)
+    unsat = 0
+    for i in file_contents:
+        if "unsat" in i:
+            unsat +=1
+    print("Unsat ", unsat, "out of ", len(file_contents))
+

cmake/ConfigureCvc5.cmake

@@ -83,10 +83,10 @@ check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
 check_symbol_exists(setitimer "sys/time.h" HAVE_SETITIMER)
 
 # on non-POSIX systems, time limit is implemented with threads
-if(NOT HAVE_SETITIMER)
-  find_package(Threads REQUIRED)
-  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_THREAD_LIBS_INIT}")
-endif()
+#if(NOT HAVE_SETITIMER)
+find_package(Threads REQUIRED)
+set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_THREAD_LIBS_INIT}")
+ #endif()
 
 # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
 check_c_source_compiles(

include/cvc5/cvc5.h

@@ -3517,6 +3517,7 @@ class CVC5_EXPORT Solver
    */
   Sort mkFiniteFieldSort(const std::string& size, uint32_t base = 10) const;
 
+  Sort mkIntegerRingSort() const;
   /**
    * Create a datatype sort.
    * @param dtypedecl The datatype declaration from which the sort is created.
@@ -3982,6 +3983,9 @@ class CVC5_EXPORT Solver
                          const Sort& sort,
                          uint32_t base = 10) const;
 
+  Term mkIntegerRingElem(const std::string& value,
+                         uint32_t base = 10) const;
+
   /**
    * Create a constant array with the provided constant value stored at every
    * index.

include/cvc5/cvc5_kind.h

@@ -2030,6 +2030,19 @@ enum ENUM(Kind) : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    */
   EVALUE(FINITE_FIELD_BITSUM),
+  /**
+   * Less than one integer and greater than or equal to zero: 0 <= x < y.
+   *
+   * - Arity: ``n = 2``
+   *
+   *   - ``1..n:`` Terms of finite field Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   */
+  EVALUE(FINITE_FIELD_LT),
   /**
    * Multiplication of two or more finite field elements.
    *
@@ -2048,6 +2061,16 @@ enum ENUM(Kind) : int32_t
    */
   EVALUE(FINITE_FIELD_MULT),
 
+  EVALUE(INTEGER_RING_MULT),
+
+  EVALUE(INTEGER_RING_ADD),
+
+  EVALUE(INTEGER_RING_EQ),
+
+  EVALUE(INTEGER_RING_LT),
+
+
+  EVALUE(CONST_INTEGER_RING),
   /* FP -------------------------------------------------------------------- */
 
   /**
@@ -5870,6 +5893,16 @@ enum ENUM(SortKind) : int32_t
    *   - Solver::mkFiniteFieldSort(const std::string&, uint32_t base) const
    */
   EVALUE(FINITE_FIELD_SORT),
+
+  /**
+   * A finite field sort, parameterized by a size.
+   *
+   * - Create Sort of this Kind with:
+   *
+   *   - Solver::mkIntegerRingSort() const
+   */
+
+  EVALUE(INTEGER_RING_SORT),
   /**
    * A floating-point sort, parameterized by two integers denoting its
    * exponent and significand bit-widths.

run_ff.sh

@@ -0,0 +1,56 @@
+#!/bin/bash
+
+# Check if at least three arguments are provided
+if [ "$#" -lt 3 ]; then
+    echo "Usage: $0 <path_to_cvc5> <TEST_DIR> <output_file> [cvc5_options...]"
+    exit 1
+fi
+
+# Extract the arguments
+CVC5=$1
+TEST_DIR=$2
+output_file=$3
+shift 3  # Remove the first three arguments from the list
+
+# The remaining arguments are options for cvc5
+CVC5_OPTIONS="$@"
+solved=0
+total=0
+
+# Create or clear the output file
+if [ ! -f "$output_file" ]; then
+    touch "$output_file"
+else
+    > "$output_file"
+fi
+
+# Add CSV headers
+echo "Filename,Result,Global Time (ms)" > "$output_file"
+
+# Find all files in the directory (including nested directories) that contain 'smt' in their names
+find "$TEST_DIR" -type f -name '*smt*' | while read -r file; do
+    total=$((total+1))
+
+    echo $file
+
+    # Run cvc5 and capture both stdout and stderr in one go
+    output=$( gtimeout --signal=SIGTERM --kill-after=5s 130s  "$CVC5" --tlimit 1200000 $CVC5_OPTIONS --stats  "$file" 2>&1 )
+
+    echo "Finished cvc5"
+
+    # Extract the last line (result) from stdout (assuming unsat/sat is in stdout)
+    result=$(echo "$output" | grep -v 'global::totalTime' | tail -n 5 | head -n 1)
+
+    echo "finished first grep"
+
+    # Extract the global::totalTime from stderr
+    global_time=$(echo "$output" | awk '/global::totalTime/ {print $NF}' || echo "timeout")
+
+     echo "finished second grep"
+
+    # Write filename, result, and global time to the CSV file
+    echo "$file,$result,$global_time" >> "$output_file"
+done 
+
+# Analyze the results
+python3 analyze.py "$output_file"

src/CMakeLists.txt

@@ -126,6 +126,8 @@ libcvc5_add_sources(
   preprocessing/passes/theory_preprocess.h
   preprocessing/passes/unconstrained_simplifier.cpp
   preprocessing/passes/unconstrained_simplifier.h
+  preprocessing/passes/int_range_or.cpp
+  preprocessing/passes/int_range_or.h
   preprocessing/preprocessing_pass.cpp
   preprocessing/preprocessing_pass.h
   preprocessing/preprocessing_pass_context.cpp
@@ -553,6 +555,16 @@ libcvc5_add_sources(
   theory/arrays/theory_arrays_type_rules.h
   theory/arrays/type_enumerator.h
   theory/arrays/type_enumerator.cpp
+  theory/arith/modular/range-solver.h
+  theory/arith/modular/range-solver.cpp
+  theory/arith/modular/int_cocoa_encoder.h
+  theory/arith/modular/int_cocoa_encoder.cpp
+  theory/arith/modular/cocoa_util.h
+  theory/arith/modular/cocoa_util.cpp
+  theory/arith/modular/util.h
+  theory/arith/modular/util.cpp
+  theory/arith/modular/gb_simplify.h
+  theory/arith/modular/gb_simplify.cpp
   theory/assertion.cpp
   theory/assertion.h
   theory/atom_requests.cpp
@@ -711,10 +723,14 @@ libcvc5_add_sources(
   theory/ff/multi_roots.h
   theory/ff/parse.cpp
   theory/ff/parse.h
+  theory/ff/singular_parse.cpp
+  theory/ff/singular_parse.h
   theory/ff/split_gb.cpp
   theory/ff/split_gb.h
   theory/ff/stats.cpp
   theory/ff/stats.h
+  theory/ff/range_solver_ff.cpp
+  theory/ff/range_solver_ff.h
   theory/ff/sub_theory.cpp
   theory/ff/sub_theory.h
   theory/ff/theory_ff.cpp
@@ -1518,3 +1534,5 @@ endif()
 # Thus, we can only visit main as soon as all dependencies for cvc5 are set up.
 
 add_subdirectory(main)
+
+#configure_file("theory/arith/modular/gb_input.txt",${CMAKE_BINARY_DIR}"/theory/arith/modular/gb_input.txt" )

src/api/cpp/cvc5.cpp

@@ -76,6 +76,7 @@
 #include "util/bitvector.h"
 #include "util/divisible.h"
 #include "util/finite_field_value.h"
+#include "util/integer_ring_value.h"
 #include "util/floatingpoint.h"
 #include "util/iand.h"
 #include "util/random.h"
@@ -239,6 +240,11 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
         KIND_ENUM(Kind::CONST_FINITE_FIELD, internal::Kind::CONST_FINITE_FIELD),
         KIND_ENUM(Kind::FINITE_FIELD_BITSUM,
                   internal::Kind::FINITE_FIELD_BITSUM),
+        KIND_ENUM(Kind::FINITE_FIELD_LT, internal::Kind::FINITE_FIELD_LT),
+        KIND_ENUM(Kind::INTEGER_RING_LT, internal::Kind::INTEGER_RING_LT),
+        KIND_ENUM(Kind::INTEGER_RING_MULT, internal::Kind::INTEGER_RING_MULT),
+        KIND_ENUM(Kind::INTEGER_RING_ADD, internal::Kind::INTEGER_RING_ADD),
+        KIND_ENUM(Kind::INTEGER_RING_EQ, internal::Kind::INTEGER_RING_EQ),
         KIND_ENUM(Kind::FINITE_FIELD_MULT, internal::Kind::FINITE_FIELD_MULT),
         KIND_ENUM(Kind::FINITE_FIELD_ADD, internal::Kind::FINITE_FIELD_ADD),
         KIND_ENUM(Kind::FINITE_FIELD_NEG, internal::Kind::FINITE_FIELD_NEG),
@@ -628,6 +634,7 @@ const static std::unordered_map<internal::Kind,
         /* Finite Fields --------------------------------------------------- */
         {internal::Kind::CONST_FINITE_FIELD, Kind::CONST_FINITE_FIELD},
         {internal::Kind::FINITE_FIELD_BITSUM, Kind::FINITE_FIELD_BITSUM},
+        {internal::Kind::FINITE_FIELD_LT, Kind::FINITE_FIELD_LT},
         {internal::Kind::FINITE_FIELD_MULT, Kind::FINITE_FIELD_MULT},
         {internal::Kind::FINITE_FIELD_ADD, Kind::FINITE_FIELD_ADD},
         {internal::Kind::FINITE_FIELD_NEG, Kind::FINITE_FIELD_NEG},
@@ -5565,6 +5572,16 @@ Sort Solver::mkFiniteFieldSort(const std::string& modulus, uint32_t base) const
   CVC5_API_TRY_CATCH_END;
 }
 
+Sort Solver::mkIntegerRingSort() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return Sort(d_nm, d_nm->mkIntegerRingType());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+
 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -6035,6 +6052,23 @@ Term Solver::mkFiniteFieldElem(const std::string& value,
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::mkIntegerRingElem(const std::string& value,
+                               uint32_t base) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  //internal::Integer v(value, base);
+  internal::Integer v(value, base);
+  internal::IntegerRingValue ir(v);
+  //internal::Node res = d_nm->mkConst(v);
+  //(void)res.getType(true); /* kick off type checking */
+  //return Term(d_nm, res);
+  return mkValHelper<internal::IntegerRingValue>(d_nm, ir);
+
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::mkConstArray(const Sort& sort, const Term& val) const
 {
   CVC5_API_TRY_CATCH_BEGIN;

src/expr/node_manager_template.cpp

@@ -210,6 +210,11 @@ TypeNode NodeManager::mkFiniteFieldType(const Integer& modulus)
                                            FfSize(modulus));
 }
 
+TypeNode NodeManager::mkIntegerRingType()
+{
+  return mkConstInternal<TypeNode, TypeConstant>(Kind::TYPE_CONSTANT, INTEGER_RING_TYPE);
+}
+
 TypeNode NodeManager::sExprType()
 {
   return mkConstInternal<TypeNode, TypeConstant>(Kind::TYPE_CONSTANT,

src/expr/node_manager_template.h

@@ -453,6 +453,9 @@ class NodeManager
   /** Make the type of finite field elements modulo <code>modulus</code> */
   TypeNode mkFiniteFieldType(const Integer& modulus);
 
+  /** Make the type of Integer for finite field theory */
+  TypeNode mkIntegerRingType();
+
   /** Make the type of arrays with the given parameterization */
   TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 

src/options/arith_options.toml

@@ -598,3 +598,19 @@ name   = "Arithmetic Theory"
   type       = "bool"
   default    = "true"
   help       = "do arithmetic static learning for ite terms based on bounds when static learning is enabled"
+
+[[option]]
+  name       = "modularRangeSolver"
+  category   = "regular"
+  long       = "mod-range-solver"
+  type       = "bool"
+  default    = "false"
+  help       = "solve modular arithmetic using range solver"
+
+[[option]]
+  name       = "intRangeOr"
+  category   = "regular"
+  long       = "int-range-or"
+  type       = "bool"
+  default    = "false"
+  help       = "solve modular arithmetic using range solver"

src/options/ff_options.toml

@@ -32,6 +32,15 @@ name   = "Finite Field Theory"
   type       = "bool"
   default    = "false"
   help       = "parse bitsums"
+
+[[option]]
+  name       = "ffRangeSolver"
+  category   = "expert"
+  long       = "ff-range-solver"
+  type       = "bool"
+  default    = "false"
+  help       = "Solve using the range solver"
+
 [[option]]
   name       = "ffSolver"
   category   = "expert"

src/parser/smt2/smt2_lexer.cpp

@@ -172,6 +172,13 @@ Token Smt2Lexer::computeNextToken()
             parseError("Error expected decimal for finite field size");
           }
           return Token::FIELD_LITERAL;
+        case 'z':
+          pushToToken(ch);
+          if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
+          {
+            parseError("Error expected decimal for finite field value");
+          }
+          return Token::INTEGER_RING_LITERAL;
         default:
           // otherwise error
           parseError("Error finding token following #");