Fix models for sygus-inference, bv2int, real2int (#6421)

In each case, previously we were generating a define-fun, what we needed was to do a model substitution.

This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 6fe676e30fa04aee44d0f3642c2065dceb59d8c8..c725081c2a8f77580fe29dd40e38b4aeda6462ee 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -840,8 +840,15 @@ void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
   }
   // If the result is BV, it needs to be casted back.
   result = castToType(result, resultType);
-  // add the function definition to the smt engine.
-  d_preprocContext->getSmt()->defineFunction(bvUF, args, result, true);
+  // add the substitution to the preprocessing context, which ensures the
+  // model for bvUF is correct, as well as substituting it in the input
+  // assertions when necessary.
+  if (!args.empty())
+  {
+    result = d_nm->mkNode(
+        kind::LAMBDA, d_nm->mkNode(kind::BOUND_VAR_LIST, args), result);
+  }
+  d_preprocContext->addSubstitution(bvUF, result);
 }
 
 bool BVToInt::childrenTypesChanged(Node n)

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 7c40975644785c723498c500d341e075fe501415..9e84dc851ac22db09b8303b846028457f1cf449f 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -26,12 +26,17 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
+using namespace cvc5::theory;
+
 namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace std;
-using namespace cvc5::theory;
+RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "real-to-int"),
+      d_cache(preprocContext->getUserContext())
+{
+}
 
 Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
 {
@@ -181,15 +186,13 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
         }
         else if (n.isVar())
         {
-          ret = sm->mkDummySkolem(
-              "__realToIntInternal_var",
-              nm->integerType(),
-              "Variable introduced in realToIntInternal pass");
+          Node toIntN = nm->mkNode(kind::TO_INTEGER, n);
+          ret = sm->mkPurifySkolem(toIntN, "__realToIntInternal_var");
           var_eq.push_back(n.eqNode(ret));
-          // ensure that the original variable is defined to be the returned
-          // one, which is important for models and for incremental solving.
-          std::vector<Node> args;
-          d_preprocContext->getSmt()->defineFunction(n, args, ret);
+          // add the substitution to the preprocessing context, which ensures
+          // the model for n is correct, as well as substituting it in the input
+          // assertions when necessary.
+          d_preprocContext->addSubstitution(n, ret);
         }
       }
     }
@@ -198,18 +201,14 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
   }
 }
 
-RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "real-to-int"){};
-
 PreprocessingPassResult RealToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  unordered_map<Node, Node, NodeHashFunction> cache;
   std::vector<Node> var_eq;
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     assertionsToPreprocess->replace(
-        i, realToIntInternal((*assertionsToPreprocess)[i], cache, var_eq));
+        i, realToIntInternal((*assertionsToPreprocess)[i], d_cache, var_eq));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }

diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
index 9f0eb529f1223145dc07370a96d8f52012896776..d26547372ab3402943c95638ed4bd70cbc513ca1 100644 (file)
--- a/src/preprocessing/passes/real_to_int.h
+++ b/src/preprocessing/passes/real_to_int.h
@@ -22,6 +22,7 @@
 
 #include <vector>
 
+#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
@@ -29,10 +30,10 @@ namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
-
 class RealToInt : public PreprocessingPass
 {
+  using NodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
  public:
   RealToInt(PreprocessingPassContext* preprocContext);
 
@@ -42,6 +43,8 @@ class RealToInt : public PreprocessingPass
 
  private:
   Node realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq);
+  /** Cache for the above method */
+  NodeMap d_cache;
 };
 
 }  // namespace passes

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 870ad6625b121827efe09ee21f4c1442a314302a..b15d5a377f125edd66ea6d2eb7aa3568aee3a69a 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -47,23 +47,13 @@ PreprocessingPassResult SygusInference::applyInternal(
   // see if we can succesfully solve the input as a sygus problem
   if (solveSygus(assertionsToPreprocess->ref(), funs, sols))
   {
+    Trace("sygus-infer") << "...Solved:" << std::endl;
     Assert(funs.size() == sols.size());
-    // if so, sygus gives us function definitions
-    SmtEngine* master_smte = d_preprocContext->getSmt();
+    // if so, sygus gives us function definitions, which we add as substitutions
     for (unsigned i = 0, size = funs.size(); i < size; i++)
     {
-      std::vector<Node> args;
-      Node sol = sols[i];
-      // if it is a non-constant function
-      if (sol.getKind() == LAMBDA)
-      {
-        for (const Node& v : sol[0])
-        {
-          args.push_back(v);
-        }
-        sol = sol[1];
-      }
-      master_smte->defineFunction(funs[i], args, sol);
+      Trace("sygus-infer") << funs[i] << " -> " << sols[i] << std::endl;
+      d_preprocContext->addSubstitution(funs[i], sols[i]);
     }
 
     // apply substitution to everything, should result in SAT

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 22cc15a973c6c67d876f4e84bbc8cbf491bec43f..4be6b4aac07743d613093db8b0d25efb4e447059 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -63,6 +63,15 @@ void PreprocessingPassContext::addModelSubstitution(const Node& lhs,
       lhs, d_smt->expandDefinitions(rhs, false));
 }
 
+void PreprocessingPassContext::addSubstitution(const Node& lhs,
+                                               const Node& rhs,
+                                               ProofGenerator* pg)
+{
+  d_topLevelSubstitutions.addSubstitution(lhs, rhs, pg);
+  // also add as a model substitution
+  addModelSubstitution(lhs, rhs);
+}
+
 ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
 {
   return d_pnm;

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index f1d92e864f01abeff73d0167aec93ae1f8de3dd0..a7e9b0debfc28a69e02f2da384a0172290868a7a 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -81,11 +81,22 @@ class PreprocessingPassContext
   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
 
   /**
-   * Add substitution to theory model.
+   * Add substitution to theory model. This method should only be called if
+   * we have already added the substitution to the top-level substitutions
+   * class. Otherwise, addSubstitution should be called instead.
    * @param lhs The node replaced by node 'rhs'
    * @param rhs The node to substitute node 'lhs'
    */
   void addModelSubstitution(const Node& lhs, const Node& rhs);
+  /**
+   * Add substitution to the top-level substitutions and to the theory model.
+   * @param lhs The node replaced by node 'rhs'
+   * @param rhs The node to substitute node 'lhs'
+   * @param pg The proof generator that can provide a proof of lhs == rhs.
+   */
+  void addSubstitution(const Node& lhs,
+                       const Node& rhs,
+                       ProofGenerator* pg = nullptr);
 
   /** The the proof node manager associated with this context, if it exists */
   ProofNodeManager* getProofNodeManager();

diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
index 81af8c4e7765713c60938df382cca7da36f7d4e5..155033d7db17fb7f82531437cf67cfb42662daf4 100644 (file)
--- a/test/regress/regress0/push-pop/real-as-int-incremental.smt2
+++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --solve-real-as-int
+; COMMAND-LINE: --incremental --solve-real-as-int -q
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
index 082df249bc2874be8740c86390510a31ed86a38b..3a4f24521a3ba3cd1f27b4c989cdbf2c2cbfb61b 100644 (file)
--- a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
+++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
index b851d2e19fcb233c5d8c1524a87cd17fb53da1fa..d333358ed5986b30561bc15718c67c93b6bb696d 100644 (file)
--- a/test/regress/regress1/quantifiers/horn-simple.smt2
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer -q
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)

diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
index 471cc519bd68b5ebe6f4b5f0c7a520aa2095ae2f..6d0b37a305afe5a0c9086542cf24022af520f93d 100644 (file)
--- a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
+++ b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-option :conjecture-filter-model true)
 (set-option :conjecture-gen true)