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 df46fc924460794701896c8fa535351ee4e4ec54..914e20b0540966bd19902cf360425539a65dd73e 100644 (file)
--- 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 9f56a1cd3ad5e9ef103195153abf5d1dbc2cdb85..dc275218f2df1935ce2619d4db25dc30546be09b 100644 (file)
--- 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 17971f184cf28abcbcade1b4f0740635d013be8c..bda2376762fd4181b1967a1027d203a3bc09fcc1 100644 (file)
--- 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 bdb6806134435492413a0f4d6ee83b5d26f09923..4b7870c780042bfa361991351e70d8f2cea40432 100644 (file)
--- 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 d01f5f5ff45a922356696487928fc952c87edcb0..ed1ea6ddf01d09df6da86f533e5e54dc0a55ad1d 100644 (file)
--- 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)))