diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-18 08:34:12 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-18 08:34:12 -0600 |
commit | 3c246952ce90ae7c27b4c0646fce05bc69037f46 (patch) | |
tree | abb7ef449ad0329157a5e5188a7500e8ea1d55c6 /src/printer | |
parent | 8cdef42785fd294d1727ce1df1b11d754c9bb3d1 (diff) |
Use symbol manager for get assignment (#5451)
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.
Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 12 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 7 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 10 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 7 | ||||
-rw-r--r-- | src/printer/printer.cpp | 9 | ||||
-rw-r--r-- | src/printer/printer.h | 7 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 7 |
8 files changed, 0 insertions, 73 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 76549d01d..8bf3bd24e 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -296,18 +296,6 @@ void AstPrinter::toStreamCmdDefineType(std::ostream& out, out << "]," << t << ')' << std::endl; } -void AstPrinter::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const -{ - out << "DefineNamedFunction( "; - toStreamCmdDefineFunction(out, id, formals, range, formula); - out << " )" << std::endl; -} - void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const { out << "Simplify( << " << n << " >> )" << std::endl; diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index ce621d8e1..ad20ffb79 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -79,13 +79,6 @@ class AstPrinter : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const override; - /** Print check-sat command */ void toStreamCmdCheckSat(std::ostream& out, Node n = Node::null()) const override; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8b252d0ea..44ff7be10 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1410,16 +1410,6 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out, } } -void CvcPrinter::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const -{ - toStreamCmdDefineFunction(out, id, formals, range, formula); -} - void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const { out << "TRANSFORM " << n << ';' << std::endl; diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 934caf91b..ee4750a61 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -80,13 +80,6 @@ class CvcPrinter : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const override; - /** Print check-sat command */ void toStreamCmdCheckSat(std::ostream& out, Node n = Node::null()) const override; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 21eb88c8c..b24025124 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -184,15 +184,6 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out, printUnknownCommand(out, "define-fun"); } -void Printer::toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const -{ - printUnknownCommand(out, "define-named-function"); -} - void Printer::toStreamCmdDefineFunctionRec( std::ostream& out, const std::vector<Node>& funcs, diff --git a/src/printer/printer.h b/src/printer/printer.h index ffacaa5d8..d32418deb 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -103,13 +103,6 @@ class Printer TypeNode range, Node formula) const; - /** Print define-named-fun command */ - virtual void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const; - /** Print define-fun-rec command */ virtual void toStreamCmdDefineFunctionRec( std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6628576dd..bed6a890b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1715,20 +1715,6 @@ void Smt2Printer::toStreamCmdDefineType(std::ostream& out, out << ") " << t << ")" << std::endl; } -void Smt2Printer::toStreamCmdDefineNamedFunction( - std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const -{ - out << "DefineNamedFunction( "; - toStreamCmdDefineFunction(out, id, formals, range, formula); - out << " )" << std::endl; - - printUnknownCommand(out, "define-named-function"); -} - void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const { out << "(simplify " << n << ')' << std::endl; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 3fc144d46..bc8674275 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -92,13 +92,6 @@ class Smt2Printer : public CVC4::Printer TypeNode range, Node formula) const override; - /** Print define-named-fun command */ - void toStreamCmdDefineNamedFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const override; - /** Print define-fun-rec command */ void toStreamCmdDefineFunctionRec( std::ostream& out, |