diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e768bf826..bba6b1cef 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -186,8 +186,8 @@ class CVC4_PUBLIC SmtEngine { std::vector<Command*> d_dumpCommands; /** - *A vector of command definitions to be imported in the new - *SmtEngine when checking unsat-cores. + * A vector of command definitions to be imported in the new + * SmtEngine when checking unsat-cores. */ std::vector<Command*> d_defineCommands; @@ -207,10 +207,10 @@ class CVC4_PUBLIC SmtEngine { unsigned d_pendingPops; /** - * Whether or not this SmtEngine has been fully initialized (that is, - * the ). This post-construction initialization is automatically - * triggered by the use of the SmtEngine; e.g. when setLogic() is - * called, or the first assertion is made, etc. + * Whether or not this SmtEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SmtEngine; e.g. when setLogic() is called, or the first + * assertion is made, etc. */ bool d_fullyInited; @@ -400,7 +400,12 @@ class CVC4_PUBLIC SmtEngine { SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED; //check satisfiability (for query and check-sat) - Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery); + Result checkSatisfiability(const Expr& expr, + bool inUnsatCore, + bool isQuery); + Result checkSatisfiability(const std::vector<Expr>& exprs, + bool inUnsatCore, + bool isQuery); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is @@ -535,7 +540,10 @@ class CVC4_PUBLIC SmtEngine { * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const Expr& e, bool inUnsatCore = true) /* throw(Exception) */; + Result query(const Expr& e = Expr(), + bool inUnsatCore = true) /* throw(Exception) */; + Result query(const std::vector<Expr>& exprs, + bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a formula (if provided) to the current context and call @@ -543,6 +551,8 @@ class CVC4_PUBLIC SmtEngine { */ Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) /* throw(Exception) */; + Result checkSat(const std::vector<Expr>& exprs, + bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a synthesis conjecture to the current context and call @@ -598,7 +608,7 @@ class CVC4_PUBLIC SmtEngine { * INVALID query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ - CVC4::SExpr getAssignment(); + std::vector<std::pair<Expr, Expr> > getAssignment(); /** * Get the last proof (only if immediately preceded by an UNSAT @@ -871,13 +881,13 @@ class CVC4_PUBLIC SmtEngine { * translation. */ void setReplayStream(ExprStream* exprStream); - + /** get expression name * Returns true if e has an expression name in the current context. * If it returns true, the name of e is stored in name. */ bool getExpressionName(Expr e, std::string& name) const; - + /** set expression name * Sets the expression name of e to name. * This information is user-context-dependent. |