Allow FORALL in quantifier elimination command (#1322)

* Allow FORALL passed as an argument to get-qe.

* Document

* Format

* Minor

2 files changed, 58 insertions, 8 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2ff115606..1634345e0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5300,8 +5300,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull,
   }
   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
   Node n_e = Node::fromExpr( e );
-  if( n_e.getKind()!=kind::EXISTS ){
-    throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
+  if (n_e.getKind() != kind::EXISTS && n_e.getKind() != kind::FORALL)
+  {
+    throw ModalException(
+        "Expecting a quantified formula as argument to get-qe.");
   }
   //tag the quantified formula with the quant-elim attribute
   TypeNode t = NodeManager::currentNM()->booleanType();
@@ -5312,7 +5314,8 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull,
   n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
   std::vector< Node > e_children;
   e_children.push_back( n_e[0] );
-  e_children.push_back( n_e[1] );
+  e_children.push_back(n_e.getKind() == kind::EXISTS ? n_e[1]
+                                                     : n_e[1].negate());
   e_children.push_back( n_attr );
   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
   Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
@@ -5336,13 +5339,18 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull,
       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
       ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
       Trace("smt-qe") << "Returned : " << ret_n << std::endl;
-      ret_n = Rewriter::rewrite( ret_n.negate() );
+      if (n_e.getKind() == kind::EXISTS)
+      {
+        ret_n = Rewriter::rewrite(ret_n.negate());
+      }
     }else{
-      ret_n = NodeManager::currentNM()->mkConst(false);
+      ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS);
     }
     return ret_n.toExpr();
   }else {
-    return NodeManager::currentNM()->mkConst(true).toExpr();
+    return NodeManager::currentNM()
+        ->mkConst(n_e.getKind() == kind::EXISTS)
+        .toExpr();
   }
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 48ae24898..8961fbee0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -538,8 +538,50 @@ public:
   void printSynthSolution( std::ostream& out );
 
   /**
-   * Do quantifier elimination, doFull false means just output one disjunct,
-   * strict is whether to output warnings.
+   * Do quantifier elimination.
+   *
+   * This function takes as input a quantified formula e
+   * of the form:
+   *   Q x1...xn. P( x1...xn, y1...yn )
+   * where P( x1...xn, y1...yn ) is a quantifier-free
+   * formula in a logic that supports quantifier elimination.
+   * Currently, the only logics supported by quantifier
+   * elimination is LRA and LIA.
+   *
+   * This function returns a formula ret such that, given
+   * the current set of formulas A asserted to this SmtEngine :
+   *
+   * If doFull = true, then
+   *   - ( A ^ e ) and ( A ^ ret ) are equivalent
+   *   - ret is quantifier-free formula containing
+   *     only free variables in y1...yn.
+   *
+   * If doFull = false, then
+   *   - (A ^ e) => (A ^ ret) if Q is forall or
+   *     (A ^ ret) => (A ^ e) if Q is exists,
+   *   - ret is quantifier-free formula containing
+   *     only free variables in y1...yn,
+   *   - If Q is exists, let A^Q_n be the formula
+   *       A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
+   *     where for each i=1,...n, formula ret^Q_i
+   *     is the result of calling doQuantifierElimination
+   *     for e with the set of assertions A^Q_{i-1}.
+   *     Similarly, if Q is forall, then let A^Q_n be
+   *       A ^ ret^Q_1 ^ ... ^ ret^Q_n
+   *     where ret^Q_i is the same as above.
+   *     In either case, we have that ret^Q_j will
+   *     eventually be true or false, for some finite j.
+   *
+   * The former feature is quantifier elimination, and
+   * is run on invocations of the smt2 extended command get-qe.
+   * The latter feature is referred to as partial quantifier
+   * elimination, and is run on invocations of the smt2
+   * extended command get-qe-disjunct, which can be used
+   * for incrementally computing the result of a
+   * quantifier elimination.
+   * 
+   * The argument strict is whether to output
+   * warnings, such as when an unexpected logic is used.
    */
   Expr doQuantifierElimination(const Expr& e, bool doFull,
                                bool strict = true) throw(Exception);