Fix cache for sygus post-condition inference (#2592)

5 files changed, 82 insertions, 7 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 36690cfcc..b698422a7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -804,7 +804,7 @@ void TransitionInference::process( Node n ) {
   }
   for( unsigned i=0; i<n_check.size(); i++ ){
     Node nn = n_check[i];
-    std::map< Node, bool > visited;
+    std::map<bool, std::map<Node, bool> > visited;
     std::map< bool, Node > terms;
     std::vector< Node > disjuncts;
     Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl;
@@ -949,10 +949,16 @@ void TransitionInference::getNormalizedSubstitution(
   }
 }
 
-bool TransitionInference::processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, 
-                                           std::map< Node, bool >& visited, bool topLevel ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
+bool TransitionInference::processDisjunct(
+    Node n,
+    std::map<bool, Node>& terms,
+    std::vector<Node>& disjuncts,
+    std::map<bool, std::map<Node, bool> >& visited,
+    bool topLevel)
+{
+  if (visited[topLevel].find(n) == visited[topLevel].end())
+  {
+    visited[topLevel][n] = true;
     bool childTopLevel = n.getKind()==OR && topLevel;
     //if another part mentions UF or a free variable, then fail
     bool lit_pol = n.getKind()!=NOT;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index c797bc3cb..cfd7cd23b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -58,9 +58,47 @@ public:
   void print( const char* c );
 };
 
+/**
+ * This class is used for inferring that an arbitrary synthesis conjecture
+ * corresponds to an invariant synthesis problem for some predicate (d_func).
+ *
+ * The invariant-to-synthesize can either be explicitly given, via a call
+ * to initialize( f, vars ), or otherwise inferred if this method is not called.
+ */
 class TransitionInference {
-private:
-  bool processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, std::map< Node, bool >& visited, bool topLevel );
+ private:
+  /** process disjunct
+   *
+   * The purpose of this function is to infer pre/post/transition conditions
+   * for a (possibly unknown) invariant-to-synthesis, given a conjunct from
+   * an arbitrary synthesis conjecture.
+   *
+   * Assume our negated synthesis conjecture is of the form:
+   *    forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n}))
+   * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true
+   * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i}
+   * to disjuncts.
+   *
+   * If this method returns true, then (1) all applications of free function
+   * symbols have operator d_func. Note this function may set d_func to a
+   * function symbol in n if d_func was null prior to this call. In other words,
+   * this method may infer the subject of the invariant synthesis problem;
+   * (2) all occurrences of d_func are "top-level", that is, each Fij may be
+   * of the form (not) <d_func>( tj ), but otherwise d_func does not occur in
+   * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of
+   * <d_func>( tj ), and (not <d_func>( tk )).
+   *
+   * If the above conditions are met, then terms[true] is set to <d_func>( tj )
+   * if Fij is <d_func>( tj ) for some j, and likewise terms[false]
+   * is set to <d_func>( tk ) if Fik is (not <d_func>( tk )) for some k.
+   *
+   * The argument visited caches the results of this function for (topLevel, n).
+   */
+  bool processDisjunct(Node n,
+                       std::map<bool, Node>& terms,
+                       std::vector<Node>& disjuncts,
+                       std::map<bool, std::map<Node, bool> >& visited,
+                       bool topLevel);
   void getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol );
   bool d_complete;
   /** get normalized substitution
@@ -89,6 +127,10 @@ private:
   TransitionInference() : d_complete( false ) {}
   std::vector< Node > d_vars;
   std::vector< Node > d_prime_vars;
+  /**
+   * The function (predicate) that is the subject of the invariant synthesis
+   * problem we are inferring.
+   */
   Node d_func;
   
   class Component {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 441327b3a..19513ada3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1585,6 +1585,7 @@ set(regress_1_tests
   regress1/sygus/icfp_28_10.sy
   regress1/sygus/icfp_easy-ite.sy
   regress1/sygus/inv-example.sy
+  regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 4e9837c36..5bd187e8f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1582,6 +1582,7 @@ REG1_TESTS = \
 	regress1/sygus/icfp_28_10.sy \
 	regress1/sygus/icfp_easy-ite.sy \
 	regress1/sygus/inv-example.sy \
+	regress1/sygus/inv-missed-sol-true.sy \
 	regress1/sygus/inv-unused.sy \
 	regress1/sygus/large-const-simp.sy \
 	regress1/sygus/let-bug-simp.sy \
diff --git a/test/regress/regress1/sygus/inv-missed-sol-true.sy b/test/regress/regress1/sygus/inv-missed-sol-true.sy
new file mode 100644
index 000000000..b04022766
--- /dev/null
+++ b/test/regress/regress1/sygus/inv-missed-sol-true.sy
@@ -0,0 +1,25 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-inv inv-f ((x Int) (z Int)))
+
+(declare-primed-var x Int)
+(declare-primed-var z Int)
+
+(define-fun pre-f ((x Int) (z Int)) Bool
+  (and (> x (- 0 100)) (< x 200)
+       (> z 100) (< z 200)))
+
+(define-fun trans-f ((x Int) (z Int) (x! Int) (z! Int)) Bool
+  (and (< x 100) (> z 100)
+       (or (and (= x! (+ x 1)) (= z! z))
+           (and (= x! (- x 1)) (= z! (- z 1))))))
+
+(define-fun post-f ((x Int) (z Int)) Bool
+  (or (and (< x 100) (> z 100))
+      (or (>= x 100) (<= z 100))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)
\ No newline at end of file