diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-ex1-grammar.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test-user.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test.smt2 | 2 |
5 files changed, 8 insertions, 6 deletions
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))) |