From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Aug 2019 21:04:43 +0000 (-0500)
Subject: Flip the polarity of the argument of get-abduct (#3153)
X-Git-Tag: cvc5-1.0.0~4048
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=902262c421e52405204b3a95310c8414cc51a5c5;p=cvc5.git

Flip the polarity of the argument of get-abduct (#3153)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index df46fc924..914e20b05 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5078,7 +5078,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
     axioms.push_back(Node::fromExpr(easserts[i]));
   }
   std::vector<Node> asserts(axioms.begin(), axioms.end());
-  asserts.push_back(Node::fromExpr(conj));
+  // negate the conjecture
+  Node conjn = Node::fromExpr(conj).negate();
+  asserts.push_back(conjn);
   d_sssfVarlist.clear();
   d_sssfSyms.clear();
   std::string name("A");
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9f56a1cd3..dc275218f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -949,7 +949,7 @@ class CVC4_PUBLIC SmtEngine {
    * This method asks this SMT engine to find an abduct with respect to the
    * current assertion stack (call it A) and the conjecture (call it B).
    * If this method returns true, then abd is set to a formula C such that
-   * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable.
+   * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
    *
    * The argument grammarType is a sygus datatype type that encodes the syntax
    * restrictions on the shape of possible solutions.
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
index 17971f184..bda237676 100644
--- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
+++ b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
@@ -19,7 +19,7 @@
 ; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
 ; first.
 (get-abduct A 
-  (not (<= n m))
+  (<= n m)
   ((GA Bool) (GI Int))
   (
   (GA Bool ((>= GI GI)))
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index bdb680613..4b7870c78 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -14,9 +14,9 @@
 
 ; Generate a predicate A that is consistent with the above axioms (i.e.
 ; their conjunction is SAT), and is such that the conjunction of the above
-; axioms, A and the conjecture below are UNSAT.
+; axioms, A and the negation of the conjecture below are UNSAT.
 ; The signature of A is below grammar.
-(get-abduct A (< x y)
+(get-abduct A (not (< x y))
 
 ; the grammar for the abduct-to-synthesize
 ((Start Bool) (StartInt Int))
diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2
index d01f5f5ff..ed1ea6ddf 100644
--- a/test/regress/regress1/sygus-abduct-test.smt2
+++ b/test/regress/regress1/sygus-abduct-test.smt2
@@ -13,4 +13,4 @@
 (assert (and (<= n x)(<= x (+ n 5))))
 (assert (and (<= 1 y)(<= y m)))
 
-(get-abduct A (< x y))
+(get-abduct A (not (< x y)))