Merge branch 'disableRewrite' into cav2019strings

4 files changed, 307 insertions, 17 deletions

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index d777a143a..d0f647452 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -229,21 +229,158 @@
                                  (collect_pseudo_resolvents cs c)))))))
 
 ; Is this proof a valid DRAT proof of bottom?
-(program is_drat_proof_of_bottom ((f cnf) (proof DRATProof)) bool
+(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
          (match proof
                 (DRATProofn (cnf_has_bottom f))
                 ((DRATProofa c p) (match
                                     (is_rat f c)
-                                    (tt (is_drat_proof_of_bottom (cnfc c f) p))
+                                    (tt (is_specified_drat_proof (cnfc c f) p))
                                     (ff ff)))
                 ((DRATProofd c p)
-                 (is_drat_proof_of_bottom (cnf_remove_clause c f) p))))
+                 (is_specified_drat_proof (cnf_remove_clause c f) p))))
 
 
+; =============================== ;
+; Operational DRAT implementation ;
+; =============================== ;
+
+; Operation DRAT is defined in the paper "Two Flavors of DRAT".
+; Below is an extension of the DRAT signature to handle it.
+
+; Notes on types.
+; For operational DRAT it is useful to manifest partial assignments in values
+; (although we still use the global assignment in some places). To this end,
+; literals are used to represent single-variable assignments ((pos v) denotes
+; {v maps to true}) and clauses are partial assignments by way of being
+; literal lists.
+
+; Copy the partial assignment represented by a clause into the global
+; assignment. Fails if that clause represents an inconsistent partial
+; assignment (e.g. v is both true and false)
+(program clause_into_global ((a clause)) Unit
+         (match a
+                (cln unit)
+                ((clc l rest)
+                 (do (lit_mk_sat l) (clause_into_global rest)))))
+
+; Remove the partial assignment represented by c from the global assignment
+(program clause_undo_into_global ((a clause)) Unit
+         (match a
+                (cln unit)
+                ((clc l rest)
+                 (do (lit_un_mk_sat l) (clause_undo_into_global rest)))))
+
+; Does this clause have no floating literals w.r.t. the global assignment?
+(program clause_no_floating ((c clause)) bool
+         (match c
+                (cln tt)
+                ((clc l rest) (match (lit_is_floating l)
+                                    (tt ff)
+                                    (ff (clause_no_floating rest))))))
+
+; Does this clause have no sat literals w.r.t. the global assignment?
+(program clause_no_sat ((c clause)) bool
+         (match c
+                (cln tt)
+                ((clc l rest) (match (lit_is_sat l)
+                                    (tt ff)
+                                    (ff (clause_no_sat rest))))))
+
+; Does this clause have one sat literal w.r.t. the global assignment?
+(program clause_one_sat ((c clause)) bool
+         (match c
+                (cln ff)
+                ((clc l rest) (match (lit_is_sat l)
+                                    (tt (clause_no_sat rest))
+                                    (ff (clause_one_sat rest))))))
+
+; Is this clause a unit clause w.r.t. the global assignment?
+; This notion is defined as:
+;    * A clause where no literals are floating, and exactly one is sat.
+(program clause_is_unit_wrt_up_model ((c clause) (up_model clause)) bool
+         (let c' (clause_dedup c)
+         (do (clause_into_global up_model)
+           (let result (match (clause_no_floating c')
+                              (tt (clause_one_sat c'))
+                              (ff ff))
+             (do (clause_undo_into_global up_model)
+               result)))))
+
+; Result from constructing a UP model (defined in "Two Flavors of DRAT")
+; Technically, we're constructing the shared UP model -- the intersection of all
+; UP models.
+; Informally, this is just the partial assignment implied by UP.
+;
+; This type is necessary, because constructing a UP model can reveal an
+; inconsistent UP model -- one which assigns some variable to true and false.
+; This would break our machinery, so we special case it.
+(declare UPConstructionResult type)
+; An actual model
+(declare UPCRModel (! up_model clause UPConstructionResult))
+; Bottom is implied!
+(declare UPCRBottom UPConstructionResult)
+
+
+; Do unit propagation on `f`, constructing a UP model for it.
+(program build_up_model ((f cnf)) clause
+         (match (unit_search f)
+                (USRBottom UPCRBottom)
+                (USRNoUnit (UPCRModel cln))
+                ((USRUnit l f')
+                 (let result (build_up_model f')
+                   (do (lit_un_mk_sat l)
+                     (match result
+                            (UPCRBottom UPCRBottom)
+                            ((UPCRModel model) (UPCRModel (clc l model)))))))))
+
+; Given some starting assignment (`up_model`), continue UP to construct a larger
+; model.
+(program extend_up_model ((f cnf) (up_model clause)) clause
+         (do (clause_into_global up_model)
+           (let result (build_up_model f)
+             (do (clause_undo_into_global up_model)
+               (match result
+                      (UPCRBottom UPCRBottom)
+                      ((UPCRModel up_model')
+                       (UPCRModel (clause_append up_model up_model'))))))))
+
+; Helper for `is_operational_drat_proof` which takes a UP model for the working
+; formula. The UP model is important for determining which clause deletions
+; actually are executed in operational DRAT. Passing the UP model along
+; prevents it from being fully recomputed everytime.
+(program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool
+         (match pf
+                (DRATProofn (cnf_has_bottom f))
+                ((DRATProofd c pf')
+                 (match (clause_is_unit_wrt_up_model c up_model)
+                        (tt (is_operational_drat_proof_h f up_model pf'))
+                        (ff (is_operational_drat_proof_h
+                              (cnf_remove_clause c f) up_model pf'))))
+                ((DRATProofa c pf')
+                 (let f' (cnfc c f)
+                   (match (is_rat f c)
+                          (tt (match (extend_up_model f' up_model)
+                                     (UPCRBottom tt)
+                                     ((UPCRModel up_model')
+                                      (is_operational_drat_proof_h f' up_model' pf'))))
+                          (ff ff))))))
+
+; Is this an operational DRAT proof of bottom for this formula?
+(program is_operational_drat_proof ((f cnf) (pf DRATProof)) bool
+         (match (build_up_model f)
+                (UPCRBottom tt)
+                ((UPCRModel model) (is_operational_drat_proof_h f model pf))))
+
+; Is this a specified or operational DRAT proof of bottom for this formula?
+(program is_drat_proof ((f cnf) (pf DRATProof)) bool
+         (match (is_specified_drat_proof f pf)
+                (tt tt)
+                (ff (is_operational_drat_proof f pf))))
+
 (declare drat_proof_of_bottom
          (! f cnf
             (! proof_of_formula (cnf_holds f)
                (! proof DRATProof
-                  (! sc (^ (is_drat_proof_of_bottom f proof) tt)
+                  (! sc (^ (is_drat_proof f proof) tt)
                      bottom)))))
 
diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf
index 57de39111..2ede6df34 100644
--- a/proofs/signatures/drat_test.plf
+++ b/proofs/signatures/drat_test.plf
@@ -280,3 +280,155 @@
                (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
                (DRATProofa cln
                 DRATProofn)))))))))))))))
+
+; ===================================== ;
+; Test Suite from "Two Flavors of DRAT" ;
+; ===================================== ;
+
+; The paper includes a number of proofs which explore specified and operational
+; DRAT validity.
+
+; Our test predicate for asserting the specified and operational validity of
+; DRAT proofs
+(declare spec_oper_test
+         (! f cnf
+         (! proof DRATProof
+         (! spec_validity bool
+         (! oper_validity bool
+            (! sc (^ (bool_and
+                       (bool_eq (is_specified_drat_proof f proof) spec_validity)
+                       (bool_eq (is_operational_drat_proof f proof) oper_validity)
+                     ) tt)
+         TestSuccess))))))
+
+
+(declare x var)
+(declare y var)
+(declare z var)
+(declare w var)
+(define ex_1_formula
+  (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln)))
+        cnfn)))))))))
+
+; Spec-valid, operationally-invalid
+(define ex_1_pf_pi
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofd (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn)))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_pi tt ff)))
+
+; Spec-invalid, operationally valid
+(define ex_1_pf_sigma
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofd (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt)))
+
+(declare x1 var)
+(declare x2 var)
+(declare x3 var)
+(declare x4 var)
+(declare x5 var)
+(declare x6 var)
+(declare x7 var)
+(declare x8 var)
+(declare x9 var)
+(declare x10 var)
+
+(define ex_2_formula
+  (cnfc (clc (pos x1) cln)
+  (cnfc (clc (neg x1) (clc (pos x2) cln))
+  (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln)))
+  (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln)))
+  (cnfc (clc (pos x5) (clc (pos x6) cln))
+  (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln)))
+  (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln)))
+  (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln)))
+  (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln)))
+  (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln)))
+  (cnfc (clc (neg x8) (clc (pos x5) cln))
+  (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x10) (clc (pos x9) cln))
+  (cnfc (clc (neg x9) (clc (pos x7) cln))
+  (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln))))
+        cnfn)))))))))))))))))
+
+; Spec-valid, operationally-valid
+(define ex_2_pf_tau
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofa (clc (pos x4) cln)
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_2_pf_tau tt tt)))
+
+; Spec-valid, operationally unspecified in the paper, but its operationally valid.
+(define ex_3_pf_tau_prime
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofd (clc (neg x1) (clc (pos x2) cln))
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt)))
+
+; Spec-invalid, operationally-invalid
+(define ex_4_pf_pi_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff)))
+
+
+; Spec-valid, operationally valid
+(define ex_5_pf_sigma_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn)))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt)))
+
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c4a6905c4..902b5a670 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2424,19 +2424,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       {
         return returnRewrite(node, node[0], "rpl-const-nfind");
       }
-      // if no overlap, we can pull the first child
-      if (s.overlap(t) == 0)
-      {
-        std::vector<Node> spl(children0.begin() + 1, children0.end());
-        Node ret = NodeManager::currentNM()->mkNode(
-            kind::STRING_CONCAT,
-            children0[0],
-            NodeManager::currentNM()->mkNode(kind::STRING_STRREPL,
-                                             mkConcat(kind::STRING_CONCAT, spl),
-                                             node[1],
-                                             node[2]));
-        return returnRewrite(node, ret, "rpl-prefix-nfind");
-      }
     }
     else
     {
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 457e78cfc..e489f1106 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -536,6 +536,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node ab = d_nm->mkConst(::CVC4::String("AB"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
     Node d = d_nm->mkConst(::CVC4::String("D"));
@@ -666,6 +667,19 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              b);
     repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
     differentNormalForms(repl_repl, repl);
+
+    {
+      // Same normal form:
+      //
+      // (str.replace (str.++ "AB" x) "C" y)
+      //
+      // (str.++ "AB" (str.replace x "C" y))
+      Node lhs = d_nm->mkNode(
+          kind::STRING_STRREPL, d_nm->mkNode(kind::STRING_CONCAT, ab, x), c, y);
+      Node rhs = d_nm->mkNode(
+          kind::STRING_CONCAT, ab, d_nm->mkNode(kind::STRING_STRREPL, x, c, y));
+      sameNormalForm(lhs, rhs);
+    }
   }
 
   void testRewriteContains()