diff options
Diffstat (limited to 'src/smt')
34 files changed, 663 insertions, 380 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 20f2dcff9..095c59374 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -23,6 +23,7 @@ #include <utility> #include <vector> +#include "api/cvc4cpp.h" #include "base/check.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -134,7 +135,13 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) /* class Command */ /* -------------------------------------------------------------------------- */ -Command::Command() : d_commandStatus(NULL), d_muted(false) {} +Command::Command() : d_commandStatus(nullptr), d_muted(false) {} + +Command::Command(api::Solver* solver) + : d_solver(solver), d_commandStatus(nullptr), d_muted(false) +{ +} + Command::Command(const Command& cmd) { d_commandStatus = @@ -599,48 +606,6 @@ std::string DeclareSygusVarCommand::getCommandName() const } /* -------------------------------------------------------------------------- */ -/* class DeclareSygusPrimedVarCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand( - const std::string& id, Type t) - : DeclarationDefinitionCommand(id), d_type(t) -{ -} - -Type DeclareSygusPrimedVarCommand::getType() const { return d_type; } - -void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine) -{ - try - { - smtEngine->declareSygusPrimedVar(d_symbol, d_type); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DeclareSygusPrimedVarCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new DeclareSygusPrimedVarCommand( - d_symbol, d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareSygusPrimedVarCommand::clone() const -{ - return new DeclareSygusPrimedVarCommand(d_symbol, d_type); -} - -std::string DeclareSygusPrimedVarCommand::getCommandName() const -{ - return "declare-primed-var"; -} - -/* -------------------------------------------------------------------------- */ /* class DeclareSygusFunctionCommand */ /* -------------------------------------------------------------------------- */ @@ -1266,22 +1231,27 @@ std::string DefineTypeCommand::getCommandName() const { return "define-sort"; } DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, - Expr formula) + Expr formula, + bool global) : DeclarationDefinitionCommand(id), d_func(func), d_formals(), - d_formula(formula) + d_formula(formula), + d_global(global) { } DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) + Expr formula, + bool global) : DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), - d_formula(formula) + d_formula(formula), + d_global(global) + { } @@ -1298,7 +1268,7 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { if (!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); + smtEngine->defineFunction(d_func, d_formals, d_formula, d_global); } d_commandStatus = CommandSuccess::instance(); } @@ -1319,12 +1289,13 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, back_inserter(formals), ExportTransformer(exprManager, variableMap)); Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula); + return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global); } Command* DefineFunctionCommand::clone() const { - return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); + return new DefineFunctionCommand( + d_symbol, d_func, d_formals, d_formula, d_global); } std::string DefineFunctionCommand::getCommandName() const @@ -1340,8 +1311,9 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand( const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) - : DefineFunctionCommand(id, func, formals, formula) + Expr formula, + bool global) + : DefineFunctionCommand(id, func, formals, formula, global) { } @@ -1365,12 +1337,14 @@ Command* DefineNamedFunctionCommand::exportTo( back_inserter(formals), ExportTransformer(exprManager, variableMap)); Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); + return new DefineNamedFunctionCommand( + d_symbol, func, formals, formula, d_global); } Command* DefineNamedFunctionCommand::clone() const { - return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); + return new DefineNamedFunctionCommand( + d_symbol, d_func, d_formals, d_formula, d_global); } /* -------------------------------------------------------------------------- */ @@ -1378,7 +1352,12 @@ Command* DefineNamedFunctionCommand::clone() const /* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( - Expr func, const std::vector<Expr>& formals, Expr formula) + api::Solver* solver, + api::Term func, + const std::vector<api::Term>& formals, + api::Term formula, + bool global) + : Command(solver), d_global(global) { d_funcs.push_back(func); d_formals.push_back(formals); @@ -1386,27 +1365,31 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( } DefineFunctionRecCommand::DefineFunctionRecCommand( - const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr>>& formals, - const std::vector<Expr>& formulas) + api::Solver* solver, + const std::vector<api::Term>& funcs, + const std::vector<std::vector<api::Term>>& formals, + const std::vector<api::Term>& formulas, + bool global) + : Command(solver), + d_funcs(funcs), + d_formals(formals), + d_formulas(formulas), + d_global(global) { - d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end()); - d_formals.insert(d_formals.end(), formals.begin(), formals.end()); - d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end()); } -const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const +const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const { return d_funcs; } -const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals() - const +const std::vector<std::vector<api::Term>>& +DefineFunctionRecCommand::getFormals() const { return d_formals; } -const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const +const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const { return d_formulas; } @@ -1415,7 +1398,7 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) { try { - smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas); + d_solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -1427,35 +1410,13 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) Command* DefineFunctionRecCommand::exportTo( ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - std::vector<Expr> funcs; - for (unsigned i = 0, size = d_funcs.size(); i < size; i++) - { - Expr func = d_funcs[i].exportTo( - exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); - funcs.push_back(func); - } - std::vector<std::vector<Expr>> formals; - for (unsigned i = 0, size = d_formals.size(); i < size; i++) - { - std::vector<Expr> formals_c; - transform(d_formals[i].begin(), - d_formals[i].end(), - back_inserter(formals_c), - ExportTransformer(exprManager, variableMap)); - formals.push_back(formals_c); - } - std::vector<Expr> formulas; - for (unsigned i = 0, size = d_formulas.size(); i < size; i++) - { - Expr formula = d_formulas[i].exportTo(exprManager, variableMap); - formulas.push_back(formula); - } - return new DefineFunctionRecCommand(funcs, formals, formulas); + Unimplemented(); } Command* DefineFunctionRecCommand::clone() const { - return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas); + return new DefineFunctionRecCommand( + d_solver, d_funcs, d_formals, d_formulas, d_global); } std::string DefineFunctionRecCommand::getCommandName() const @@ -2130,6 +2091,90 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } +GetInterpolCommand::GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj) + : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) +{ +} +GetInterpolCommand::GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj, + const Type& gtype) + : Command(solver), + d_name(name), + d_conj(conj), + d_sygus_grammar_type(gtype), + d_resultStatus(false) +{ +} + +api::Term GetInterpolCommand::getConjecture() const { return d_conj; } +Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; } +api::Term GetInterpolCommand::getResult() const { return d_result; } + +void GetInterpolCommand::invoke(SmtEngine* smtEngine) +{ + try + { + if (d_sygus_grammar_type.isNull()) + { + d_resultStatus = d_solver->getInterpolant(d_conj, d_result); + } + else + { + d_resultStatus = + d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result); + } + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetInterpolCommand::printResult(std::ostream& out, + uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + expr::ExprDag::Scope scope(out, false); + if (d_resultStatus) + { + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; + } + else + { + out << "none" << std::endl; + } + } +} + +Command* GetInterpolCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) +{ + Unimplemented(); +} + +Command* GetInterpolCommand::clone() const +{ + GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj); + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetInterpolCommand::getCommandName() const +{ + return "get-interpol"; +} + GetAbductCommand::GetAbductCommand() {} GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) : d_name(name), d_conj(conj), d_resultStatus(false) diff --git a/src/smt/command.h b/src/smt/command.h index 63f1f0f33..a6a0faaae 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -28,6 +28,7 @@ #include <string> #include <vector> +#include "api/cvc4cpp.h" #include "expr/datatype.h" #include "expr/expr.h" #include "expr/type.h" @@ -39,6 +40,11 @@ namespace CVC4 { +namespace api { +class Solver; +class Term; +} // namespace api + class SmtEngine; class Command; class CommandStatus; @@ -186,27 +192,11 @@ class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus class CVC4_PUBLIC Command { - protected: - /** - * This field contains a command status if the command has been - * invoked, or NULL if it has not. This field is either a - * dynamically-allocated pointer, or it's a pointer to the singleton - * CommandSuccess instance. Doing so is somewhat asymmetric, but - * it avoids the need to dynamically allocate memory in the common - * case of a successful command. - */ - const CommandStatus* d_commandStatus; - - /** - * True if this command is "muted"---i.e., don't print "success" on - * successful execution. - */ - bool d_muted; - public: typedef CommandPrintSuccess printsuccess; Command(); + Command(api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -281,6 +271,25 @@ class CVC4_PUBLIC Command Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); } Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); } }; /* class Command::ExportTransformer */ + + /** The solver instance that this command is associated with. */ + api::Solver* d_solver; + + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + + /** + * True if this command is "muted"---i.e., don't print "success" on + * successful execution. + */ + bool d_muted; }; /* class Command */ /** @@ -436,17 +445,16 @@ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { - protected: - Expr d_func; - std::vector<Expr> d_formals; - Expr d_formula; - public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula); + DefineFunctionCommand(const std::string& id, + Expr func, + Expr formula, + bool global); DefineFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula); + Expr formula, + bool global); Expr getFunction() const; const std::vector<Expr>& getFormals() const; @@ -457,6 +465,19 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; + + protected: + /** The function we are defining */ + Expr d_func; + /** The formal arguments for the function we are defining */ + std::vector<Expr> d_formals; + /** The formula corresponding to the body of the function we are defining */ + Expr d_formula; + /** + * Stores whether this definition is global (i.e. should persist when + * popping the user context. + */ + bool d_global; }; /* class DefineFunctionCommand */ /** @@ -470,7 +491,8 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand DefineNamedFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula); + Expr formula, + bool global); void invoke(SmtEngine* smtEngine) override; Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) override; @@ -485,16 +507,20 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand class CVC4_PUBLIC DefineFunctionRecCommand : public Command { public: - DefineFunctionRecCommand(Expr func, - const std::vector<Expr>& formals, - Expr formula); - DefineFunctionRecCommand(const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr> >& formals, - const std::vector<Expr>& formula); - - const std::vector<Expr>& getFunctions() const; - const std::vector<std::vector<Expr> >& getFormals() const; - const std::vector<Expr>& getFormulas() const; + DefineFunctionRecCommand(api::Solver* solver, + api::Term func, + const std::vector<api::Term>& formals, + api::Term formula, + bool global); + DefineFunctionRecCommand(api::Solver* solver, + const std::vector<api::Term>& funcs, + const std::vector<std::vector<api::Term> >& formals, + const std::vector<api::Term>& formula, + bool global); + + const std::vector<api::Term>& getFunctions() const; + const std::vector<std::vector<api::Term> >& getFormals() const; + const std::vector<api::Term>& getFormulas() const; void invoke(SmtEngine* smtEngine) override; Command* exportTo(ExprManager* exprManager, @@ -504,11 +530,16 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command protected: /** functions we are defining */ - std::vector<Expr> d_funcs; + std::vector<api::Term> d_funcs; /** formal arguments for each of the functions we are defining */ - std::vector<std::vector<Expr> > d_formals; + std::vector<std::vector<api::Term> > d_formals; /** formulas corresponding to the bodies of the functions we are defining */ - std::vector<Expr> d_formulas; + std::vector<api::Term> d_formulas; + /** + * Stores whether this definition is global (i.e. should persist when + * popping the user context. + */ + bool d_global; }; /* class DefineFunctionRecCommand */ /** @@ -645,38 +676,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand Type d_type; }; -/** Declares a sygus primed variable, for invariant problems - * - * We do not actually build expressions for the declared variables because they - * are unnecessary for building SyGuS problems. - */ -class CVC4_PUBLIC DeclareSygusPrimedVarCommand - : public DeclarationDefinitionCommand -{ - public: - DeclareSygusPrimedVarCommand(const std::string& id, Type type); - /** returns the declared primed variable's type */ - Type getType() const; - - /** invokes this command - * - * The type of the primed variable is communicated to the SMT engine for - * debugging purposes when a synthesis conjecture is built later on. - */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - /** creates a copy of this command */ - Command* clone() const override; - /** returns this command's name */ - std::string getCommandName() const override; - - protected: - /** the type of the declared primed variable */ - Type d_type; -}; - /** Declares a sygus universal function variable */ class CVC4_PUBLIC DeclareSygusFunctionCommand : public DeclarationDefinitionCommand @@ -1040,6 +1039,58 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command SmtEngine* d_smtEngine; }; /* class GetSynthSolutionCommand */ +/** The command (get-interpol s B) + * + * This command asks for an interpolant from the current set of assertions and + * conjecture (goal) B. + * + * The symbol s is the name for the interpolation predicate. If we successfully + * find a predicate P, then the output response of this command is: (define-fun + * s () Bool P) + */ +class CVC4_PUBLIC GetInterpolCommand : public Command +{ + public: + GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj); + /** The argument gtype is the grammar of the interpolation query */ + GetInterpolCommand(api::Solver* solver, + const std::string& name, + api::Term conj, + const Type& gtype); + + /** Get the conjecture of the interpolation query */ + api::Term getConjecture() const; + /** Get the grammar sygus datatype type given for the interpolation query */ + Type getGrammarType() const; + /** Get the result of the query, which is the solution to the interpolation + * query. */ + api::Term getResult() const; + + void invoke(SmtEngine* smtEngine) override; + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + protected: + /** The name of the interpolation predicate */ + std::string d_name; + /** The conjecture of the interpolation query */ + api::Term d_conj; + /** + * The (optional) grammar of the interpolation query, expressed as a sygus + * datatype type. + */ + Type d_sygus_grammar_type; + /** the return status of the command */ + bool d_resultStatus; + /** the return expression of the command */ + api::Term d_result; +}; /* class GetInterpolCommand */ + /** The command (get-abduct s B (G)?) * * This command asks for an abduct from the current set of assertions and diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp index 43bb6b268..a88efbbec 100644 --- a/src/smt/command_list.cpp +++ b/src/smt/command_list.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/command_list.h b/src/smt/command_list.h index 0b1aaecf2..cdc8e4c22 100644 --- a/src/smt/command_list.h +++ b/src/smt/command_list.h @@ -2,9 +2,9 @@ /*! \file command_list.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h index b141ef9cb..afac2df58 100644 --- a/src/smt/defined_function.h +++ b/src/smt/defined_function.h @@ -2,7 +2,7 @@ /*! \file defined_function.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, 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. diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 823e1900d..d8d486e12 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -2,9 +2,9 @@ /*! \file dump.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Tim King + ** Andres Noetzli, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/dump.h b/src/smt/dump.h index fc2452423..050935422 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index e5da2a6e8..109d49c06 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -2,9 +2,9 @@ /*! \file logic_exception.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp index c24378cb1..486ac829d 100644 --- a/src/smt/logic_request.cpp +++ b/src/smt/logic_request.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner, Martin Brain, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h index 432d5469c..b1822d0a1 100644 --- a/src/smt/logic_request.h +++ b/src/smt/logic_request.h @@ -2,9 +2,9 @@ /*! \file logic_request.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Tim King, Mathias Preiner + ** Martin Brain, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 7615325b7..12f98aa95 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index bc12bbe39..577ef3226 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model.cpp b/src/smt/model.cpp index c6048da15..6f6a09f38 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -2,9 +2,9 @@ /*! \file model.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model.h b/src/smt/model.h index 3ff63e915..1f7c5daae 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -2,9 +2,9 @@ /*! \file model.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 6e73a61b3..7a34cd928 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -2,9 +2,9 @@ /*! \file model_blocker.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 7fc4788bb..ef4c6e700 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -2,9 +2,9 @@ /*! \file model_blocker.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 3007821e5..08f0b29c3 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -2,9 +2,9 @@ /*! \file model_core_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Mathias Preiner, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 2390d61ca..2897ce728 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -2,9 +2,9 @@ /*! \file model_core_builder.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 0e2701a1a..44944d0c2 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -2,9 +2,9 @@ /*! \file process_assertions.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index ddf5a6cba..4850d5589 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -2,9 +2,9 @@ /*! \file process_assertions.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e06363883..a7e8e6212 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -2,9 +2,9 @@ /*! \file set_defaults.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -266,12 +266,35 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) << std::endl; } } + // !!!!!!!!!!!!!!!! temporary, to support CI check for old proof system + if (options::proof()) + { + options::proofNew.set(false); + } + + if (options::arraysExp()) + { + if (!logic.isQuantified()) + { + logic = logic.getUnlockedCopy(); + logic.enableQuantifiers(); + logic.lock(); + } + // Allows to answer sat more often by default. + if (!options::fmfBound.wasSetByUser()) + { + options::fmfBound.set(true); + Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; + } + } // sygus inference may require datatypes if (!smte.isInternalSubsolver()) { - if (options::produceAbducts() || options::sygusInference() - || options::sygusRewSynthInput() || options::sygusInst()) + if (options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE + || options::sygusInference() || options::sygusRewSynthInput() + || options::sygusInst()) { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; @@ -295,6 +318,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) if ((options::checkModels() || options::checkSynthSol() || options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE || options::modelCoresMode() != options::ModelCoresMode::NONE || options::blockModelsMode() != options::BlockModelsMode::NONE) && !options::produceAssertions()) @@ -357,6 +381,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } } + + if (options::solveBVAsInt() > 0) + { + /** + * Operations on 1 bits are better handled as Boolean operations + * than as integer operations. + * Therefore, we enable bv-to-bool, which runs before + * the translation to integers. + */ + options::bitvectorToBool.set(true); + } + // Disable options incompatible with unsat cores and proofs or output an // error if enabled explicitly if (options::unsatCores() || options::proof()) @@ -413,16 +449,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) options::preSkolemQuant.set(false); } - if (options::solveBVAsInt() > 0) - { - /** - * Operations on 1 bits are better handled as Boolean operations - * than as integer operations. - * Therefore, we enable bv-to-bool, which runs before - * the translation to integers. - */ - options::bitvectorToBool.set(true); - } if (options::bitvectorToBool()) { @@ -538,18 +564,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) smte.setOption("produce-models", SExpr("true")); } - // Set the options for the theoryOf - if (!options::theoryOfMode.wasSetByUser()) - { - if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) - && !logic.isTheoryEnabled(THEORY_STRINGS) - && !logic.isTheoryEnabled(THEORY_SETS)) - { - Trace("smt") << "setting theoryof-mode to term-based" << std::endl; - options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); - } - } - ///////////////////////////////////////////////////////////////////////////// // Theory widening // @@ -609,6 +623,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } ///////////////////////////////////////////////////////////////////////////// + // Set the options for the theoryOf + if (!options::theoryOfMode.wasSetByUser()) + { + if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) + && !logic.isTheoryEnabled(THEORY_STRINGS) + && !logic.isTheoryEnabled(THEORY_SETS)) + { + Trace("smt") << "setting theoryof-mode to term-based" << std::endl; + options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); + } + } + // by default, symmetry breaker is on only for non-incremental QF_UF if (!options::ufSymmetryBreaker.wasSetByUser()) { @@ -875,6 +901,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } if (options::ufHo()) { + // if higher-order, disable proof production + if (options::proofNew()) + { + if (options::proofNew.wasSetByUser()) + { + Warning() << "SmtEngine: turning off proof production (not yet " + "supported with --uf-ho)\n"; + } + options::proofNew.set(false); + } // if higher-order, then current variants of model-based instantiation // cannot be used if (options::mbqiMode() != options::MbqiMode::NONE) @@ -1106,6 +1142,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::cegqiPreRegInst.set(true); } + // not compatible with proofs + if (options::proofNew()) + { + if (options::proofNew.wasSetByUser()) + { + Notice() << "SmtEngine: setting proof-new to false to support SyGuS" + << std::endl; + } + options::proofNew.set(false); + } } // counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors @@ -1161,11 +1207,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) // prenexing if (options::cegqiNestedQE()) { - // only complete with prenex = disj_normal or normal - if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL) - { - options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL); - } + // only complete with prenex = normal + options::prenexQuant.set(options::PrenexQuantMode::NORMAL); } else if (options::globalNegate()) { @@ -1402,12 +1445,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) disableModels = true; sOptNoModel = "minisat-elimination"; } - else if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && !options::nlExt()) - { - disableModels = true; - sOptNoModel = "nonlinear arithmetic without nl-ext"; - } else if (options::globalNegate()) { disableModels = true; @@ -1465,6 +1502,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) "division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); } + // !!!!!!!!!!!!!!!! temporary, until proof-new is functional + if (options::proofNew()) + { + throw OptionException("--proof-new is not yet supported."); + } } } // namespace smt diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 8871b0b38..f3ec21c9b 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c0a2cd8f..bb4d82fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2,9 +2,9 @@ /*! \file smt_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -29,6 +29,7 @@ #include <utility> #include <vector> +#include "api/cvc4cpp.h" #include "base/check.h" #include "base/configuration.h" #include "base/configuration_private.h" @@ -759,6 +760,7 @@ void SmtEngine::finishInit() // In the case of incremental solving, we appear to need these to // ensure the relevant Nodes remain live. d_assertionList = new (true) AssertionList(getUserContext()); + d_globalDefineFunRecLemmas.reset(new std::vector<Node>()); } // dump out a set-logic command only when raw-benchmark is disabled to avoid @@ -847,6 +849,8 @@ SmtEngine::~SmtEngine() d_assignments->deleteSelf(); } + d_globalDefineFunRecLemmas.reset(); + if(d_assertionList != NULL) { d_assertionList->deleteSelf(); } @@ -903,6 +907,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) "finished initializing."); } d_logic = logic; + d_userLogic = logic; setLogicInternal(); } @@ -929,6 +934,14 @@ void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { return d_logic; } +LogicInfo SmtEngine::getUserLogicInfo() const +{ + // Lock the logic to make sure that this logic can be queried. We create a + // copy of the user logic here to keep this method const. + LogicInfo res = d_userLogic; + res.lock(); + return res; +} void SmtEngine::setFilename(std::string filename) { d_filename = filename; } std::string SmtEngine::getFilename() const { return d_filename; } void SmtEngine::setLogicInternal() @@ -937,6 +950,7 @@ void SmtEngine::setLogicInternal() << "setting logic in SmtEngine but the engine has already" " finished initializing for this run"; d_logic.lock(); + d_userLogic.lock(); } void SmtEngine::setProblemExtended() @@ -1022,72 +1036,110 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) throw UnrecognizedOptionException(); } -CVC4::SExpr SmtEngine::getInfo(const std::string& key) const { +bool SmtEngine::isValidGetInfoFlag(const std::string& key) const +{ + if (key == "all-statistics" || key == "error-behavior" || key == "name" + || key == "version" || key == "authors" || key == "status" + || key == "reason-unknown" || key == "assertion-stack-levels" + || key == "all-options") + { + return true; + } + return false; +} +CVC4::SExpr SmtEngine::getInfo(const std::string& key) const +{ SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if(key == "all-statistics") { + if (!isValidGetInfoFlag(key)) + { + throw UnrecognizedOptionException(); + } + if (key == "all-statistics") + { vector<SExpr> stats; - for(StatisticsRegistry::const_iterator i = NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->begin(); - i != NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->end(); - ++i) { + for (StatisticsRegistry::const_iterator i = + NodeManager::fromExprManager(d_exprManager) + ->getStatisticsRegistry() + ->begin(); + i + != NodeManager::fromExprManager(d_exprManager) + ->getStatisticsRegistry() + ->end(); + ++i) + { vector<SExpr> v; v.push_back((*i).first); v.push_back((*i).second); stats.push_back(v); } - for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin(); - i != d_statisticsRegistry->end(); - ++i) { + for (StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin(); + i != d_statisticsRegistry->end(); + ++i) + { vector<SExpr> v; v.push_back((*i).first); v.push_back((*i).second); stats.push_back(v); } return SExpr(stats); - } else if(key == "error-behavior") { + } + if (key == "error-behavior") + { return SExpr(SExpr::Keyword("immediate-exit")); - } else if(key == "name") { + } + if (key == "name") + { return SExpr(Configuration::getName()); - } else if(key == "version") { + } + if (key == "version") + { return SExpr(Configuration::getVersionString()); - } else if(key == "authors") { + } + if (key == "authors") + { return SExpr(Configuration::about()); - } else if(key == "status") { + } + if (key == "status") + { // sat | unsat | unknown - switch(d_status.asSatisfiabilityResult().isSat()) { - case Result::SAT: - return SExpr(SExpr::Keyword("sat")); - case Result::UNSAT: - return SExpr(SExpr::Keyword("unsat")); - default: - return SExpr(SExpr::Keyword("unknown")); - } - } else if(key == "reason-unknown") { - if(!d_status.isNull() && d_status.isUnknown()) { + switch (d_status.asSatisfiabilityResult().isSat()) + { + case Result::SAT: return SExpr(SExpr::Keyword("sat")); + case Result::UNSAT: return SExpr(SExpr::Keyword("unsat")); + default: return SExpr(SExpr::Keyword("unknown")); + } + } + if (key == "reason-unknown") + { + if (!d_status.isNull() && d_status.isUnknown()) + { stringstream ss; ss << d_status.whyUnknown(); string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); return SExpr(SExpr::Keyword(s)); - } else { + } + else + { throw RecoverableModalException( "Can't get-info :reason-unknown when the " "last result wasn't unknown!"); } - } else if(key == "assertion-stack-levels") { + } + if (key == "assertion-stack-levels") + { AlwaysAssert(d_userLevels.size() <= std::numeric_limits<unsigned long int>::max()); return SExpr(static_cast<unsigned long int>(d_userLevels.size())); - } else if(key == "all-options") { - // get the options, like all-statistics - std::vector< std::vector<std::string> > current_options = - Options::current()->getOptions(); - return SExpr::parseListOfListOfAtoms(current_options); - } else { - throw UnrecognizedOptionException(); } + Assert(key == "all-options"); + // get the options, like all-statistics + std::vector<std::vector<std::string>> current_options = + Options::current()->getOptions(); + return SExpr::parseListOfListOfAtoms(current_options); } void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func) @@ -1141,7 +1193,8 @@ void SmtEngine::debugCheckFunctionBody(Expr formula, void SmtEngine::defineFunction(Expr func, const std::vector<Expr>& formals, - Expr formula) + Expr formula, + bool global) { SmtScope smts(this); finalOptionsAreSet(); @@ -1153,7 +1206,7 @@ void SmtEngine::defineFunction(Expr func, ss << language::SetLanguage( language::SetLanguage::getLanguage(Dump.getStream())) << func; - DefineFunctionCommand c(ss.str(), func, formals, formula); + DefineFunctionCommand c(ss.str(), func, formals, formula, global); addToModelCommandAndDump( c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); @@ -1182,13 +1235,22 @@ void SmtEngine::defineFunction(Expr func, // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks // d_haveAdditions = true; Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl; - d_definedFunctions->insert(funcNode, def); + + if (global) + { + d_definedFunctions->insertAtContextLevelZero(funcNode, def); + } + else + { + d_definedFunctions->insert(funcNode, def); + } } void SmtEngine::defineFunctionsRec( const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr> >& formals, - const std::vector<Expr>& formulas) + const std::vector<std::vector<Expr>>& formals, + const std::vector<Expr>& formulas, + bool global) { SmtScope smts(this); finalOptionsAreSet(); @@ -1216,7 +1278,16 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") << DefineFunctionRecCommand(funcs, formals, formulas); + std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs); + std::vector<std::vector<api::Term>> tFormals; + for (const std::vector<Expr>& formal : formals) + { + tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal)); + } + std::vector<api::Term> tFormulas = + api::exprVectorToTerms(d_solver, formulas); + Dump("raw-benchmark") << DefineFunctionRecCommand( + d_solver, tFuncs, tFormals, tFormulas, global); } ExprManager* em = getExprManager(); @@ -1256,17 +1327,28 @@ void SmtEngine::defineFunctionsRec( // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr(); - if (d_assertionList != NULL) + if (d_assertionList != nullptr) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode(), false, true, false, maybeHasFv); + if (global && d_globalDefineFunRecLemmas != nullptr) + { + // Global definitions are asserted at check-sat-time because we have to + // make sure that they are always present + Assert(!language::isInputLangSygus(options::inputLanguage())); + d_globalDefineFunRecLemmas->emplace_back(Node::fromExpr(e)); + } + else + { + d_private->addFormula(e.getNode(), false, true, false, maybeHasFv); + } } } void SmtEngine::defineFunctionRec(Expr func, const std::vector<Expr>& formals, - Expr formula) + Expr formula, + bool global) { std::vector<Expr> funcs; funcs.push_back(func); @@ -1274,7 +1356,7 @@ void SmtEngine::defineFunctionRec(Expr func, formals_multi.push_back(formals); std::vector<Expr> formulas; formulas.push_back(formula); - defineFunctionsRec(funcs, formals_multi, formulas); + defineFunctionsRec(funcs, formals_multi, formulas, global); } bool SmtEngine::isDefinedFunction( Expr func ){ @@ -1614,6 +1696,17 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, d_private->addFormula(e.getNode(), inUnsatCore, true, true); } + if (d_globalDefineFunRecLemmas != nullptr) + { + // Global definitions are asserted at check-sat-time because we have to + // make sure that they are always present (they are essentially level + // zero assertions) + for (const Node& lemma : *d_globalDefineFunRecLemmas) + { + d_private->addFormula(lemma, false, true, false, false); + } + } + r = check(); if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) @@ -1780,15 +1873,6 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) // don't need to set that the conjecture is stale } -void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) -{ - SmtScope smts(this); - finalOptionsAreSet(); - // do nothing (the command is spurious) - Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; - // don't need to set that the conjecture is stale -} - void SmtEngine::declareSygusFunctionVar(const std::string& id, Expr var, Type type) @@ -2850,6 +2934,12 @@ void SmtEngine::checkSynthSolution() } } +void SmtEngine::checkInterpol(Expr interpol, + const std::vector<Expr>& easserts, + const Node& conj) +{ +} + void SmtEngine::checkAbduct(Expr a) { Assert(a.getType().isBoolean()); @@ -3068,6 +3158,19 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +bool SmtEngine::getInterpol(const Expr& conj, + const Type& grammarType, + Expr& interpol) +{ + return false; +} + +bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol) +{ + Type grammarType; + return getInterpol(conj, grammarType, interpol); +} + bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 672bec821..afb39b41b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -2,9 +2,9 @@ /*! \file smt_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Haniel Barbosa + ** Morgan Deters, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -65,6 +65,12 @@ class StatisticsRegistry; /* -------------------------------------------------------------------------- */ +namespace api { +class Solver; +} // namespace api + +/* -------------------------------------------------------------------------- */ + namespace context { class Context; class UserContext; @@ -126,6 +132,7 @@ namespace theory { class CVC4_PUBLIC SmtEngine { + friend class ::CVC4::api::Solver; // TODO (Issue #1096): Remove this friend relationship. friend class ::CVC4::preprocessing::PreprocessingPassContext; friend class ::CVC4::smt::SmtEnginePrivate; @@ -141,6 +148,29 @@ class CVC4_PUBLIC SmtEngine public: /* ....................................................................... */ + /** + * The current mode of the solver, which is an extension of Figure 4.1 on + * page 52 of the SMT-LIB version 2.6 standard + * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf + */ + enum SmtMode + { + // the initial state of the solver + SMT_MODE_START, + // normal state of the solver, after assert/push/pop/declare/define + SMT_MODE_ASSERT, + // immediately after a check-sat returning "sat" + SMT_MODE_SAT, + // immediately after a check-sat returning "unknown" + SMT_MODE_SAT_UNKNOWN, + // immediately after a check-sat returning "unsat" + SMT_MODE_UNSAT, + // immediately after a successful call to get-abduct + SMT_MODE_ABDUCT, + // immediately after a successful call to get-interpol + SMT_MODE_INTERPOL + }; + /** Construct an SmtEngine with the given expression manager. */ SmtEngine(ExprManager* em); /** Destruct the SMT engine. */ @@ -162,6 +192,9 @@ class CVC4_PUBLIC SmtEngine /** Return the user context level. */ size_t getNumUserLevels() { return d_userLevels.size(); } + /** Return the current mode of the solver. */ + SmtMode getSmtMode() { return d_smtMode; } + /** * Set the logic of the script. * @throw ModalException, LogicException @@ -183,12 +216,18 @@ class CVC4_PUBLIC SmtEngine /** Get the logic information currently set. */ LogicInfo getLogicInfo() const; + /** Get the logic information set by the user. */ + LogicInfo getUserLogicInfo() const; + /** * Set information about the script executing. * @throw OptionException, ModalException */ void setInfo(const std::string& key, const CVC4::SExpr& value); + /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */ + bool isValidGetInfoFlag(const std::string& key) const; + /** Query information about the SMT environment. */ CVC4::SExpr getInfo(const std::string& key) const; @@ -263,15 +302,18 @@ class CVC4_PUBLIC SmtEngine * (lambda (formals) formula) * This adds func to the list of defined functions, which indicates that * all occurrences of func should be expanded during expandDefinitions. - * This method expects input such that: - * - func : a variable of function type that expects the arguments in - * formals, - * - formals : a list of BOUND_VARIABLE expressions, - * - formula does not contain func. + * + * @param func a variable of function type that expects the arguments in + * formal + * @param formals a list of BOUND_VARIABLE expressions + * @param formula The body of the function, must not contain func + * @param global True if this definition is global (i.e. should persist when + * popping the user context) */ void defineFunction(Expr func, const std::vector<Expr>& formals, - Expr formula); + Expr formula, + bool global = false); /** Return true if given expression is a defined function. */ bool isDefinedFunction(Expr func); @@ -290,17 +332,22 @@ class CVC4_PUBLIC SmtEngine * - func[i] : a variable of function type that expects the arguments in * formals[i], and * - formals[i] : a list of BOUND_VARIABLE expressions. + * + * @param global True if this definition is global (i.e. should persist when + * popping the user context) */ void defineFunctionsRec(const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr> >& formals, - const std::vector<Expr>& formulas); + const std::vector<std::vector<Expr>>& formals, + const std::vector<Expr>& formulas, + bool global = false); /** * Define function recursive * Same as above, but for a single function. */ void defineFunctionRec(Expr func, const std::vector<Expr>& formals, - Expr formula); + Expr formula, + bool global = false); /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for @@ -359,16 +406,6 @@ class CVC4_PUBLIC SmtEngine void declareSygusVar(const std::string& id, Expr var, Type type); /** - * Store information for debugging sygus invariants setup. - * - * Since in SyGuS the commands "declare-primed-var" are not necessary for - * building invariant constraints, we only use them to check that the number - * of variables declared corresponds to the number of arguments of the - * invariant-to-synthesize. - */ - void declareSygusPrimedVar(const std::string& id, Type type); - - /** * Add a function variable declaration. * * Is SyGuS semantics declared functions are treated in the same manner as @@ -584,6 +621,23 @@ class CVC4_PUBLIC SmtEngine Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true); /** + * This method asks this SMT engine to find an interpolant with respect to + * the current assertion stack (call it A) and the conjecture (call it B). If + * this method returns true, then interpolant is set to a formula I such that + * A ^ ~I and I ^ ~B are both unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shapes of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol); + + /** Same as above, but without user-provided grammar restrictions */ + bool getInterpol(const Expr& conj, Expr& interpol); + + /** * This method asks this SMT engine to find an abduct with respect to the * current assertion stack (call it A) and the conjecture (call it B). * If this method returns true, then abd is set to a formula C such that @@ -835,34 +889,14 @@ class CVC4_PUBLIC SmtEngine typedef context::CDList<Expr> AssertionList; /** The type of our internal assignment set */ typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; - /** The types for the recursive function definitions */ - typedef context::CDList<Node> NodeList; - - /** - * The current mode of the solver, which is an extension of Figure 4.1 on - * page 52 of the SMT-LIB version 2.6 standard - * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf - */ - enum SmtMode - { - // the initial state of the solver - SMT_MODE_START, - // normal state of the solver, after assert/push/pop/declare/define - SMT_MODE_ASSERT, - // immediately after a check-sat returning "sat" - SMT_MODE_SAT, - // immediately after a check-sat returning "unknown" - SMT_MODE_SAT_UNKNOWN, - // immediately after a check-sat returning "unsat" - SMT_MODE_UNSAT, - // immediately after a successful call to get-abduct - SMT_MODE_ABDUCT - }; // disallow copy/assignment SmtEngine(const SmtEngine&) = delete; SmtEngine& operator=(const SmtEngine&) = delete; + /** Set solver instance that owns this SmtEngine. */ + void setSolver(api::Solver* solver) { d_solver = solver; } + /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); } @@ -920,6 +954,18 @@ class CVC4_PUBLIC SmtEngine * unsatisfiable. If not, then the found solutions are wrong. */ void checkSynthSolution(); + + /** + * Check that a solution to an interpolation problem is indeed a solution. + * + * The check is made by determining that the assertions imply the solution of + * the interpolation problem (interpol), and the solution implies the goal + * (conj). If these criteria are not met, an internal error is thrown. + */ + void checkInterpol(Expr interpol, + const std::vector<Expr>& easserts, + const Node& conj); + /** * Check that a solution to an abduction conjecture is indeed a solution. * @@ -1043,6 +1089,7 @@ class CVC4_PUBLIC SmtEngine void debugCheckFunctionBody(Expr formula, const std::vector<Expr>& formals, Expr func); + /** * Get abduct internal. * @@ -1070,6 +1117,9 @@ class CVC4_PUBLIC SmtEngine /* Members -------------------------------------------------------------- */ + /** Solver instance that owns this SmtEngine instance. */ + api::Solver* d_solver = nullptr; + /** Expr manager context */ std::unique_ptr<context::Context> d_context; /** User level context */ @@ -1133,11 +1183,17 @@ class CVC4_PUBLIC SmtEngine /** * The assertion list (before any conversion) for supporting - * getAssertions(). Only maintained if in interactive mode. + * getAssertions(). Only maintained if in incremental mode. */ AssertionList* d_assertionList; /** + * List of lemmas generated for global recursive function definitions. We + * assert this list of definitions in each check-sat call. + */ + std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas; + + /** * The list of assumptions from the previous call to checkSatisfiability. * Note that if the last call to checkSatisfiability was an entailment check, * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains @@ -1179,10 +1235,14 @@ class CVC4_PUBLIC SmtEngine std::vector<Command*> d_defineCommands; /** - * The logic we're in. + * The logic we're in. This logic may be an extension of the logic set by the + * user. */ LogicInfo d_logic; + /** The logic set by the user. */ + LogicInfo d_userLogic; + /** * Keep a copy of the original option settings (for reset()). */ diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index 635e593bb..95a5f4f3b 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -3,51 +3,33 @@ %} #ifdef SWIGJAVA + %typemap(javacode) CVC4::SmtEngine %{ // a ref is kept here to keep Java GC from collecting the EM // before the SmtEngine - private Object emRef; - static final native Object mkRef(Object obj); - static final native void dlRef(Object obj); + private ExprManager em; %} -%native (mkRef) jobject SmtEngine::mkRef(jobject); -%native (dlRef) void SmtEngine::dlRef(jobject); -%{ -extern "C" { -SWIGEXPORT jobject JNICALL Java_edu_stanford_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) { - if(o == NULL) { - return NULL; - } - return jenv->NewGlobalRef(o); + +%typemap(javaconstruct) SmtEngine { + this($imcall, true); + this.em = em; // keep ref to expr manager in SWIG proxy class } -SWIGEXPORT void JNICALL Java_edu_stanford_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) { - if(o != NULL) { - jenv->DeleteGlobalRef(o); - } + +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); } + +%typemap(javaout) CVC4::UnsatCore { + return new UnsatCore(this.em, $jnicall, true); } -%} -%typemap(javaconstruct) SmtEngine { - this($imcall, true); - emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class - } -%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine { - dlRef(emRef); - emRef = null; - if (swigCPtr != 0) { - if (swigCMemOwn) { - swigCMemOwn = false; - CVC4JNI.delete_SmtEngine(swigCPtr); - } - swigCPtr = 0; - } - } - -%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>; + +// %template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>; +%ignore CVC4::SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map); #endif // SWIGJAVA %ignore CVC4::SmtEngine::setLogic(const char*); +%ignore CVC4::SmtEngine::setReplayStream(ExprStream* exprStream); %ignore CVC4::smt::currentProofManager(); %include "smt/smt_engine.h" diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 55af4bfd2..7c438073a 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -2,9 +2,9 @@ /*! \file smt_engine_scope.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Tim King + ** Andres Noetzli, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index d72d58caa..012c2ec31 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index c45f77b9b..964237499 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -2,7 +2,7 @@ /*! \file smt_engine_stats.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Tim King, Andres Noetzli, 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. diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index cebf85d95..3ea46eaa4 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -2,7 +2,7 @@ /*! \file smt_engine_stats.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Liana Hadarean ** 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. diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index 1912b0eb2..7191da012 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 1a0993d1d..c54e881f5 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -2,9 +2,9 @@ /*! \file smt_statistics_registry.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 1ae125e03..89091d309 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -2,9 +2,9 @@ /*! \file term_formula_removal.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -89,8 +89,8 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, if (node.getKind() == kind::ITE && !nodeType.isBoolean()) { // Here, we eliminate the ITE if we are not Boolean and if we do not contain - // a bound variable. - if (!inQuant || !expr::hasBoundVar(node)) + // a free variable. + if (!inQuant || !expr::hasFreeVar(node)) { skolem = getSkolemForNode(node); if (skolem.isNull()) @@ -111,7 +111,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, else if (node.getKind() == kind::LAMBDA) { // if a lambda, do lambda-lifting - if (!inQuant) + if (!inQuant || !expr::hasFreeVar(node)) { skolem = getSkolemForNode(node); if (skolem.isNull()) @@ -143,7 +143,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, // If a witness choice // For details on this operator, see // http://planetmath.org/hilbertsvarepsilonoperator. - if (!inQuant) + if (!inQuant || !expr::hasFreeVar(node)) { skolem = getSkolemForNode(node); if (skolem.isNull()) diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 3b72b46a5..9ec12cb12 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index 53d5e5ce0..51fbc66e1 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 |