Merge branch 'master' into nprocnproc

9 files changed, 177 insertions, 112 deletions

diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake
index 80fa2e4ec..0c095a529 100644
--- a/cmake/FindCaDiCaL.cmake
+++ b/cmake/FindCaDiCaL.cmake
@@ -47,8 +47,6 @@ if(NOT CaDiCaL_FOUND_SYSTEM)
   include(CheckSymbolExists)
   include(ExternalProject)
 
-  fail_if_include_missing("sys/resource.h" "CaDiCaL")
-
   set(CaDiCaL_VERSION "88623ef0866370448c34f6e320c148fc18e6f4cc")
 
   # avoid configure script and instantiate the makefile manually the configure
@@ -110,6 +108,16 @@ set_target_properties(
   CaDiCaL PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${CaDiCaL_INCLUDE_DIR}"
 )
 
+if (WIN32)
+  # The Windows version of CaDiCaL calls GetProcessMemoryInfo(), which is
+  # defined in the Process Status API (psapi), so we declare it as a dependency
+  # of the CaDiCaL library (without this, linking a static cvc5 executable
+  # fails).
+  set_target_properties(
+    CaDiCaL PROPERTIES IMPORTED_LINK_INTERFACE_LIBRARIES psapi
+  )
+endif ()
+
 mark_as_advanced(CaDiCaL_FOUND)
 mark_as_advanced(CaDiCaL_FOUND_SYSTEM)
 mark_as_advanced(CaDiCaL_INCLUDE_DIR)
diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake
index 734962423..e11d85c3f 100644
--- a/cmake/FindPoly.cmake
+++ b/cmake/FindPoly.cmake
@@ -51,10 +51,6 @@ if(NOT Poly_FOUND_SYSTEM)
   if(CCWIN)
     # Roughly following https://stackoverflow.com/a/44383330/2375725
     set(patchcmd
-        COMMAND
-        patch
-        <SOURCE_DIR>/src/CMakeLists.txt
-        ${CMAKE_CURRENT_LIST_DIR}/deps-utils/Poly-patch-cmake.patch
         # Avoid %z and %llu format specifiers
         COMMAND find <SOURCE_DIR>/ -type f -exec
                 sed -i.orig "s/%z[diu]/%\" PRIu64 \"/g" {} +
diff --git a/cmake/deps-utils/Poly-patch-cmake.patch b/cmake/deps-utils/Poly-patch-cmake.patch
deleted file mode 100644
index fe8528f70..000000000
--- a/cmake/deps-utils/Poly-patch-cmake.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
-index f91e3e8..6205689 100755
---- a/src/CMakeLists.txt
-+++ b/src/CMakeLists.txt
-@@ -38,7 +38,7 @@ set(poly_SOURCES
- )
- 
- if (NOT HAVE_OPEN_MEMSTREAM) 
--  set(poly_SOURCES "utils/open_memstream.c ${poly_SOURCES}")
-+  set(poly_SOURCES utils/open_memstream.c ${poly_SOURCES})
- endif()
- 
- set(polyxx_SOURCES
diff --git a/docs/conf.py.in b/docs/conf.py.in
index 65e880bc9..35f0b3dd2 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -67,6 +67,7 @@ html_theme = 'sphinx_rtd_theme'
 html_theme_options = {}
 html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/']
 html_css_files = ['custom.css']
+html_show_sourcelink = False
 
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f8a34ec42..40853b33a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -292,7 +292,7 @@ SatLiteral CnfStream::getLiteral(TNode node) {
   return literal;
 }
 
-SatLiteral CnfStream::handleXor(TNode xorNode)
+void CnfStream::handleXor(TNode xorNode)
 {
   Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
   Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!";
@@ -300,8 +300,8 @@ SatLiteral CnfStream::handleXor(TNode xorNode)
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
   Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
 
-  SatLiteral a = toCNF(xorNode[0]);
-  SatLiteral b = toCNF(xorNode[1]);
+  SatLiteral a = getLiteral(xorNode[0]);
+  SatLiteral b = getLiteral(xorNode[1]);
 
   SatLiteral xorLit = newLiteral(xorNode);
 
@@ -309,11 +309,9 @@ SatLiteral CnfStream::handleXor(TNode xorNode)
   assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
   assertClause(xorNode, a, ~b, xorLit);
   assertClause(xorNode, ~a, b, xorLit);
-
-  return xorLit;
 }
 
-SatLiteral CnfStream::handleOr(TNode orNode)
+void CnfStream::handleOr(TNode orNode)
 {
   Assert(!hasLiteral(orNode)) << "Atom already mapped!";
   Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!";
@@ -322,37 +320,31 @@ SatLiteral CnfStream::handleOr(TNode orNode)
   Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
 
   // Number of children
-  unsigned n_children = orNode.getNumChildren();
-
-  // Transform all the children first
-  TNode::const_iterator node_it = orNode.begin();
-  TNode::const_iterator node_it_end = orNode.end();
-  SatClause clause(n_children + 1);
-  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
-    clause[i] = toCNF(*node_it);
-  }
+  size_t numChildren = orNode.getNumChildren();
 
   // Get the literal for this node
   SatLiteral orLit = newLiteral(orNode);
 
-  // lit <- (a_1 | a_2 | a_3 | ... | a_n)
-  // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
-  // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
-  for(unsigned i = 0; i < n_children; ++i) {
+  // Transform all the children first
+  SatClause clause(numChildren + 1);
+  for (size_t i = 0; i < numChildren; ++i)
+  {
+    clause[i] = getLiteral(orNode[i]);
+
+    // lit <- (a_1 | a_2 | a_3 | ... | a_n)
+    // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
+    // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
     assertClause(orNode, orLit, ~clause[i]);
   }
 
   // lit -> (a_1 | a_2 | a_3 | ... | a_n)
   // ~lit | a_1 | a_2 | a_3 | ... | a_n
-  clause[n_children] = ~orLit;
+  clause[numChildren] = ~orLit;
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(orNode.negate(), clause);
-
-  // Return the literal
-  return orLit;
 }
 
-SatLiteral CnfStream::handleAnd(TNode andNode)
+void CnfStream::handleAnd(TNode andNode)
 {
   Assert(!hasLiteral(andNode)) << "Atom already mapped!";
   Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!";
@@ -361,37 +353,32 @@ SatLiteral CnfStream::handleAnd(TNode andNode)
   Trace("cnf") << "handleAnd(" << andNode << ")\n";
 
   // Number of children
-  unsigned n_children = andNode.getNumChildren();
-
-  // Transform all the children first (remembering the negation)
-  TNode::const_iterator node_it = andNode.begin();
-  TNode::const_iterator node_it_end = andNode.end();
-  SatClause clause(n_children + 1);
-  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
-    clause[i] = ~toCNF(*node_it);
-  }
+  size_t numChildren = andNode.getNumChildren();
 
   // Get the literal for this node
   SatLiteral andLit = newLiteral(andNode);
 
-  // lit -> (a_1 & a_2 & a_3 & ... & a_n)
-  // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
-  // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
-  for(unsigned i = 0; i < n_children; ++i) {
+  // Transform all the children first (remembering the negation)
+  SatClause clause(numChildren + 1);
+  for (size_t i = 0; i < numChildren; ++i)
+  {
+    clause[i] = ~getLiteral(andNode[i]);
+
+    // lit -> (a_1 & a_2 & a_3 & ... & a_n)
+    // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
+    // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
     assertClause(andNode.negate(), ~andLit, ~clause[i]);
   }
 
   // lit <- (a_1 & a_2 & a_3 & ... a_n)
   // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
   // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
-  clause[n_children] = andLit;
+  clause[numChildren] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(andNode, clause);
-
-  return andLit;
 }
 
-SatLiteral CnfStream::handleImplies(TNode impliesNode)
+void CnfStream::handleImplies(TNode impliesNode)
 {
   Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
   Assert(impliesNode.getKind() == kind::IMPLIES)
@@ -401,8 +388,8 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode)
   Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
 
   // Convert the children to cnf
-  SatLiteral a = toCNF(impliesNode[0]);
-  SatLiteral b = toCNF(impliesNode[1]);
+  SatLiteral a = getLiteral(impliesNode[0]);
+  SatLiteral b = getLiteral(impliesNode[1]);
 
   SatLiteral impliesLit = newLiteral(impliesNode);
 
@@ -415,11 +402,9 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode)
   // (a | l) & (~b | l)
   assertClause(impliesNode, a, impliesLit);
   assertClause(impliesNode, ~b, impliesLit);
-
-  return impliesLit;
 }
 
-SatLiteral CnfStream::handleIff(TNode iffNode)
+void CnfStream::handleIff(TNode iffNode)
 {
   Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
   Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
@@ -428,8 +413,8 @@ SatLiteral CnfStream::handleIff(TNode iffNode)
   Trace("cnf") << "handleIff(" << iffNode << ")\n";
 
   // Convert the children to CNF
-  SatLiteral a = toCNF(iffNode[0]);
-  SatLiteral b = toCNF(iffNode[1]);
+  SatLiteral a = getLiteral(iffNode[0]);
+  SatLiteral b = getLiteral(iffNode[1]);
 
   // Get the now literal
   SatLiteral iffLit = newLiteral(iffNode);
@@ -447,11 +432,9 @@ SatLiteral CnfStream::handleIff(TNode iffNode)
   // (~a | ~b | lit) & (a | b | lit)
   assertClause(iffNode, ~a, ~b, iffLit);
   assertClause(iffNode, a, b, iffLit);
-
-  return iffLit;
 }
 
-SatLiteral CnfStream::handleIte(TNode iteNode)
+void CnfStream::handleIte(TNode iteNode)
 {
   Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
   Assert(iteNode.getKind() == kind::ITE);
@@ -460,9 +443,9 @@ SatLiteral CnfStream::handleIte(TNode iteNode)
   Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
                << iteNode[2] << ")\n";
 
-  SatLiteral condLit = toCNF(iteNode[0]);
-  SatLiteral thenLit = toCNF(iteNode[1]);
-  SatLiteral elseLit = toCNF(iteNode[2]);
+  SatLiteral condLit = getLiteral(iteNode[0]);
+  SatLiteral thenLit = getLiteral(iteNode[1]);
+  SatLiteral elseLit = getLiteral(iteNode[2]);
 
   SatLiteral iteLit = newLiteral(iteNode);
 
@@ -485,47 +468,79 @@ SatLiteral CnfStream::handleIte(TNode iteNode)
   assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
   assertClause(iteNode, iteLit, ~condLit, ~thenLit);
   assertClause(iteNode, iteLit, condLit, ~elseLit);
-
-  return iteLit;
 }
 
 SatLiteral CnfStream::toCNF(TNode node, bool negated)
 {
   Trace("cnf") << "toCNF(" << node
                << ", negated = " << (negated ? "true" : "false") << ")\n";
+
+  TNode cur;
   SatLiteral nodeLit;
-  Node negatedNode = node.notNode();
-
-  // If the non-negated node has already been translated, get the translation
-  if(hasLiteral(node)) {
-    Trace("cnf") << "toCNF(): already translated\n";
-    nodeLit = getLiteral(node);
-    // Return the (maybe negated) literal
-    return !negated ? nodeLit : ~nodeLit;
-  }
-  // Handle each Boolean operator case
-  switch (node.getKind())
+  std::vector<TNode> visit;
+  std::unordered_map<TNode, bool> cache;
+
+  visit.push_back(node);
+  while (!visit.empty())
   {
-    case kind::NOT: nodeLit = ~toCNF(node[0]); break;
-    case kind::XOR: nodeLit = handleXor(node); break;
-    case kind::ITE: nodeLit = handleIte(node); break;
-    case kind::IMPLIES: nodeLit = handleImplies(node); break;
-    case kind::OR: nodeLit = handleOr(node); break;
-    case kind::AND: nodeLit = handleAnd(node); break;
-    case kind::EQUAL:
-      nodeLit =
-          node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node);
-      break;
-    default:
+    cur = visit.back();
+    Assert(cur.getType().isBoolean());
+
+    if (hasLiteral(cur))
     {
-      nodeLit = convertAtom(node);
+      visit.pop_back();
+      continue;
     }
-    break;
+
+    const auto& it = cache.find(cur);
+    if (it == cache.end())
+    {
+      cache.emplace(cur, false);
+      Kind k = cur.getKind();
+      // Only traverse Boolean nodes
+      if (k == kind::NOT || k == kind::XOR || k == kind::ITE
+          || k == kind::IMPLIES || k == kind::OR || k == kind::AND
+          || (k == kind::EQUAL && cur[0].getType().isBoolean()))
+      {
+        // Preserve the order of the recursive version
+        for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
+        {
+          visit.push_back(cur[size - 1 - i]);
+        }
+      }
+      continue;
+    }
+    else if (!it->second)
+    {
+      it->second = true;
+      Kind k = cur.getKind();
+      switch (k)
+      {
+        case kind::NOT: Assert(hasLiteral(cur[0])); break;
+        case kind::XOR: handleXor(cur); break;
+        case kind::ITE: handleIte(cur); break;
+        case kind::IMPLIES: handleImplies(cur); break;
+        case kind::OR: handleOr(cur); break;
+        case kind::AND: handleAnd(cur); break;
+        default:
+          if (k == kind::EQUAL && cur[0].getType().isBoolean())
+          {
+            handleIff(cur);
+          }
+          else
+          {
+            convertAtom(cur);
+          }
+          break;
+      }
+    }
+    visit.pop_back();
   }
-  // Return the (maybe negated) literal
+
+  nodeLit = getLiteral(node);
   Trace("cnf") << "toCNF(): resulting literal: "
                << (!negated ? nodeLit : ~nodeLit) << "\n";
-  return !negated ? nodeLit : ~nodeLit;
+  return negated ? ~nodeLit : nodeLit;
 }
 
 void CnfStream::convertAndAssertAnd(TNode node, bool negated)
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 264e26777..2959ae726 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -191,16 +191,16 @@ class CnfStream {
    */
   SatLiteral toCNF(TNode node, bool negated = false);
 
-  /** Specific clausifiers, based on the formula kinds, that clausify a formula,
-   * by calling toCNF into each of the formula's children under the respective
-   * kind, and introduce a literal definitionally equal to it. */
-  SatLiteral handleNot(TNode node);
-  SatLiteral handleXor(TNode node);
-  SatLiteral handleImplies(TNode node);
-  SatLiteral handleIff(TNode node);
-  SatLiteral handleIte(TNode node);
-  SatLiteral handleAnd(TNode node);
-  SatLiteral handleOr(TNode node);
+  /**
+   * Specific clausifiers that clausify a formula based on the given formula
+   * kind and introduce a literal definitionally equal to it.
+   */
+  void handleXor(TNode node);
+  void handleImplies(TNode node);
+  void handleIff(TNode node);
+  void handleIte(TNode node);
+  void handleAnd(TNode node);
+  void handleOr(TNode node);
 
   /** Stores the literal of the given node in d_literalToNodeMap.
    *
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 9972581c0..af131c2c3 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -133,7 +133,6 @@ class ProofCnfStream : public ProofGenerator
    * Specific clausifiers, based on the formula kinds, that clausify a formula,
    * by calling toCNF into each of the formula's children under the respective
    * kind, and introduce a literal definitionally equal to it. */
-  SatLiteral handleNot(TNode node);
   SatLiteral handleXor(TNode node);
   SatLiteral handleImplies(TNode node);
   SatLiteral handleIff(TNode node);
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index e9fd47261..4811cca1b 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance)
 cvc5_add_api_test(two_solvers)
 cvc5_add_api_test(issue5074)
 cvc5_add_api_test(issue4889)
+cvc5_add_api_test(issue6111)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp
new file mode 100644
index 000000000..bd7be2ad0
--- /dev/null
+++ b/test/api/issue6111.cpp
@@ -0,0 +1,58 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Test for issue #6111
+ *
+ */
+#include <iostream>
+#include <vector>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main()
+{
+  Solver solver;
+  solver.setLogic("QF_BV");
+  Sort bvsort12979 = solver.mkBitVectorSort(12979);
+  Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1");
+  Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10);
+
+  vector<Term> args1;
+  args1.push_back(zero);
+  args1.push_back(input2_1);
+  Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1);
+  solver.assertFormula(bvult_res);
+
+  Sort bvsort4 = solver.mkBitVectorSort(4);
+  Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42");
+  Sort bvsort8 = solver.mkBitVectorSort(8);
+  Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43");
+
+  vector<Term> args2;
+  args2.push_back(concat_result_42);
+  args2.push_back(
+      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
+  solver.assertFormula(solver.mkTerm(EQUAL, args2));
+
+  vector<Term> args3;
+  args3.push_back(concat_result_42);
+  args3.push_back(
+      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
+  solver.assertFormula(solver.mkTerm(EQUAL, args3));
+
+  cout << solver.checkSat() << endl;
+
+  return 0;
+}