diff options
Diffstat (limited to 'src')
57 files changed, 659 insertions, 447 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 869699ac5..e56379f0c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1137,7 +1137,6 @@ install(FILES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4) install(FILES - expr/array.h expr/array_store_all.h expr/ascription_type.h expr/emptyset.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5eabcfe62..748a1ce06 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -354,6 +354,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::DISTINCT, DISTINCT}, {CVC4::Kind::VARIABLE, CONSTANT}, {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, + {CVC4::Kind::SEXPR, SEXPR}, {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::WITNESS, WITNESS}, /* Boolean --------------------------------------------------------- */ @@ -822,6 +823,14 @@ class CVC4ApiRecoverableExceptionStream << "Invalid argument '" << arg << "' for '" << #arg \ << "', expected " +#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiRecoverableExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 \ @@ -842,6 +851,10 @@ class CVC4ApiRecoverableExceptionStream { #define CVC4_API_SOLVER_TRY_CATCH_END \ } \ + catch (const UnrecognizedOptionException& e) \ + { \ + throw CVC4ApiRecoverableException(e.getMessage()); \ + } \ catch (const CVC4::RecoverableModalException& e) \ { \ throw CVC4ApiRecoverableException(e.getMessage()); \ @@ -5083,7 +5096,7 @@ std::vector<Term> Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; return d_smtEngine->getInfo(flag).toString(); @@ -5415,7 +5428,7 @@ void Solver::resetAssertions(void) const void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED( + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( keyword == "source" || keyword == "category" || keyword == "difficulty" || keyword == "filename" || keyword == "license" || keyword == "name" || keyword == "notes" || keyword == "smt-lib-version" @@ -5423,10 +5436,10 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const keyword) << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " "'notes', 'smt-lib-version' or 'status'"; - CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" - || value == "2.0" || value == "2.5" - || value == "2.6", - value) + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( + keyword != "smt-lib-version" || value == "2" || value == "2.0" + || value == "2.5" || value == "2.6", + value) << "'2.0', '2.5', '2.6'"; CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" || value == "unsat" || value == "unknown", diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 18de83e90..391db4bd4 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -9,7 +9,6 @@ ## directory for licensing information. ## libcvc4_add_sources( - array.h array_store_all.cpp array_store_all.h ascription_type.cpp diff --git a/src/expr/array.h b/src/expr/array.h deleted file mode 100644 index 620e61ea0..000000000 --- a/src/expr/array.h +++ /dev/null @@ -1,26 +0,0 @@ -/********************* */ -/*! \file array.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Array types. - ** - ** Array types. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__ARRAY_H -#define CVC4__ARRAY_H - -// we get ArrayType right now by #including type.h. -// array.h is still useful for the auto-generated kinds #includes. -#include "expr/type.h" - -#endif /* CVC4__ARRAY_H */ diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 19efe6285..58dfd973c 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -959,11 +959,13 @@ enum class PfRule : uint32_t // fixed length of component i of the regular expression concatenation R. RE_UNFOLD_NEG_CONCAT_FIXED, // ======== Regular expression elimination - // Children: (P:F) - // Arguments: none + // Children: none + // Arguments: (F, b) // --------------------- - // Conclusion: R - // where R = strings::RegExpElimination::eliminate(F). + // Conclusion: (= F strings::RegExpElimination::eliminate(F, b)) + // where b is a Boolean indicating whether we are using aggressive + // eliminations. Notice this rule concludes (= F F) if no eliminations + // are performed for F. RE_ELIM, //======================== Code points // Children: none diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 35bed1dbf..d6a632ac5 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -24,7 +24,6 @@ #include <vector> #include "base/exception.h" -#include "expr/expr.h" #include "expr/type.h" namespace CVC4 { diff --git a/src/expr/type.h b/src/expr/type.h index 0b923f027..0c70b1667 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -35,9 +35,6 @@ struct CVC4_PUBLIC ExprManagerMapCollection; class SmtEngine; -class CVC4_PUBLIC Datatype; -class Record; - template <bool ref_count> class NodeTemplate; diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 264d065d6..723f805b7 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -22,8 +22,8 @@ #include <sstream> #include "base/check.h" -#include "expr/expr.h" #include "expr/kind.h" +#include "expr/node.h" #include "expr/type_node.h" #include "options/language.h" diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 673c5ddd9..ab2c8a218 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -209,7 +209,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { "--tear-down-incremental doesn't work in interactive mode"); } if(!opts.wasSetByUserIncrementalSolving()) { - cmd.reset(new SetOptionCommand("incremental", SExpr(true))); + cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); } @@ -246,7 +246,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) { // For tear-down-incremental values greater than 1, need incremental // on too. - cmd.reset(new SetOptionCommand("incremental", SExpr(true))); + cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); // if(opts.wasSetByUserIncrementalSolving()) { @@ -410,7 +410,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } else { if(!opts.wasSetByUserIncrementalSolving()) { - cmd.reset(new SetOptionCommand("incremental", SExpr(false))); + cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); pExecutor->doCommand(cmd); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 91c7d0ded..30edf86cd 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -686,7 +686,7 @@ options { backtrack = true; } mainCommand[std::unique_ptr<CVC4::Command>* cmd] @init { api::Term f; - SExpr sexpr; + api::Term sexpr; std::string id; api::Sort t; std::vector<CVC4::api::DatatypeDecl> dts; @@ -715,14 +715,14 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) ( symbolicExpr[sexpr] { if(s == "logic") { - cmd->reset(new SetBenchmarkLogicCommand(sexpr.getValue())); + cmd->reset(new SetBenchmarkLogicCommand(sexprToString(sexpr))); } else { - cmd->reset(new SetOptionCommand(s, sexpr)); + cmd->reset(new SetOptionCommand(s, sexprToString(sexpr))); } } - | TRUE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("true"))); } - | FALSE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("false"))); } - | { cmd->reset(new SetOptionCommand(s, SExpr("true"))); } + | TRUE_TOK { cmd->reset(new SetOptionCommand(s, "true")); } + | FALSE_TOK { cmd->reset(new SetOptionCommand(s, "false")); } + | { cmd->reset(new SetOptionCommand(s, "true")); } ) /* push / pop */ @@ -832,8 +832,8 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] { UNSUPPORTED("CALL command"); } | ECHO_TOK - ( simpleSymbolicExpr[sexpr] - { cmd->reset(new EchoCommand(sexpr.getValue())); } + ( simpleSymbolicExpr[s] + { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -939,34 +939,31 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] | toplevelDeclaration[cmd] ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] -@declarations { - std::string s; - CVC4::Rational r; -} +simpleSymbolicExpr[std::string& s] : INTEGER_LITERAL - { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = AntlrInput::tokenText($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL - { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = std::to_string(MINUS_TOK) + AntlrInput::tokenText($INTEGER_LITERAL); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + { s = AntlrInput::tokenText($DECIMAL_LITERAL); } | HEX_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); } + { s = AntlrInput::tokenText($HEX_LITERAL); } | BINARY_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); } + { s = AntlrInput::tokenText($BINARY_LITERAL); } | str[s] - { sexpr = SExpr(s); } | IDENTIFIER - { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); } + { s = AntlrInput::tokenText($IDENTIFIER); } ; -symbolicExpr[CVC4::SExpr& sexpr] +symbolicExpr[CVC4::api::Term& sexpr] @declarations { - std::vector<SExpr> children; + std::string s; + std::vector<api::Term> children; } - : simpleSymbolicExpr[sexpr] + : simpleSymbolicExpr[s] + { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN - { sexpr = SExpr(children); } + { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); } ; /** diff --git a/src/parser/parser.h b/src/parser/parser.h index 96a16b31f..686a0d147 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -803,7 +803,6 @@ public: */ api::Term mkStringConstant(const std::string& s); - private: /** ad-hoc string escaping * * Returns the (internal) vector of code points corresponding to processing diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88035dba4..6eb3d8061 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -722,29 +722,27 @@ sygusGrammar[CVC4::api::Grammar*& ret, setInfoInternal[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; - SExpr sexpr; + api::Term sexpr; } : KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setInfo(name.c_str() + 1, sexpr); - cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr)); + cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); } ; setOptionInternal[std::unique_ptr<CVC4::Command>* cmd] @init { std::string name; - SExpr sexpr; + api::Term sexpr; } : keyword[name] symbolicExpr[sexpr] - { PARSER_STATE->setOption(name.c_str() + 1, sexpr); - cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr)); + { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr))); // Ugly that this changes the state of the parser; but // global-declarations affects parsing, so we can't hold off // on this until some SmtEngine eventually (if ever) executes it. if(name == ":global-declarations") { - SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true"); + SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true"); } } ; @@ -755,7 +753,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] std::string fname; CVC4::api::Term expr, expr2; std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; - SExpr sexpr; + std::string s; CVC4::api::Sort t; CVC4::api::Term func; std::vector<CVC4::api::Term> bvs; @@ -786,8 +784,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] /* echo */ | ECHO_TOK - ( simpleSymbolicExpr[sexpr] - { cmd->reset(new EchoCommand(sexpr.toString())); } + ( simpleSymbolicExpr[s] + { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -1246,30 +1244,17 @@ datatypesDef[bool isCo, } ; -simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] -@declarations { - CVC4::Kind k; - std::string s; - std::vector<unsigned int> s_vec; -} +simpleSymbolicExprNoKeyword[std::string& s] : INTEGER_LITERAL - { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = AntlrInput::tokenText($INTEGER_LITERAL); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + { s = AntlrInput::tokenText($DECIMAL_LITERAL); } | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - sexpr = SExpr(Integer(hexString, 16)); - } + { s = AntlrInput::tokenText($HEX_LITERAL); } | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - sexpr = SExpr(Integer(binString, 2)); - } + { s = AntlrInput::tokenText($BINARY_LITERAL); } | str[s,false] - { sexpr = SExpr(s); } | symbol[s,CHECK_NONE,SYM_SORT] - { sexpr = SExpr(SExpr::Keyword(s)); } | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK @@ -1279,7 +1264,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK) - { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } + { s = AntlrInput::tokenText($tok); } ; keyword[std::string& s] @@ -1287,20 +1272,21 @@ keyword[std::string& s] { s = AntlrInput::tokenText($KEYWORD); } ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] - : simpleSymbolicExprNoKeyword[sexpr] - | KEYWORD - { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } +simpleSymbolicExpr[std::string& s] + : simpleSymbolicExprNoKeyword[s] + | KEYWORD { s = AntlrInput::tokenText($KEYWORD); } ; -symbolicExpr[CVC4::SExpr& sexpr] +symbolicExpr[CVC4::api::Term& sexpr] @declarations { - std::vector<SExpr> children; + std::string s; + std::vector<api::Term> children; } - : simpleSymbolicExpr[sexpr] + : simpleSymbolicExpr[s] + { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN_TOK ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK - { sexpr = SExpr(children); } + { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); } ; /** @@ -1781,13 +1767,14 @@ termAtomic[CVC4::api::Term& atomTerm] */ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] @init { - SExpr sexpr; + api::Term sexpr; + std::string s; CVC4::api::Term patexpr; std::vector<CVC4::api::Term> patexprs; CVC4::api::Term e2; bool hasValue = false; } - : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )? + : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )? { attr = AntlrInput::tokenText($KEYWORD); PARSER_STATE->attributeNotSupported(attr); @@ -1824,7 +1811,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] { api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = SOLVER->mkConst(boolType, sexpr.toString()); + api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr)); attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand("qid", avar); @@ -1835,7 +1822,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] { attr = std::string(":named"); // notify that expression was given a name - PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue()); + PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr)); } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b9279fcb0..17f5661b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -750,14 +750,6 @@ bool Smt2::sygus_v2() const return getLanguage() == language::input::LANG_SYGUS_V2; } -void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { - // TODO: ??? -} - -void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { - // TODO: ??? -} - void Smt2::checkThatLogicIsSet() { if (!logicIsSet()) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fd08ab241..654ff9fbf 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -261,10 +261,6 @@ class Smt2 : public Parser */ bool escapeDupDblQuote() const { return v2_5() || sygus(); } - void setInfo(const std::string& flag, const SExpr& sexpr); - - void setOption(const std::string& flag, const SExpr& sexpr); - void checkThatLogicIsSet(); /** diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 447a867c8..6b66b5422 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -259,7 +259,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if(filename.substr(filename.length() - 2) == ".p") { filename = filename.substr(0, filename.length() - 2); } - seq->addCommand(new SetInfoCommand("filename", SExpr(filename))); + seq->addCommand(new SetInfoCommand("filename", filename)); if(PARSER_STATE->hasConjecture()) { seq->addCommand(new QueryCommand(SOLVER->mkFalse())); } else { diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 4b9371181..30b09acae 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -24,10 +24,9 @@ #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" #include "options/language.h" // for LANG_AST -#include "printer/dagification_visitor.h" +#include "printer/let_binding.h" #include "smt/command.h" #include "smt/node_command.h" -#include "theory/substitutions.h" using namespace std; @@ -41,38 +40,17 @@ void AstPrinter::toStream(std::ostream& out, size_t dag) const { if(dag != 0) { - DagificationVisitor dv(dag); - NodeVisitor<DagificationVisitor> visitor; - visitor.run(dv, n); - const theory::SubstitutionMap& lets = dv.getLets(); - if(!lets.empty()) { - out << "(LET "; - bool first = true; - for(theory::SubstitutionMap::const_iterator i = lets.begin(); - i != lets.end(); - ++i) { - if(! first) { - out << ", "; - } else { - first = false; - } - toStream(out, (*i).second, toDepth, false); - out << " := "; - toStream(out, (*i).first, toDepth, false); - } - out << " IN "; - } - Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth); - if(!lets.empty()) { - out << ')'; - } + LetBinding lbind(dag + 1); + toStreamWithLetify(out, n, toDepth, &lbind); } else { toStream(out, n, toDepth); } } -void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const +void AstPrinter::toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind) const { // null if(n.getKind() == kind::NULL_EXPR) { @@ -96,12 +74,28 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const // constant out << ' '; kind::metakind::NodeValueConstPrinter::toStream(out, n); - } else { + } + else if (n.isClosure()) + { + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + // body is re-letified + if (i == 1) + { + toStreamWithLetify(out, n[i], toDepth, lbind); + continue; + } + toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind); + } + } + else + { // operator if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { out << ' '; if(toDepth != 0) { - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1); + toStream( + out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } @@ -114,7 +108,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const out << ' '; } if(toDepth != 0) { - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } @@ -394,6 +388,50 @@ void AstPrinter::toStreamCmdComment(std::ostream& out, out << "CommentCommand([" << comment << "])" << std::endl; } +void AstPrinter::toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const +{ + if (lbind == nullptr) + { + toStream(out, n, toDepth); + return; + } + std::stringstream cparen; + std::vector<Node> letList; + lbind->letify(n, letList); + if (!letList.empty()) + { + std::map<Node, uint32_t>::const_iterator it; + out << "(LET "; + cparen << ")"; + bool first = true; + for (size_t i = 0, nlets = letList.size(); i < nlets; i++) + { + if (!first) + { + out << ", "; + } + else + { + first = false; + } + Node nl = letList[i]; + uint32_t id = lbind->getId(nl); + out << "_let_" << id << " := "; + Node nlc = lbind->convert(nl, "_let_", false); + toStream(out, nlc, toDepth, lbind); + } + out << " IN "; + } + Node nc = lbind->convert(n, "_let_"); + // print the body, passing the lbind object + toStream(out, nc, toDepth, lbind); + out << cparen.str(); + lbind->popScope(); +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index e4251eba0..e0bc7b6bf 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -24,6 +24,9 @@ #include "printer/printer.h" namespace CVC4 { + +class LetBinding; + namespace printer { namespace ast { @@ -162,7 +165,10 @@ class AstPrinter : public CVC4::Printer std::ostream& out, const std::vector<Command*>& sequence) const override; private: - void toStream(std::ostream& out, TNode n, int toDepth) const; + void toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind = nullptr) const; /** * To stream model sort. This prints the appropriate output for type * tn declared via declare-sort or declare-datatype. @@ -178,6 +184,14 @@ class AstPrinter : public CVC4::Printer void toStreamModelTerm(std::ostream& out, const smt::Model& m, Node n) const override; + /** + * To stream with let binding. This prints n, possibly in the scope + * of letification generated by this method based on lbind. + */ + void toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const; }; /* class AstPrinter */ } // namespace ast diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9e9500bdb..d3e9b48e4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -40,7 +40,6 @@ #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/substitutions.h" #include "theory/theory_model.h" #include "util/smt2_quote_string.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e6361be9e..14b9ed0aa 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -29,7 +29,7 @@ #include "expr/expr_iomanip.h" #include "expr/node.h" #include "expr/symbol_manager.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -45,6 +45,43 @@ using namespace std; namespace CVC4 { +std::string sexprToString(api::Term sexpr) +{ + // if sexpr is a spec constant and not a string, return the result of calling + // Term::toString + if (sexpr.getKind() == api::CONST_BOOLEAN + || sexpr.getKind() == api::CONST_FLOATINGPOINT + || sexpr.getKind() == api::CONST_RATIONAL) + { + return sexpr.toString(); + } + + // if sexpr is a constant string, return the result of calling Term::toString. + // However, strip the surrounding quotes + if (sexpr.getKind() == api::CONST_STRING) + { + return sexpr.toString().substr(1, sexpr.toString().length() - 2); + } + + // if sexpr is not a spec constant, make sure it is an array of sub-sexprs + Assert(sexpr.getKind() == api::SEXPR); + + std::stringstream ss; + auto it = sexpr.begin(); + + // recursively print the sub-sexprs + ss << '(' << sexprToString(*it); + ++it; + while (it != sexpr.end()) + { + ss << ' ' << sexprToString(*it); + ++it; + } + ss << ')'; + + return ss.str(); +} + const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); const CommandInterrupted* CommandInterrupted::s_instance = @@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(const api::Solver* solver) - : d_commandStatus(nullptr), d_muted(false) -{ -} - Command::Command(const Command& cmd) { d_commandStatus = @@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out, /* class SetInfoCommand */ /* -------------------------------------------------------------------------- */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) +SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetInfoCommand::getFlag() const { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } +const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; } void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setInfo(d_flag, d_sexpr); + solver->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.emplace_back(solver->getSmtEngine()->getInfo(d_flag)); - stringstream ss; - if (d_flag == "all-options" || d_flag == "all-statistics") - { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); + std::vector<api::Term> v; + v.push_back(solver->mkString(":" + d_flag)); + v.push_back(solver->mkString(solver->getInfo(d_flag))); + d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) - { - d_commandStatus = new CommandUnsupported(); - } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out, /* class SetOptionCommand */ /* -------------------------------------------------------------------------- */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) +SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetOptionCommand::getFlag() const { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } +const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; } void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setOption(d_flag, d_sexpr); + solver->setOption(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } diff --git a/src/smt/command.h b/src/smt/command.h index 0b86f3539..bfe5e737a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -29,8 +29,6 @@ #include <vector> #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" @@ -51,6 +49,16 @@ namespace smt { class Model; } +/** + * Convert a symbolic expression to string. This method differs from + * Term::toString in that it does not surround constant strings with double + * quote symbols. + * + * @param sexpr the symbolic expression to convert + * @return the symbolic expression as string + */ +std::string sexprToString(api::Term sexpr); + std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC; @@ -198,7 +206,6 @@ class CVC4_PUBLIC Command typedef CommandPrintSuccess printsuccess; Command(); - Command(const api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -1285,13 +1292,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); + SetInfoCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; @@ -1330,13 +1337,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); + SetOptionCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 9d3031b4d..51fcf8b5b 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -14,7 +14,6 @@ #include "smt/dump_manager.h" -#include "expr/expr_manager.h" #include "options/smt_options.h" #include "smt/dump.h" #include "smt/node_command.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 7d34f3373..356cfa8a6 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -15,7 +15,6 @@ #include "smt/listeners.h" #include "expr/attribute.h" -#include "expr/expr.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 92d200d40..5c45a6a56 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -19,7 +19,7 @@ #include <vector> -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 7a28c47f2..327933f1b 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -19,7 +19,7 @@ #include <vector> -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 118b82bec..1916f0162 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -18,7 +18,6 @@ #define CVC4__SMT__PROOF_MANAGER_H #include "context/cdlist.h" -#include "expr/expr.h" #include "expr/node.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e5ecafd4a..4636cf17a 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" @@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {} Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, - bool doFull) + bool doFull, + bool isInternalSubsolver) { Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) @@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + NodeManager* nm = NodeManager::currentNM(); + // ensure the body is rewritten + q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; - NodeManager* nm = NodeManager::currentNM(); // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); @@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // do extended rewrite to minimize the size of the formula aggressively theory::quantifiers::ExtendedRewriter extr(true); ret = extr.extendedRewrite(ret); + // if we are not an internal subsolver, convert to witness form, since + // internally generated skolems should not escape + if (!isInternalSubsolver) + { + ret = SkolemManager::getWitnessForm(ret); + } return ret; } // otherwise, just true/false diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f40db530..d3ba676fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -468,11 +468,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.6" ) { ilang = language::input::LANG_SMTLIB_V2_6; } - else - { - Warning() << "Warning: unsupported smt-lib-version: " << value << endl; - throw UnrecognizedOptionException(); - } options::inputLanguage.set(ilang); // also update the output language if (!options::outputLanguage.wasSetByUser()) @@ -497,7 +492,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_state->notifyExpectedStatus(s); return; } - throw UnrecognizedOptionException(); } bool SmtEngine::isValidGetInfoFlag(const std::string& key) const @@ -517,10 +511,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if (!isValidGetInfoFlag(key)) - { - throw UnrecognizedOptionException(); - } if (key == "all-statistics") { vector<SExpr> stats; @@ -1508,7 +1498,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 78d7f8c38..d2fbeb413 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -23,7 +23,6 @@ #include <algorithm> #include "base/check.h" -#include "expr/expr_manager_scope.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 1e031c322..f4016d032 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -18,7 +18,6 @@ #include <vector> #include "base/output.h" -#include "expr/expr.h" #include "expr/node_algorithm.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 7d7d0c23c..482e3bc21 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -170,31 +170,41 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } -void ExponentialSolver::doSecantLemmas( - TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d) +void ExponentialSolver::doSecantLemmas(TNode e, + TNode poly_approx, + TNode center, + TNode cval, + unsigned d, + unsigned actual_d) { - d_data->doSecantLemmas( - getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1); + d_data->doSecantLemmas(getSecantBounds(e, center, d), + poly_approx, + center, + cval, + e, + Convexity::CONVEX, + d, + actual_d); } std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e, - TNode c, + TNode center, unsigned d) { - std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, c, d); + std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, center, d); // Check if we already have neighboring secant points if (bounds.first.isNull()) { // pick c-1 bounds.first = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one)); } if (bounds.second.isNull()) { // pick c+1 bounds.second = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one)); } return bounds; } diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index b20c23e56..b4d08559a 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -87,12 +87,16 @@ class ExponentialSolver void doTangentLemma(TNode e, TNode c, TNode poly_approx); /** Sent secant lemmas around c for e */ - void doSecantLemmas( - TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d); + void doSecantLemmas(TNode e, + TNode poly_approx, + TNode center, + TNode cval, + unsigned d, + unsigned actual_d); private: /** Generate bounds for secant lemmas */ - std::pair<Node, Node> getSecantBounds(TNode e, TNode c, unsigned d); + std::pair<Node, Node> getSecantBounds(TNode e, TNode center, unsigned d); /** Holds common state for transcendental solvers */ TranscendentalState* d_data; diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 31fd47503..cba85b80e 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -266,19 +266,20 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region) // Figure 3: T( x ) // We use zero slope tangent planes, since the concavity of the Taylor // approximation cannot be easily established. - int concavity = regionToConcavity(region); + Convexity convexity = regionToConvexity(region); int mdir = regionToMonotonicityDir(region); + bool usec = (mdir == 1) == (convexity == Convexity::CONCAVE); Node lem = nm->mkNode( Kind::IMPLIES, nm->mkNode( Kind::AND, - nm->mkNode(Kind::GEQ, - e[0], - mdir == concavity ? Node(c) : regionToLowerBound(region)), - nm->mkNode(Kind::LEQ, - e[0], - mdir != concavity ? Node(c) : regionToUpperBound(region))), - nm->mkNode(concavity == 1 ? Kind::GEQ : Kind::LEQ, e, poly_approx)); + nm->mkNode( + Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)), + nm->mkNode( + Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))), + nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ, + e, + poly_approx)); Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem << std::endl; @@ -294,6 +295,7 @@ void SineSolver::doSecantLemmas(TNode e, TNode c, TNode poly_approx_c, unsigned d, + unsigned actual_d, int region) { d_data->doSecantLemmas(getSecantBounds(e, c, d, region), @@ -301,8 +303,9 @@ void SineSolver::doSecantLemmas(TNode e, c, poly_approx_c, e, + regionToConvexity(region), d, - regionToConcavity(region)); + actual_d); } std::pair<Node, Node> SineSolver::getSecantBounds(TNode e, diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 9f9102a53..e41e6bd4f 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -93,6 +93,7 @@ class SineSolver TNode c, TNode poly_approx_c, unsigned d, + unsigned actual_d, int region); private: @@ -152,15 +153,15 @@ class SineSolver default: return 0; } } - int regionToConcavity(int region) + Convexity regionToConvexity(int region) { switch (region) { case 1: - case 2: return -1; + case 2: return Convexity::CONCAVE; case 3: - case 4: return 1; - default: return 0; + case 4: return Convexity::CONVEX; + default: return Convexity::UNKNOWN; } } diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index a373339e9..1b7257f8f 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -212,7 +212,7 @@ void TaylorGenerator::getPolynomialApproximationBounds( } } -void TaylorGenerator::getPolynomialApproximationBoundForArg( +unsigned TaylorGenerator::getPolynomialApproximationBoundForArg( Kind k, Node c, unsigned d, std::vector<Node>& pbounds) { getPolynomialApproximationBounds(k, d, pbounds); @@ -252,7 +252,9 @@ void TaylorGenerator::getPolynomialApproximationBoundForArg( getPolynomialApproximationBounds(k, ds, pboundss); pbounds[2] = pboundss[2]; } + return ds; } + return d; } std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf, unsigned d, NlModel& model) diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index c647f7fd2..2dbfcccde 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -79,11 +79,13 @@ class TaylorGenerator * polynomials may depend on c. In particular, for P_u+[x] for <k>( c ) where * c>0, we return the P_u+[x] from the function above for the minimum degree * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive. + * @return the actual degree of the polynomial approximations (which may be + * larger than d). */ - void getPolynomialApproximationBoundForArg(Kind k, - Node c, - unsigned d, - std::vector<Node>& pbounds); + unsigned getPolynomialApproximationBoundForArg(Kind k, + Node c, + unsigned d, + std::vector<Node>& pbounds); /** get transcendental function model bounds * diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 8eb69e50b..ad3f49576 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -233,7 +233,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) // mapped to for signs of c std::map<int, Node> poly_approx_bounds[2]; std::vector<Node> pbounds; - d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds); + unsigned actual_d = + d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds); poly_approx_bounds[0][1] = pbounds[0]; poly_approx_bounds[0][-1] = pbounds[1]; poly_approx_bounds[1][1] = pbounds[2]; @@ -362,11 +363,12 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) { if (k == EXPONENTIAL) { - d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d); + d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d); } else if (k == Kind::SINE) { - d_sineSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, region); + d_sineSlv.doSecantLemmas( + tf, poly_approx, c, poly_approx_c, d, actual_d, region); } } return true; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 41ed2c53d..69678c621 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -267,26 +267,26 @@ void TranscendentalState::getCurrentPiBounds() } std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e, - TNode c, + TNode center, unsigned d) { // bounds are the minimum and maximum previous secant points // should not repeat secant points: secant lemmas should suffice to // rule out previous assignment - Assert( - std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c) - == d_secant_points[e][d].end()); + Assert(std::find( + d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center) + == d_secant_points[e][d].end()); // Insert into the (temporary) vector. We do not update this vector // until we are sure this secant plane lemma has been processed. We do // this by mapping the lemma to a side effect below. std::vector<Node> spoints = d_secant_points[e][d]; - spoints.push_back(c); + spoints.push_back(center); // sort sortByNlModel(spoints.begin(), spoints.end(), &d_model); // get the resulting index of c unsigned index = - std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); + std::find(spoints.begin(), spoints.end(), center) - spoints.begin(); // bounds are the next closest upper/lower bound values return {index > 0 ? spoints[index - 1] : Node(), @@ -294,24 +294,40 @@ std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e, } Node TranscendentalState::mkSecantPlane( - TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c) + TNode arg, TNode lower, TNode upper, TNode lval, TNode uval) { NodeManager* nm = NodeManager::currentNM(); // Figure 3: S_l( x ), S_u( x ) for s = 0,1 - Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c)); + Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper)); Assert(rcoeff_n.isConst()); Rational rcoeff = rcoeff_n.getConst<Rational>(); Assert(rcoeff.sgn() != 0); - return nm->mkNode(Kind::PLUS, - approx_b, - nm->mkNode(Kind::MULT, - nm->mkNode(Kind::MINUS, approx_b, approx_c), - nm->mkConst(rcoeff.inverse()), - nm->mkNode(Kind::MINUS, arg, b))); + Node res = + nm->mkNode(Kind::PLUS, + lval, + nm->mkNode(Kind::MULT, + nm->mkNode(Kind::DIVISION, + nm->mkNode(Kind::MINUS, lval, uval), + nm->mkNode(Kind::MINUS, lower, upper)), + nm->mkNode(Kind::MINUS, arg, lower))); + Trace("nl-trans") << "Creating secant plane for transcendental function of " + << arg << std::endl; + Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( " + << upper << " ; " << uval << " )" << std::endl; + Trace("nl-trans") << "\t" << res << std::endl; + Trace("nl-trans") << "\trewritten: " << Rewriter::rewrite(res) << std::endl; + return res; } -NlLemma TranscendentalState::mkSecantLemma( - TNode lower, TNode upper, int concavity, TNode tf, TNode splane) +NlLemma TranscendentalState::mkSecantLemma(TNode lower, + TNode upper, + TNode lapprox, + TNode uapprox, + int csign, + Convexity convexity, + TNode tf, + TNode splane, + unsigned actual_d) { NodeManager* nm = NodeManager::currentNM(); // With respect to Figure 3, this is slightly different. @@ -329,60 +345,73 @@ NlLemma TranscendentalState::mkSecantLemma( Node antec_n = nm->mkNode(Kind::AND, nm->mkNode(Kind::GEQ, tf[0], lower), nm->mkNode(Kind::LEQ, tf[0], upper)); + Trace("nl-trans") << "Bound for secant plane: " << lower << " <= " << tf[0] + << " <= " << upper << std::endl; + Trace("nl-trans") << "\t" << antec_n << std::endl; + // Convex: actual value is below the secant + // Concave: actual value is above the secant Node lem = nm->mkNode( Kind::IMPLIES, antec_n, - nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane)); - Trace("nl-ext-tftp-debug2") - << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl; + nm->mkNode( + convexity == Convexity::CONVEX ? Kind::LEQ : Kind::GEQ, tf, splane)); + Trace("nl-trans-lemma") << "*** Secant plane lemma (pre-rewrite) : " << lem + << std::endl; lem = Rewriter::rewrite(lem); - Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl; + Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl; Assert(d_model.computeAbstractModelValue(lem) == d_false); return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT); } void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds, TNode poly_approx, - TNode c, - TNode approx_c, + TNode center, + TNode cval, TNode tf, + Convexity convexity, unsigned d, - int concavity) + unsigned actual_d) { - Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first - << " ... " << bounds.second << std::endl; - // take the model value of l or u (since may contain PI) - // Make secant from bounds.first to c - Node lval = d_model.computeAbstractModelValue(bounds.first); - Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first - << " is " << lval << std::endl; - if (lval != c) + int csign = center.getConst<Rational>().sgn(); + Trace("nl-trans") << "...do secant lemma with center " << center << " val " + << cval << " sign " << csign << std::endl; + Trace("nl-trans") << "...secant bounds are : " << bounds.first << " ... " + << bounds.second << std::endl; + // take the model value of lower (since may contain PI) + // Make secant from bounds.first to center + Node lower = d_model.computeAbstractModelValue(bounds.first); + Trace("nl-trans") << "...model value of bound " << bounds.first << " is " + << lower << std::endl; + if (lower != center) { // Figure 3 : P(l), P(u), for s = 0 - Node approx_l = Rewriter::rewrite( - poly_approx.substitute(d_taylor.getTaylorVariable(), lval)); - Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c); - NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane); + Node lval = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), lower)); + Node splane = mkSecantPlane(tf[0], lower, center, lval, cval); + NlLemma nlem = mkSecantLemma( + lower, center, lval, cval, csign, convexity, tf, splane, actual_d); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). - nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); d_im.addPendingArithLemma(nlem, true); } - // Make secant from c to bounds.second - Node uval = d_model.computeAbstractModelValue(bounds.second); - Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second - << " is " << uval << std::endl; - if (c != uval) + // take the model value of upper (since may contain PI) + // Make secant from center to bounds.second + Node upper = d_model.computeAbstractModelValue(bounds.second); + Trace("nl-trans") << "...model value of bound " << bounds.second << " is " + << upper << std::endl; + if (center != upper) { // Figure 3 : P(l), P(u), for s = 1 - Node approx_u = Rewriter::rewrite( - poly_approx.substitute(d_taylor.getTaylorVariable(), uval)); - Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u); - NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane); + Node uval = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), upper)); + Node splane = mkSecantPlane(tf[0], center, upper, cval, uval); + NlLemma nlem = mkSecantLemma( + center, upper, cval, uval, csign, convexity, tf, splane, actual_d); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). - nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); d_im.addPendingArithLemma(nlem, true); } } diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 0a4e46eca..e1510c3b3 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -27,6 +27,24 @@ namespace nl { namespace transcendental { /** + * This enum indicates whether some function is convex, concave or unknown at + * some point. + */ +enum class Convexity +{ + CONVEX, + CONCAVE, + UNKNOWN +}; +inline std::ostream& operator<<(std::ostream& os, Convexity c) { + switch (c) { + case Convexity::CONVEX: return os << "CONVEX"; + case Convexity::CONCAVE: return os << "CONCAVE"; + default: return os << "UNKNOWN"; + } +} + +/** * Holds common state and utilities for transcendental solvers. * * This includes common lookups and caches as well as generic utilities for @@ -60,20 +78,24 @@ struct TranscendentalState * Get the two closest secant points from the once stored already. * "closest" is determined according to the current model. * @param e The transcendental term (like (exp t)) - * @param c The point currently under consideration (probably the model of t) + * @param center The point currently under consideration (probably the model + * of t) * @param d The taylor degree. */ - std::pair<Node, Node> getClosestSecantPoints(TNode e, TNode c, unsigned d); + std::pair<Node, Node> getClosestSecantPoints(TNode e, + TNode center, + unsigned d); /** - * Construct a secant plane between b and c + * Construct a secant plane as function in arg between lower and upper * @param arg The argument of the transcendental term - * @param b Left secant point - * @param c Right secant point - * @param approx Approximation for b (not yet substituted) - * @param approx_c Approximation for c (already substituted) + * @param lower Left secant point + * @param upper Right secant point + * @param lval Evaluation at lower + * @param uval Evaluation at upper */ - Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c); + Node mkSecantPlane( + TNode arg, TNode lower, TNode upper, TNode lval, TNode uval); /** * Construct a secant lemma between lower and upper for tf. @@ -83,26 +105,34 @@ struct TranscendentalState * @param tf Current transcendental term * @param splane Secant plane as computed by mkSecantPlane() */ - NlLemma mkSecantLemma( - TNode lower, TNode upper, int concavity, TNode tf, TNode splane); + NlLemma mkSecantLemma(TNode lower, + TNode upper, + TNode lapprox, + TNode uapprox, + int csign, + Convexity convexity, + TNode tf, + TNode splane, + unsigned actual_d); /** * Construct and send secant lemmas (if appropriate) * @param bounds Secant bounds * @param poly_approx Polynomial approximation - * @param c Current point - * @param approx_c Approximation for c + * @param center Current point + * @param cval Evaluation at c * @param tf Current transcendental term * @param d Current taylor degree * @param concavity Concavity in region of c */ void doSecantLemmas(const std::pair<Node, Node>& bounds, TNode poly_approx, - TNode c, - TNode approx_c, + TNode center, + TNode cval, TNode tf, + Convexity convexity, unsigned d, - int concavity); + unsigned actual_d); Node d_true; Node d_false; diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index a0def66c5..a090a58fe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,7 +21,6 @@ #include "expr/dtype.h" #include "expr/kind.h" -#include "expr/type.h" #include "expr/type_node.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 85482bf6d..858710746 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } FpConverter::FpConverter(context::UserContext* user) - : + : d_additionalAssertions(user) #ifdef CVC4_USE_SYMFPU + , d_fpMap(user), d_rmMap(user), d_boolMap(user), d_ubvMap(user), - d_sbvMap(user), + d_sbvMap(user) #endif - d_additionalAssertions(user) { } +FpConverter::~FpConverter() {} + #ifdef CVC4_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 59e65c9e1..6688e8607 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -14,6 +14,8 @@ ** Uses the symfpu library to convert from floating-point operations to ** bit-vectors and propositions allowing the theory to be solved by ** 'bit-blasting'. + ** + ** !!! This header is not to be included in any other headers !!! **/ #include "cvc4_private.h" @@ -26,7 +28,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "theory/valuation.h" #include "util/bitvector.h" #include "util/floatingpoint_size.h" @@ -49,10 +51,6 @@ namespace CVC4 { namespace theory { namespace fp { -typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction, - TypeNodeHashFunction> - PairTypeNodeHashFunction; - /** * This is a symfpu symbolic "back-end". It allows the library to be used to * construct bit-vector expressions that compute floating-point operations. @@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize */ class FpConverter { + public: + /** Constructor. */ + FpConverter(context::UserContext*); + /** Destructor. */ + ~FpConverter(); + + /** Adds a node to the conversion, returns the converted node */ + Node convert(TNode); + + /** Gives the node representing the value of a given variable */ + Node getValue(Valuation&, TNode); + + context::CDList<Node> d_additionalAssertions; + protected: #ifdef CVC4_USE_SYMFPU typedef symfpuSymbolic::traits traits; @@ -338,17 +350,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); #endif - - public: - context::CDList<Node> d_additionalAssertions; - - FpConverter(context::UserContext *); - - /** Adds a node to the conversion, returns the converted node */ - Node convert(TNode); - - /** Gives the node representing the value of a given variable */ - Node getValue(Valuation &, TNode); }; } // namespace fp diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 0b15486e2..01fab92c8 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -23,6 +23,7 @@ #include <vector> #include "options/fp_options.h" +#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c, : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), d_notification(*this), d_registeredTerms(u), - d_conv(u), + d_conv(new FpConverter(u)), d_expansionRequested(false), d_conflictNode(c, Node::null()), d_minMap(u), @@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c, d_toUBVMap(u), d_toSBVMap(u), d_toRealMap(u), - realToFloatMap(u), - floatToRealMap(u), - abstractionMap(u), + d_realToFloatMap(u), + d_floatToRealMap(u), + d_abstractionMap(u), d_state(c, u, valuation) { // indicate we are using the default theory state object @@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(realToFloatMap.find(t)); + ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t)); Node fun; - if (i == realToFloatMap.end()) + if (i == d_realToFloatMap.end()) { std::vector<TypeNode> args(2); args[0] = node[0].getType(); @@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node) nm->mkFunctionType(args, node.getType()), "floatingpoint_abstract_real_to_float", NodeManager::SKOLEM_EXACT_NAME); - realToFloatMap.insert(t, fun); + d_realToFloatMap.insert(t, fun); } else { @@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(floatToRealMap.find(t)); + ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t)); Node fun; - if (i == floatToRealMap.end()) + if (i == d_floatToRealMap.end()) { std::vector<TypeNode> args(2); args[0] = t; @@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node) nm->mkFunctionType(args, nm->realType()), "floatingpoint_abstract_float_to_real", NodeManager::SKOLEM_EXACT_NAME); - floatToRealMap.insert(t, fun); + d_floatToRealMap.insert(t, fun); } else { @@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) void TheoryFp::convertAndEquateTerm(TNode node) { Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; - size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size(); - Node converted(d_conv.convert(node)); + Node converted(d_conv->convert(node)); if (converted != node) { Debug("fp-convertTerm") @@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { << "TheoryFp::convertTerm(): after " << converted << std::endl; } - size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size(); Assert(oldAdditionalAssertions <= newAdditionalAssertions); while (oldAdditionalAssertions < newAdditionalAssertions) { - Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions]; + Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions]; Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion " << addA << std::endl; @@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level) TheoryModel* m = getValuation().getModel(); bool lemmaAdded = false; - for (abstractionMapType::const_iterator i = abstractionMap.begin(); - i != abstractionMap.end(); + for (AbstractionMap::const_iterator i = d_abstractionMap.begin(); + i != d_abstractionMap.end(); ++i) { if (m->hasTerm((*i).first)) @@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n) } Node TheoryFp::getModelValue(TNode var) { - return d_conv.getValue(d_valuation, var); + return d_conv->getValue(d_valuation, var); } bool TheoryFp::collectModelInfo(TheoryModel* m, @@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m, } for (std::set<TNode>::const_iterator i(relevantVariables.begin()); - i != relevantVariables.end(); ++i) { + i != relevantVariables.end(); + ++i) + { TNode node = *i; Trace("fp-collectModelInfo") << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true)) + if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true)) { return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 42c009893..fe91a39bd 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -24,7 +24,6 @@ #include <utility> #include "context/cdo.h" -#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -33,7 +32,10 @@ namespace CVC4 { namespace theory { namespace fp { -class TheoryFp : public Theory { +class FpConverter; + +class TheoryFp : public Theory +{ public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp(context::Context* c, @@ -42,8 +44,9 @@ class TheoryFp : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr); + //--------------------------------- initialization - /** get the official theory rewriter of this theory */ + /** Get the official theory rewriter of this theory. */ TheoryRewriter* getTheoryRewriter() override; /** * Returns true if we need an equality engine. If so, we initialize the @@ -51,7 +54,7 @@ class TheoryFp : public Theory { * documentation in Theory::needsEqualityEngine. */ bool needsEqualityEngine(EeSetupInfo& esi) override; - /** finish initialization */ + /** Finish initialization. */ void finishInit() override; //--------------------------------- end initialization @@ -77,8 +80,10 @@ class TheoryFp : public Theory { Node getModelValue(TNode var) override; bool collectModelInfo(TheoryModel* m, const std::set<Node>& relevantTerms) override; - /** Collect model values in m based on the relevant terms given by - * relevantTerms */ + /** + * Collect model values in m based on the relevant terms given by + * relevantTerms. + */ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms) override; @@ -87,7 +92,20 @@ class TheoryFp : public Theory { TrustNode explain(TNode n) override; protected: - /** Equality engine */ + using PairTypeNodeHashFunction = PairHashFunction<TypeNode, + TypeNode, + TypeNodeHashFunction, + TypeNodeHashFunction>; + /** Uninterpreted functions for undefined cases of non-total operators. */ + using ComparisonUFMap = + context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>; + /** Uninterpreted functions for lazy handling of conversions. */ + using ConversionUFMap = context:: + CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>; + using ConversionAbstractionMap = ComparisonUFMap; + using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>; + + /** Equality engine. */ class NotifyClass : public eq::EqualityEngineNotify { protected: TheoryFp& d_theorySolver; @@ -108,14 +126,15 @@ class TheoryFp : public Theory { NotifyClass d_notification; - /** General utility **/ + /** General utility. */ void registerTerm(TNode node); bool isRegistered(TNode node); context::CDHashSet<Node, NodeHashFunction> d_registeredTerms; - /** Bit-blasting conversion */ - FpConverter d_conv; + /** The word-blaster. Translates FP -> BV. */ + std::unique_ptr<FpConverter> d_conv; + bool d_expansionRequested; void convertAndEquateTerm(TNode node); @@ -133,44 +152,30 @@ class TheoryFp : public Theory { */ void conflictEqConstantMerge(TNode t1, TNode t2); - context::CDO<Node> d_conflictNode; - - typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction> - ComparisonUFMap; - - ComparisonUFMap d_minMap; - ComparisonUFMap d_maxMap; + bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); Node minUF(Node); Node maxUF(Node); - typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node, - PairTypeNodeHashFunction> - ConversionUFMap; - - ConversionUFMap d_toUBVMap; - ConversionUFMap d_toSBVMap; - Node toUBVUF(Node); Node toSBVUF(Node); - ComparisonUFMap d_toRealMap; - Node toRealUF(Node); - /** Uninterpretted functions for lazy handling of conversions */ - typedef ComparisonUFMap conversionAbstractionMap; - - conversionAbstractionMap realToFloatMap; - conversionAbstractionMap floatToRealMap; - Node abstractRealToFloat(Node); Node abstractFloatToReal(Node); - typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType; - abstractionMapType abstractionMap; // abstract -> original + private: + context::CDO<Node> d_conflictNode; - bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); + ComparisonUFMap d_minMap; + ComparisonUFMap d_maxMap; + ConversionUFMap d_toUBVMap; + ConversionUFMap d_toSBVMap; + ComparisonUFMap d_toRealMap; + ConversionAbstractionMap d_realToFloatMap; + ConversionAbstractionMap d_floatToRealMap; + AbstractionMap d_abstractionMap; // abstract -> original /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index aa0e62891..a3938412d 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -21,8 +21,7 @@ #include <memory> #include <vector> -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/node.h" #include "smt/smt_engine.h" #include "theory/quantifiers/sygus_sampler.h" diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index 9fc8e703c..d39d2a377 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -19,7 +19,7 @@ #include <string> #include <vector> #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index acafeec3c..48a5dbe06 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -24,7 +24,6 @@ #include "expr/node.h" #include "expr/sygus_datatype.h" -#include "expr/type.h" #include "expr/type_node.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 916f2d9b5..4db5f261a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -20,7 +20,7 @@ #include <vector> #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "smt/smt_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 2214d4beb..daee1762f 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -18,7 +18,7 @@ #include <string> #include <vector> #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 297f11690..da9fdd022 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; + d_lemmas_waiting.clear(); + d_phase_req_waiting.clear(); for( unsigned i=0; i<d_modules.size(); i++ ){ d_modules[i]->presolve(); } diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index f68900ccc..e2742c812 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -22,7 +22,6 @@ #include <memory> #include <vector> -#include "expr/expr_manager.h" #include "expr/node.h" #include "smt/smt_engine.h" diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 0b6cf6652..2726097bc 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -438,9 +438,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::RE_ELIM) { - Assert(children.size() == 1); - Assert(args.empty()); - return RegExpElimination::eliminate(children[0]); + Assert(children.empty()); + Assert(args.size() == 2); + bool isAgg; + if (!getBool(args[1], isAgg)) + { + return Node::null(); + } + Node ea = RegExpElimination::eliminate(args[0], isAgg); + // if we didn't eliminate, then this trivially proves the reflexive equality + if (ea.isNull()) + { + ea = args[0]; + } + return args[0].eqNode(ea); } else if (id == PfRule::STRING_CODE_INJ) { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1d0db0e4d..aaa9ffc48 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,30 +20,58 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; -RegExpElimination::RegExpElimination() +namespace CVC4 { +namespace theory { +namespace strings { + +RegExpElimination::RegExpElimination(bool isAgg, + ProofNodeManager* pnm, + context::Context* c) + : d_isAggressive(isAgg), + d_pnm(pnm), + d_epg(pnm == nullptr + ? nullptr + : new EagerProofGenerator(pnm, c, "RegExpElimination::epg")) { } -Node RegExpElimination::eliminate(Node atom) +Node RegExpElimination::eliminate(Node atom, bool isAgg) { Assert(atom.getKind() == STRING_IN_REGEXP); if (atom[1].getKind() == REGEXP_CONCAT) { - return eliminateConcat(atom); + return eliminateConcat(atom, isAgg); } else if (atom[1].getKind() == REGEXP_STAR) { - return eliminateStar(atom); + return eliminateStar(atom, isAgg); } return Node::null(); } -Node RegExpElimination::eliminateConcat(Node atom) +TrustNode RegExpElimination::eliminateTrusted(Node atom) +{ + Node eatom = eliminate(atom, d_isAggressive); + if (!eatom.isNull()) + { + // Currently aggressive doesnt work due to fresh bound variables + if (isProofEnabled() && !d_isAggressive) + { + Node eq = atom.eqNode(eatom); + Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive); + std::shared_ptr<ProofNode> pn = + d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq); + d_epg->setProofFor(eq, pn); + return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get()); + } + return TrustNode::mkTrustRewrite(atom, eatom, nullptr); + } + return TrustNode::null(); +} + +Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { NodeManager* nm = NodeManager::currentNM(); Node x = atom[0]; @@ -217,7 +245,7 @@ Node RegExpElimination::eliminateConcat(Node atom) // otherwise, we can use indexof to represent some next occurrence if (gap_exact[i + 1] && i + 1 != size) { - if (!options::regExpElimAgg()) + if (!isAgg) { canProcess = false; break; @@ -330,7 +358,7 @@ Node RegExpElimination::eliminateConcat(Node atom) } } - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -455,9 +483,9 @@ Node RegExpElimination::eliminateConcat(Node atom) return Node::null(); } -Node RegExpElimination::eliminateStar(Node atom) +Node RegExpElimination::eliminateStar(Node atom, bool isAgg) { - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -580,3 +608,8 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id) << "." << std::endl; return atomElim; } +bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 0c1acd29d..9d6fecc93 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -18,6 +18,8 @@ #define CVC4__THEORY__STRINGS__REGEXP_ELIM_H #include "expr/node.h" +#include "theory/eager_proof_generator.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { @@ -33,14 +35,32 @@ namespace strings { class RegExpElimination { public: - RegExpElimination(); + /** + * @param isAgg Whether aggressive eliminations are enabled + * @param pnm The proof node manager to use (for proofs) + * @param c The context to use (for proofs) + */ + RegExpElimination(bool isAgg = false, + ProofNodeManager* pnm = nullptr, + context::Context* c = nullptr); /** eliminate membership * * This method takes as input a regular expression membership atom of the * form (str.in.re x R). If this method returns a non-null node ret, then ret * is equivalent to atom. + * + * @param atom The node to eliminate + * @param isAgg Whether we apply aggressive elimination techniques + * @return The node with regular expressions eliminated, or null if atom + * was unchanged. + */ + static Node eliminate(Node atom, bool isAgg); + + /** + * Return the trust node corresponding to rewriting n based on eliminate + * above. */ - static Node eliminate(Node atom); + TrustNode eliminateTrusted(Node atom); private: /** return elimination @@ -50,9 +70,17 @@ class RegExpElimination */ static Node returnElim(Node atom, Node atomElim, const char* id); /** elimination for regular expression concatenation */ - static Node eliminateConcat(Node atom); + static Node eliminateConcat(Node atom, bool isAgg); /** elimination for regular expression star */ - static Node eliminateStar(Node atom); + static Node eliminateStar(Node atom, bool isAgg); + /** Are proofs enabled? */ + bool isProofEnabled() const; + /** Are aggressive eliminations enabled? */ + bool d_isAggressive; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; + /** An eager proof generator for storing proofs in eliminate trusted above */ + std::unique_ptr<EagerProofGenerator> d_epg; }; /* class RegExpElimination */ } // namespace strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a9e2c0051..d3e9e34f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -997,27 +997,28 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + TrustNode ret; Node atomRet = atom; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership - Node atomElim = d_regexp_elim.eliminate(atomRet); - if (!atomElim.isNull()) + ret = d_regexp_elim.eliminateTrusted(atomRet); + if (!ret.isNull()) { - Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim + Trace("strings-ppr") << " rewrote " << atom << " -> " << ret.getNode() << " via regular expression elimination." << std::endl; - atomRet = atomElim; + atomRet = ret.getNode(); } } if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; StringsPreprocess* p = d_esolver.getPreprocess(); - Node ret = p->processAssertion(atomRet, new_nodes); - if (ret != atomRet) + Node pret = p->processAssertion(atomRet, new_nodes); + if (pret != atomRet) { - Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret + Trace("strings-ppr") << " rewrote " << atomRet << " -> " << pret << ", with " << new_nodes.size() << " lemmas." << std::endl; for (const Node& lem : new_nodes) @@ -1026,16 +1027,16 @@ TrustNode TheoryStrings::ppRewrite(TNode atom) ++(d_statistics.d_lemmasEagerPreproc); d_out->lemma(lem); } - atomRet = ret; + atomRet = pret; + // Don't support proofs yet, thus we must return nullptr. This is the + // case even if we had proven the elimination via regexp elimination + // above. + ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr); }else{ Assert(new_nodes.empty()); } } - if (atomRet != atom) - { - return TrustNode::mkTrustRewrite(atom, atomRet, nullptr); - } - return TrustNode::null(); + return ret; } /** run the given inference step */ diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index c5ec4d0c6..5b291f3c5 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -129,35 +129,35 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, #ifdef CVC4_USE_SYMFPU if (signedBV) { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4SignedBitVector(bv))); + symfpuLiteral::CVC4SignedBitVector(bv)))); } else { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertUBVToFloat<symfpuLiteral::traits>( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4UnsignedBitVector(bv))); + symfpuLiteral::CVC4UnsignedBitVector(bv)))); } #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl) + FloatingPointLiteral* fpl) : d_fp_size(fp_size) { - d_fpl = new FloatingPointLiteral(*fpl); + d_fpl.reset(fpl); } FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) { - d_fpl = new FloatingPointLiteral(*fp.d_fpl); + d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl)); } FloatingPoint::FloatingPoint(const FloatingPointSize& size, @@ -171,10 +171,10 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, { #ifdef CVC4_USE_SYMFPU // In keeping with the SMT-LIB standard - d_fpl = new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeZero(size, false)); + d_fpl.reset(new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, false))); #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } else @@ -285,8 +285,8 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, negative, exactExp.signExtend(extension), sig); // Then cast... - d_fpl = new FloatingPointLiteral( - symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf)); + d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat( + exactFormat, size, rm, exactFloat.d_symuf))); #else Unreachable() << "no concrete implementation of FloatingPointLiteral"; #endif @@ -295,8 +295,6 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, FloatingPoint::~FloatingPoint() { - delete d_fpl; - d_fpl = nullptr; } FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 754c38290..2d27b836e 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -20,6 +20,8 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H +#include <memory> + #include "util/bitvector.h" #include "util/floatingpoint_size.h" #include "util/rational.h" @@ -60,8 +62,6 @@ class CVC4_PUBLIC FloatingPoint /** Constructors. */ FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl); FloatingPoint(const FloatingPoint& fp); FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, @@ -118,7 +118,7 @@ class CVC4_PUBLIC FloatingPoint static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); /** Get the wrapped floating-point value. */ - const FloatingPointLiteral* getLiteral(void) const { return d_fpl; } + const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); } /** * Return a string representation of this floating-point. @@ -258,8 +258,16 @@ class CVC4_PUBLIC FloatingPoint FloatingPointSize d_fp_size; private: + /** + * Constructor. + * + * Note: This constructor takes ownership of 'fpl' and is not intended for + * public use. + */ + FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl); + /** The floating-point literal of this floating-point value. */ - FloatingPointLiteral* d_fpl; + std::unique_ptr<FloatingPointLiteral> d_fpl; }; /* class FloatingPoint */ |