Add datatype support for z3 (#346)

.gitignore

@@ -42,3 +42,5 @@ deps/CVC4/
 deps/
 
 local/
+.cache/
+.vscode/

contrib/setup-z3.sh

@@ -1,13 +1,21 @@
 #!/bin/bash
 set -e
 
-Z3_VERSION=6cc52e04c3ea7e2534644a285d231bdaaafd8714
+Z3_VERSION=z3-4.12.6
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps
 
 mkdir -p $DEPS
 
+if [ "$(uname)" == "Darwin" ]; then
+    NUM_CORES=$(sysctl -n hw.logicalcpu)
+elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+    NUM_CORES=$(nproc)
+else
+    NUM_CORES=1
+fi
+
 if [ ! -d "$DEPS/z3" ]; then
     cd $DEPS
     git clone https://github.com/Z3Prover/z3.git
@@ -18,10 +26,19 @@ if [ ! -d "$DEPS/z3" ]; then
     # a pthread related issue
     # compiling with --single-threaded helps, but isn't a real solution
     # see https://github.com/Z3Prover/z3/issues/4554
-    ./configure --staticlib --single-threaded
-    cd build
-    make -j$(nproc)
+    cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_LIBZ3_SHARED=Off -DZ3_BUILD_LIBZ3_MSVC_STATIC=On
+    cmake --build build -j$NUM_CORES
     cd $DIR
 else
     echo "$DEPS/z3 already exists. If you want to rebuild, please remove it manually."
 fi
+
+if [ -f $DEPS/z3/build/libz3.a ]; then
+    echo "It appears z3 was setup successfully into $DEPS/z3."
+    echo "You may now install it with make ./configure.sh --z3 && cd build && make"
+else
+    echo "Building z3 failed."
+    echo "You might be missing some dependencies."
+    echo "Please see their github page for installation instructions: https://github.com/z3/z3"
+    exit 1
+fi

src/solver_enums.cpp

@@ -108,6 +108,7 @@ const unordered_map<SolverEnum, unordered_set<SolverAttribute>>
             ARRAY_FUN_BOOLS,
             CONSTARR,
             UNSAT_CORE,
+            THEORY_DATATYPE,
             QUANTIFIERS,
             UNINTERP_SORT,
             TIMELIMIT } },

tests/z3/z3_test.cpp

@@ -32,6 +32,18 @@ int main()
       FUNCTION, SortVec{ boolsort1, intsort1, realsort1, boolsort1 });
   cout << functionsort << endl;
 
+  DatatypeDecl listSpec = s->make_datatype_decl("list");
+  DatatypeConstructorDecl nildecl = s->make_datatype_constructor_decl("nil");
+  DatatypeConstructorDecl consdecl = s->make_datatype_constructor_decl("cons");
+  s->add_selector(consdecl, "head", s->make_sort(INT));
+  s->add_selector_self(consdecl, "tail");
+  s->add_constructor(listSpec, nildecl);
+  s->add_constructor(listSpec, consdecl);
+  Sort listsort = s->make_sort(listSpec);
+  z3::sort sort = std::static_pointer_cast<Z3Sort>(listsort)->get_z3_type();
+  cout << sort << endl
+       << sort.constructors() << endl
+       << sort.recognizers() << endl;
   cout << "* * * end sort testing * * *" << endl
        << "* * * basic term testing * * *" << endl;
 

z3/CMakeLists.txt

@@ -4,6 +4,7 @@ add_library(smt-switch-z3 "${SMT_SWITCH_LIB_TYPE}"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_solver.cpp"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_sort.cpp"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_term.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_datatype.cpp"
   )
 
 target_include_directories (smt-switch-z3 PUBLIC "${PROJECT_SOURCE_DIR}/include")

z3/include/z3_datatype.h

@@ -0,0 +1,62 @@
+#pragma once
+#include "z3++.h"
+#include "datatype.h"
+#include "exceptions.h"
+
+namespace smt {
+
+class Z3DatatypeDecl : public AbsDatatypeDecl
+{
+ public:
+  Z3DatatypeDecl(std::string name) : name(name){};
+
+ protected:
+  friend class Z3Solver;
+  std::string name;
+  std::vector<DatatypeConstructorDecl> consvec {};
+};
+
+class Z3DatatypeConstructorDecl : public AbsDatatypeConstructorDecl
+{
+ public:
+  Z3DatatypeConstructorDecl(z3::context & c, std::string name)
+      : c(c), constructorname(name){};
+  bool compare(const DatatypeConstructorDecl &) const override;
+
+ protected:
+  friend class Z3Solver;
+
+  z3::context & c;
+  std::string constructorname, datatypename;
+  std::vector<z3::symbol> fieldnames {};
+  std::vector<z3::sort> sorts {};
+};
+
+class Z3Datatype : public AbsDatatype
+{
+ public:
+  Z3Datatype(z3::context & c, z3::sort s) : c(c), datatype(s) {}
+  std::string get_name() const override { return datatype.name().str(); }
+  int get_num_constructors() const override
+  {
+    return Z3_get_datatype_sort_num_constructors(c, datatype);
+  }
+  int get_num_selectors(std::string name) const override
+  {
+    for (size_t i = 0; i < get_num_constructors(); i++)
+    {
+      z3::func_decl cons{ c, Z3_get_datatype_sort_constructor(c, datatype, i) };
+      if (cons.name().str() == name) return cons.arity();
+    }
+    throw InternalSolverException(datatype.name().str() + "." + name
+                                  + " not found");
+  }
+
+ private:
+  z3::context & c;
+
+  z3::sort datatype;
+  friend class Z3Solver;
+};
+
+}  // namespace smt

z3/include/z3_solver.h

@@ -26,6 +26,7 @@
 #include "result.h"
 #include "smt.h"
 #include "sort.h"
+#include "z3_datatype.h"
 #include "z3_sort.h"
 #include "z3_term.h"
 
@@ -75,6 +76,8 @@ class Z3Solver : public AbsSmtSolver
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
   Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
+  SortVec make_datatype_sorts(
+      const std::vector<DatatypeDecl> & decls) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
   DatatypeConstructorDecl make_datatype_constructor_decl(
@@ -153,5 +156,6 @@ class Z3Solver : public AbsSmtSolver
       throw NotImplementedException("Unimplemented result type from Z3");
     }
   }
+  void add_constructor(z3::sort, z3::constructors*, const DatatypeConstructorDecl&) const;
 };
 }  // namespace smt

z3/src/z3_datatype.cpp

@@ -0,0 +1,23 @@
+#include "z3_datatype.h"
+
+namespace z3 {
+const bool operator==(const z3::sort & lhs, const z3::sort & rhs)
+{
+  return z3::eq(lhs, rhs);
+}
+const bool operator==(const z3::symbol & lhs, const z3::symbol & rhs)
+{
+  return lhs.str() == rhs.str();
+}
+}  // namespace z3
+
+namespace smt {
+bool Z3DatatypeConstructorDecl::compare(
+    const DatatypeConstructorDecl & other) const
+{
+  auto cast = std::static_pointer_cast<Z3DatatypeConstructorDecl>(other);
+  return std::tie(constructorname, fieldnames, sorts)
+         == std::tie(cast->constructorname, cast->fieldnames, cast->sorts);
+}
+
+}  // namespace smt