Model blocker feature (#3112)

1 files changed, 48 insertions, 2 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 566777a89..316ca16d1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -402,6 +402,16 @@ class CVC4_PUBLIC SmtEngine {
    * that).
    */
   Result quickCheck();
+  /** get the model, if it is available and return a pointer to it
+   *
+   * This ensures that the model is currently available, which means that
+   * CVC4 is producing models, and is in "SAT mode", otherwise an exception
+   * is thrown.
+   *
+   * The flag c is used for giving an error message to indicate the context
+   * this method was called.
+   */
+  theory::TheoryModel* getAvailableModel(const char* c) const;
 
   /**
    * Fully type-check the argument, and also type-check that it's
@@ -480,6 +490,12 @@ class CVC4_PUBLIC SmtEngine {
    */
   std::pair<Expr, Expr> getSepHeapAndNilExpr();
 
+  /** get expanded assertions
+   *
+   * Returns the set of assertions, after expanding definitions.
+   */
+  std::vector<Expr> getExpandedAssertions();
+
  public:
 
   /**
@@ -553,12 +569,37 @@ class CVC4_PUBLIC SmtEngine {
   std::string getFilename() const;
   /**
    * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if CVC4 was built with model
-   * support and produce-models is on.
+   * or INVALID query).  Only permitted if produce-models is on.
    */
   Model* getModel();
 
   /**
+   * Block the current model. Can be called only if immediately preceded by
+   * a SAT or INVALID query. Only permitted if produce-models is on, and the
+   * block-models option is set to a mode other than "none".
+   *
+   * This adds an assertion to the assertion stack that blocks the current
+   * model based on the current options configured by CVC4.
+   *
+   * The return value has the same meaning as that of assertFormula.
+   */
+  Result blockModel();
+
+  /**
+   * Block the current model values of (at least) the values in exprs.
+   * Can be called only if immediately preceded by a SAT or INVALID query. Only
+   * permitted if produce-models is on, and the block-models option is set to a
+   * mode other than "none".
+   *
+   * This adds an assertion to the assertion stack of the form:
+   *  (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
+   * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
+   *
+   * The return value has the same meaning as that of assertFormula.
+   */
+  Result blockModelValues(const std::vector<Expr>& exprs);
+
+  /**
    * When using separation logic, obtain the expression for the heap.
    */
   Expr getSepHeapExpr();
@@ -775,6 +816,11 @@ class CVC4_PUBLIC SmtEngine {
       ;
 
   /**
+   * Same as getValue but for a vector of expressions
+   */
+  std::vector<Expr> getValues(const std::vector<Expr>& exprs);
+
+  /**
    * Add a function to the set of expressions whose value is to be
    * later returned by a call to getAssignment().  The expression
    * should be a Boolean zero-ary defined function or a Boolean