Merge branch 'main' into updateAlethe0

.github/actions/run-tests/action.yml

@@ -56,7 +56,7 @@ runs:
         cd examples
         mkdir -p build && cd build
         if [[ "$RUNNER_OS" == "Windows" ]]; then
-          export PATH="${{ inputs.build-dir }}/install/lib:$PATH"
+          export PATH="${{ inputs.build-dir }}/install/bin:$PATH"
           export CMAKE_GENERATOR="MSYS Makefiles"
         fi
         cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake \

cmake/FindPoly.cmake

@@ -237,8 +237,8 @@ else()
 
   ExternalProject_Get_Property(Poly-EP BUILD_BYPRODUCTS INSTALL_DIR)
   string(REPLACE "<INSTALL_DIR>" "${INSTALL_DIR}" BUILD_BYPRODUCTS "${BUILD_BYPRODUCTS}")
-  install(FILES
-    ${BUILD_BYPRODUCTS}
-    DESTINATION ${CMAKE_INSTALL_LIBDIR}
-  )
+  # Only install shared libraries
+  if (BUILD_SHARED_LIBS)
+    install(FILES ${BUILD_BYPRODUCTS} TYPE ${LIB_BUILD_TYPE})
+  endif()
 endif()

cmake/deps-helper.cmake

@@ -39,6 +39,13 @@ if(CMAKE_VERSION VERSION_GREATER_EQUAL "3.14")
     )
 endif()
 
+# On Windows, DLL libraries are runtime artifacts
+if(BUILD_SHARED_LIBS AND WIN32)
+  set(LIB_BUILD_TYPE BIN)
+else()
+  set(LIB_BUILD_TYPE LIB)
+endif()
+
 # On Windows, we need to have a shell interpreter to call 'configure'
 if(CMAKE_SYSTEM_NAME STREQUAL "Windows")
     find_program (SHELL "sh" REQUIRED)

include/cvc5/cvc5_kind.h

@@ -3555,6 +3555,38 @@ enum ENUM(Kind) : int32_t
    *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   EVALUE(RELATION_JOIN),
+   /**
+   * \rst
+   *  Table join operator for relations has the form
+   *  :math:`((\_ \; rel.table\_join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)`
+   *  where :math:`m_1 \; n_1 \; \dots \; m_k \; n_k` are natural numbers,
+   *  and :math:`A, B` are relations.
+   *  This operator filters the product of two sets based on the equality of
+   *  projected tuples using indices :math:`m_1, \dots, m_k` in relation :math:`A`,
+   *  and indices :math:`n_1, \dots, n_k` in relation :math:`B`.
+   *
+   * - Arity: ``2``
+   *
+   *   - ``1:`` Term of relation Sort
+   *
+   *   - ``2:`` Term of relation Sort
+   *
+   * - Indices: ``n``
+   *   - ``1..n:``  Indices of the projection
+   *
+   * \endrst
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+   *
+   * \rst
+   * .. warning:: This kind is experimental and may be changed or removed in
+   *              future versions.
+   * \endrst
+   */
+  EVALUE(RELATION_TABLE_JOIN),
   /**
    * Relation cartesian product.
    *

src/CMakeLists.txt

@@ -148,6 +148,8 @@ libcvc5_add_sources(
   printer/smt2/smt2_printer.h
   proof/alf/alf_dependent_type_converter.cpp
   proof/alf/alf_dependent_type_converter.h
+  proof/alf/alf_list_node_converter.cpp
+  proof/alf/alf_list_node_converter.h
   proof/alf/alf_node_converter.cpp
   proof/alf/alf_node_converter.h
   proof/alf/alf_print_channel.cpp
@@ -1454,10 +1456,9 @@ target_include_directories(cvc5
     $<BUILD_INTERFACE:${PROJECT_SOURCE_DIR}/include:${CMAKE_BINARY_DIR}/include>
     $<INSTALL_INTERFACE:include>
 )
-install(TARGETS cvc5
-  EXPORT cvc5-targets
-  DESTINATION ${CMAKE_INSTALL_LIBDIR}
-)
+# On Windows, CMake's default install action places
+# DLLs into the runtime path (by default "bin")
+install(TARGETS cvc5 EXPORT cvc5-targets)
 
 if(BUILD_SHARED_LIBS)
   set_target_properties(cvc5 PROPERTIES SOVERSION ${CVC5_SOVERSION})

src/api/cpp/cvc5.cpp

@@ -340,6 +340,8 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
         KIND_ENUM(Kind::SET_FOLD, internal::Kind::SET_FOLD),
         /* Relations -------------------------------------------------------- */
         KIND_ENUM(Kind::RELATION_JOIN, internal::Kind::RELATION_JOIN),
+        KIND_ENUM(Kind::RELATION_TABLE_JOIN,
+                  internal::Kind::RELATION_TABLE_JOIN),
         KIND_ENUM(Kind::RELATION_PRODUCT, internal::Kind::RELATION_PRODUCT),
         KIND_ENUM(Kind::RELATION_TRANSPOSE, internal::Kind::RELATION_TRANSPOSE),
         KIND_ENUM(Kind::RELATION_TCLOSURE, internal::Kind::RELATION_TCLOSURE),
@@ -735,6 +737,8 @@ const static std::unordered_map<internal::Kind,
         {internal::Kind::SET_FOLD, Kind::SET_FOLD},
         /* Relations ------------------------------------------------------- */
         {internal::Kind::RELATION_JOIN, Kind::RELATION_JOIN},
+        {internal::Kind::RELATION_TABLE_JOIN, Kind::RELATION_TABLE_JOIN},
+        {internal::Kind::RELATION_TABLE_JOIN_OP, Kind::RELATION_TABLE_JOIN},
         {internal::Kind::RELATION_PRODUCT, Kind::RELATION_PRODUCT},
         {internal::Kind::RELATION_TRANSPOSE, Kind::RELATION_TRANSPOSE},
         {internal::Kind::RELATION_TCLOSURE, Kind::RELATION_TCLOSURE},
@@ -905,6 +909,7 @@ const static std::unordered_map<Kind, internal::Kind> s_op_kinds{
     {Kind::RELATION_AGGREGATE, internal::Kind::RELATION_AGGREGATE_OP},
     {Kind::RELATION_GROUP, internal::Kind::RELATION_GROUP_OP},
     {Kind::RELATION_PROJECT, internal::Kind::RELATION_PROJECT_OP},
+    {Kind::RELATION_TABLE_JOIN, internal::Kind::RELATION_TABLE_JOIN_OP},
     {Kind::TABLE_PROJECT, internal::Kind::TABLE_PROJECT_OP},
     {Kind::TABLE_AGGREGATE, internal::Kind::TABLE_AGGREGATE_OP},
     {Kind::TABLE_JOIN, internal::Kind::TABLE_JOIN_OP},
@@ -2131,6 +2136,7 @@ size_t Op::getNumIndicesHelper() const
     case Kind::RELATION_AGGREGATE:
     case Kind::RELATION_GROUP:
     case Kind::RELATION_PROJECT:
+    case Kind::RELATION_TABLE_JOIN:
     case Kind::TABLE_AGGREGATE:
     case Kind::TABLE_GROUP:
     case Kind::TABLE_JOIN:
@@ -2302,6 +2308,7 @@ Term Op::getIndexHelper(size_t index)
     case Kind::RELATION_AGGREGATE:
     case Kind::RELATION_GROUP:
     case Kind::RELATION_PROJECT:
+    case Kind::RELATION_TABLE_JOIN:
     case Kind::TABLE_AGGREGATE:
     case Kind::TABLE_GROUP:
     case Kind::TABLE_JOIN:
@@ -5898,6 +5905,7 @@ Op TermManager::mkOp(Kind kind, const std::vector<uint32_t>& args)
     case Kind::RELATION_AGGREGATE:
     case Kind::RELATION_GROUP:
     case Kind::RELATION_PROJECT:
+    case Kind::RELATION_TABLE_JOIN:
     case Kind::TABLE_AGGREGATE:
     case Kind::TABLE_GROUP:
     case Kind::TABLE_JOIN:

src/expr/node_algorithm.cpp

@@ -704,7 +704,7 @@ bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
     visited.insert(curr);
     if (curr.first.getNumChildren() == 0)
     {
-      if (curr.first.getType() != curr.second.getType())
+      if (!curr.first.getType().isComparableTo(curr.second.getType()))
       {
         // the two subterms have different types
         return false;

src/options/proof_options.toml

@@ -219,3 +219,29 @@ name   = "Proof"
   type       = "bool"
   default    = "false"
   help       = "Print the DRAT proof in binary format"
+
+[[option]]
+  name       = "satProofMinDimacs"
+  category   = "expert"
+  long       = "sat-proof-min-dimacs"
+  type       = "bool"
+  default    = "true"
+  help       = "Minimize the DIMACs emitted when prop-proof-mode is set to sat-external-prove"
+
+[[option]]
+  name       = "propProofMode"
+  category   = "regular"
+  long       = "prop-proof-mode=MODE"
+  type       = "PropProofMode"
+  default    = "PROOF"
+  help       = "modes for proof granularity"
+  help_mode  = "Modes for proof granularity."
+[[option.mode.PROOF]]
+  name = "proof"
+  help = "A proof computed by the SAT solver."
+[[option.mode.SAT_EXTERNAL_PROVE]]
+  name = "sat-external-prove"
+  help = "A proof containing a step that will be proven externally."
+[[option.mode.SKETCH]]
+  name = "sketch"
+  help = "A sketch given by the SAT solver."

src/parser/CMakeLists.txt

@@ -82,9 +82,9 @@ endif()
 set_target_properties(cvc5parser PROPERTIES OUTPUT_NAME cvc5parser)
 target_link_libraries(cvc5parser PRIVATE cvc5)
 
-install(TARGETS cvc5parser
-  EXPORT cvc5-targets
-  DESTINATION ${CMAKE_INSTALL_LIBDIR})
+# On Windows, CMake's default install action places
+# DLLs into the runtime path (by default "bin")
+install(TARGETS cvc5parser EXPORT cvc5-targets)
 
 # The generated lexer/parser files define some functions as
 # __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of

src/parser/smt2/smt2_state.cpp

@@ -867,6 +867,7 @@ void Smt2State::setLogic(std::string name)
     addOperator(Kind::SET_FILTER, "set.filter");
     addOperator(Kind::SET_FOLD, "set.fold");
     addOperator(Kind::RELATION_JOIN, "rel.join");
+    addOperator(Kind::RELATION_TABLE_JOIN, "rel.table_join");
     addOperator(Kind::RELATION_PRODUCT, "rel.product");
     addOperator(Kind::RELATION_TRANSPOSE, "rel.transpose");
     addOperator(Kind::RELATION_TCLOSURE, "rel.tclosure");
@@ -877,6 +878,7 @@ void Smt2State::setLogic(std::string name)
     addOperator(Kind::RELATION_AGGREGATE, "rel.aggr");
     addOperator(Kind::RELATION_PROJECT, "rel.project");
     addIndexedOperator(Kind::RELATION_GROUP, "rel.group");
+    addIndexedOperator(Kind::RELATION_TABLE_JOIN, "rel.table_join");
     addIndexedOperator(Kind::RELATION_AGGREGATE, "rel.aggr");
     addIndexedOperator(Kind::RELATION_PROJECT, "rel.project");
     // set.comprehension is a closure kind
@@ -1332,7 +1334,8 @@ Term Smt2State::applyParseOp(const ParseOp& p, std::vector<Term>& args)
       if (kind == Kind::TUPLE_PROJECT || kind == Kind::TABLE_PROJECT
           || kind == Kind::TABLE_AGGREGATE || kind == Kind::TABLE_JOIN
           || kind == Kind::TABLE_GROUP || kind == Kind::RELATION_GROUP
-          || kind == Kind::RELATION_AGGREGATE || kind == Kind::RELATION_PROJECT)
+          || kind == Kind::RELATION_AGGREGATE || kind == Kind::RELATION_PROJECT
+          || kind == Kind::RELATION_TABLE_JOIN)
       {
         std::vector<uint32_t> indices;
         Op op = d_tm.mkOp(kind, indices);

src/preprocessing/passes/static_rewrite.cpp

@@ -15,6 +15,7 @@
 
 #include "preprocessing/passes/static_rewrite.h"
 
+#include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "theory/theory_engine.h"
@@ -25,9 +26,18 @@ namespace cvc5::internal {
 namespace preprocessing {
 namespace passes {
 
-StaticRewrite::StaticRewrite(
-    PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "static-rewrite"){};
+StaticRewrite::StaticRewrite(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "static-rewrite")
+{
+  if (options().smt.produceProofs)
+  {
+    d_tpg.reset(new TConvProofGenerator(d_env,
+                                        userContext(),
+                                        TConvPolicy::FIXPOINT,
+                                        TConvCachePolicy::NEVER,
+                                        "StaticRewrite::tpg"));
+  }
+}
 
 PreprocessingPassResult StaticRewrite::applyInternal(
     AssertionPipeline* assertions)
@@ -125,6 +135,14 @@ TrustNode StaticRewrite::rewriteAssertion(TNode n)
         rewrittenTo[cur] = retr;
         rewrittenTo[ret] = retr;
         visit.push_back(retr);
+        if (d_tpg != nullptr)
+        {
+          d_tpg->addRewriteStep(ret,
+                                trn.getNode(),
+                                trn.getGenerator(),
+                                false,
+                                TrustId::PP_STATIC_REWRITE);
+        }
       }
       if (!wasRewritten)
       {
@@ -144,8 +162,8 @@ TrustNode StaticRewrite::rewriteAssertion(TNode n)
   {
     return TrustNode::null();
   }
-  // can make proof producing by providing a term conversion generator here
-  return TrustNode::mkTrustRewrite(n, ret, nullptr);
+  // use the term conversion proof generator if it exists
+  return TrustNode::mkTrustRewrite(n, ret, d_tpg.get());
 }
 
 }  // namespace passes

src/preprocessing/passes/static_rewrite.h

@@ -20,6 +20,7 @@
 
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
+#include "proof/conv_proof_generator.h"
 #include "proof/trust_node.h"
 
 namespace cvc5::internal {
@@ -48,6 +49,10 @@ class StaticRewrite : public PreprocessingPass
    * Returns the trust node corresponding to the rewrite.
    */
   TrustNode rewriteAssertion(TNode assertion);
+
+ private:
+  /** A term conversion proof generator */
+  std::unique_ptr<TConvProofGenerator> d_tpg;
 };
 
 }  // namespace passes

src/printer/smt2/smt2_printer.cpp

@@ -514,6 +514,7 @@ bool Smt2Printer::toStreamBase(std::ostream& out,
     case Kind::RELATION_GROUP_OP:
     case Kind::RELATION_AGGREGATE_OP:
     case Kind::RELATION_PROJECT_OP:
+    case Kind::RELATION_TABLE_JOIN_OP:
     {
       ProjectOp op = n.getConst<ProjectOp>();
       const std::vector<uint32_t>& indices = op.getIndices();
@@ -1281,6 +1282,7 @@ std::string Smt2Printer::smtKindString(Kind k)
     case Kind::SET_FILTER: return "set.filter";
     case Kind::SET_FOLD: return "set.fold";
     case Kind::RELATION_JOIN: return "rel.join";
+    case Kind::RELATION_TABLE_JOIN: return "rel.table_join";
     case Kind::RELATION_PRODUCT: return "rel.product";
     case Kind::RELATION_TRANSPOSE: return "rel.transpose";
     case Kind::RELATION_TCLOSURE: return "rel.tclosure";

src/proof/alf/alf_list_node_converter.cpp

@@ -0,0 +1,77 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of ALF node conversion for list variables in DSL rules
+ */
+
+#include "proof/alf/alf_list_node_converter.h"
+
+#include "expr/nary_term_util.h"
+#include "printer/printer.h"
+#include "printer/smt2/smt2_printer.h"
+
+namespace cvc5::internal {
+namespace proof {
+
+AlfListNodeConverter::AlfListNodeConverter(NodeManager* nm,
+                                           BaseAlfNodeConverter& tproc)
+    : NodeConverter(nm), d_tproc(tproc)
+{
+}
+
+Node AlfListNodeConverter::postConvert(Node n)
+{
+  Kind k = n.getKind();
+  switch (k)
+  {
+    case Kind::STRING_CONCAT:
+    case Kind::BITVECTOR_ADD:
+    case Kind::BITVECTOR_MULT:
+    case Kind::BITVECTOR_AND:
+    case Kind::BITVECTOR_OR:
+    case Kind::BITVECTOR_XOR:
+    case Kind::FINITE_FIELD_ADD:
+    case Kind::FINITE_FIELD_MULT:
+    case Kind::OR:
+    case Kind::AND:
+    case Kind::SEP_STAR:
+    case Kind::ADD:
+    case Kind::MULT:
+    case Kind::NONLINEAR_MULT:
+    case Kind::BITVECTOR_CONCAT:
+    case Kind::REGEXP_CONCAT:
+    case Kind::REGEXP_UNION:
+    case Kind::REGEXP_INTER:
+      // operators with a ground null terminator
+      break;
+    default:
+      // not an n-ary kind
+      return n;
+  }
+  size_t nlistChildren = 0;
+  for (const Node& nc : n)
+  {
+    if (!expr::isListVar(nc))
+    {
+      nlistChildren++;
+    }
+  }
+  // if less than 2 non-list children, it might collapse to a single element
+  if (nlistChildren < 2)
+  {
+    return d_tproc.mkInternalApp("$dsl.singleton_elim", {n}, n.getType());
+  }
+  return n;
+}
+
+}  // namespace proof
+}  // namespace cvc5::internal