diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-18 10:07:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 10:07:18 -0500 |
commit | 406bcd32cbf8a1ee48af02fc6cddc618158762f0 (patch) | |
tree | 2c879879426023392988e0218d0357270f6dd433 /src/parser/smt2/smt2.h | |
parent | 9a3adaec00e4d36619a2eb78756914b22cde2a36 (diff) |
Introducing internal commands for SyGuS commands (#2627)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 80bd8df83..2d57332af 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -273,35 +273,6 @@ private: std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); - void addSygusConstraint(Expr constraint) { - d_sygusConstraints.push_back(constraint); - } - - Expr getSygusConstraints() { - switch(d_sygusConstraints.size()) { - case 0: return getExprManager()->mkConst(bool(true)); - case 1: return d_sygusConstraints[0]; - default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints); - } - } - - const std::vector<Expr>& getSygusVars() { - return d_sygusVars; - } - /** retrieves the invariant variables (both regular and primed) - * - * To ensure that the variable list represent the correct argument type order - * the type of the invariant predicate is used during the variable retrieval - */ - const void getSygusInvVars(FunctionType t, - std::vector<Expr>& vars, - std::vector<Expr>& primed_vars); - - const void addSygusFunSymbol( Type t, Expr synth_fun ); - const std::vector<Expr>& getSygusFunSymbols() { - return d_sygusFunSymbols; - } - /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. |