diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-28 11:59:28 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-28 13:59:28 -0500 |
| commit | e8bbee7afb039834955aee96d181b499550a28fe (patch) | |
| tree | 46913b75f97fa8a03d7eaeb1a8602090ea31c877 /src/smt | |
| parent | b224d8415386f685db31ce49f3cd331be842729e (diff) | |
Replace Expr with Node in Term/Op (#4781)
This commit changes Term and Op to use Nodes internally instead of
Exprs. This is a step towards removing the Expr-layer. This commit also
adds some missing checks regarding the number of arguments for a given
kind that were previously missing, which caused issues in unit tests when
using Node instead of Expr.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9ff6ec6f5..d8657c7dd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1731,14 +1731,14 @@ void SmtEngine::declareSynthFun(const std::string& id, setSygusConjectureStale(); } -void SmtEngine::assertSygusConstraint(Expr constraint) +void SmtEngine::assertSygusConstraint(const Node& constraint) { SmtScope smts(this); finalOptionsAreSet(); d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; - Dump("raw-benchmark") << SygusConstraintCommand(constraint); + Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr()); // sygus conjecture is now stale setSygusConjectureStale(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b38ec2d7a..a651b8d1e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -453,7 +453,7 @@ class CVC4_PUBLIC SmtEngine const std::vector<Expr>& vars); /** Add a regular sygus constraint.*/ - void assertSygusConstraint(Expr constraint); + void assertSygusConstraint(const Node& constraint); /** * Add an invariant constraint. |