diff options
Diffstat (limited to 'src/smt/sygus_solver.h')
| -rw-r--r-- | src/smt/sygus_solver.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 3db615037..90a6a87f0 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -82,8 +82,8 @@ class SygusSolver bool isInv, const std::vector<Node>& vars); - /** Add a regular sygus constraint.*/ - void assertSygusConstraint(Node constraint); + /** Add a regular sygus constraint or assumption.*/ + void assertSygusConstraint(Node n, bool isAssume); /** * Add an invariant constraint. @@ -185,6 +185,8 @@ class SygusSolver std::vector<Node> d_sygusVars; /** sygus constraints */ std::vector<Node> d_sygusConstraints; + /** sygus assumptions */ + std::vector<Node> d_sygusAssumps; /** functions-to-synthesize */ std::vector<Node> d_sygusFunSymbols; /** |