Merge branch 'master' into rmAliasesrmAliases

5 files changed, 135 insertions, 86 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f563e83f5..2e6e70d6b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -277,6 +277,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
     {REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
     {REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
+    {REGEXP_REPEAT, CVC4::Kind::REGEXP_REPEAT},
     {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
     {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
     {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
@@ -544,6 +545,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
         {CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
         {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
+        {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT},
         {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
         {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
         {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
@@ -766,22 +768,22 @@ bool Result::isSatUnknown(void) const
          && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
 }
 
-bool Result::isValid(void) const
+bool Result::isEntailed(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::VALID;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::ENTAILED;
 }
 
-bool Result::isInvalid(void) const
+bool Result::isNotEntailed(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::INVALID;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED;
 }
 
-bool Result::isValidUnknown(void) const
+bool Result::isEntailmentUnknown(void) const
 {
-  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
-         && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
+  return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
+         && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN;
 }
 
 bool Result::operator==(const Result& r) const
@@ -2292,7 +2294,7 @@ Term Solver::mkValHelper(T t) const
   return res;
 }
 
-Term Solver::mkRealFromStrHelper(std::string s) const
+Term Solver::mkRealFromStrHelper(const std::string& s) const
 {
   /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
    * throws an std::invalid_argument exception. For consistency, we treat it
@@ -2316,7 +2318,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
+Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
   CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
@@ -2326,7 +2328,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
 }
 
 Term Solver::mkBVFromStrHelper(uint32_t size,
-                               std::string s,
+                               const std::string& s,
                                uint32_t base) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
@@ -2351,6 +2353,20 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
   return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
 }
 
+Term Solver::mkCharFromStrHelper(const std::string& s) const
+{
+  CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
+                     == std::string::npos
+                 && s.size() <= 5 && s.size() > 0)
+      << "Unexpected string for hexidecimal character " << s;
+  uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
+  CVC4_API_CHECK(val < String::num_codes())
+      << "Not a valid code point for hexidecimal character " << s;
+  std::vector<unsigned> cpts;
+  cpts.push_back(val);
+  return mkValHelper<CVC4::String>(CVC4::String(cpts));
+}
+
 Term Solver::mkTermFromKind(Kind kind) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
@@ -2949,6 +2965,21 @@ Term Solver::mkString(const std::vector<unsigned>& s) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkChar(const std::string& s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  return mkCharFromStrHelper(s);
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkChar(const char* s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_NOT_NULLPTR(s);
+  return mkCharFromStrHelper(std::string(s));
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkUniverseSet(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
@@ -3490,6 +3521,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
           kind,
           *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
       break;
+    case REGEXP_REPEAT:
+      res = Op(kind,
+               *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
+                    .d_expr.get());
+      break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
           << "operator kind with uint32_t argument";
@@ -3550,6 +3586,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
                     CVC4::FloatingPointToFPGeneric(arg1, arg2))
                     .d_expr.get());
       break;
+    case REGEXP_LOOP:
+      res = Op(kind,
+               *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
+                    .d_expr.get());
+      break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
           << "operator kind with two uint32_t arguments";
@@ -3573,7 +3614,7 @@ Term Solver::simplify(const Term& t)
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkValid(void) const
+Result Solver::checkEntailed(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
@@ -3581,14 +3622,15 @@ Result Solver::checkValid(void) const
                  || CVC4::options::incrementalSolving())
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
 
-  CVC4::Result r = d_smtEngine->query();
+  CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkValidAssuming(Term assumption) const
+Result Solver::checkEntailed(const std::vector<Term>& terms) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
@@ -3596,29 +3638,13 @@ Result Solver::checkValidAssuming(Term assumption) const
                  || CVC4::options::incrementalSolving())
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
-  CVC4_API_ARG_CHECK_NOT_NULL(assumption);
-
-  CVC4::Result r = d_smtEngine->query(*assumption.d_expr);
-  return Result(r);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
-  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
-                 || CVC4::options::incrementalSolving())
-      << "Cannot make multiple queries unless incremental solving is enabled "
-         "(try --incremental)";
-  for (const Term& assumption : assumptions)
+  for (const Term& term : terms)
   {
-    CVC4_API_ARG_CHECK_NOT_NULL(assumption);
+    CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
 
-  std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
-  CVC4::Result r = d_smtEngine->query(eassumptions);
+  std::vector<Expr> exprs = termVectorToExprs(terms);
+  CVC4::Result r = d_smtEngine->checkEntailed(exprs);
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 3c99d2480..edff95a2f 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -114,22 +114,21 @@ class CVC4_PUBLIC Result
   bool isSatUnknown() const;
 
   /**
-   * Return true if corresponding query was a valid checkValid() or
-   * checkValidAssuming() query.
+   * Return true if corresponding query was an entailed checkEntailed() query.
    */
-  bool isValid() const;
+  bool isEntailed() const;
 
   /**
-   * Return true if corresponding query was an invalid checkValid() or
-   * checkValidAssuming() query.
+   * Return true if corresponding query was a checkEntailed() query that is
+   * not entailed.
    */
-  bool isInvalid() const;
+  bool isNotEntailed() const;
 
   /**
-   * Return true if query was a checkValid() or checkValidAssuming() query
-   * and CVC4 was not able to determine (in)validity.
+   * Return true if query was a checkEntailed() () query and CVC4 was not able
+   * to determine if it is entailed.
    */
-  bool isValidUnknown() const;
+  bool isEntailmentUnknown() const;
 
   /**
    * Operator overloading for equality of two results.
@@ -2304,6 +2303,20 @@ class CVC4_PUBLIC Solver
   Term mkString(const std::vector<unsigned>& s) const;
 
   /**
+   * Create a character constant from a given string.
+   * @param s the string denoting the code point of the character (in base 16)
+   * @return the character constant
+   */
+  Term mkChar(const std::string& s) const;
+
+  /**
+   * Create a character constant from a given string.
+   * @param s the string denoting the code point of the character (in base 16)
+   * @return the character constant
+   */
+  Term mkChar(const char* s) const;
+
+  /**
    * Create a universe set of the given sort.
    * @param sort the sort of the set elements
    * @return the universe set constant
@@ -2555,24 +2568,19 @@ class CVC4_PUBLIC Solver
   Result checkSatAssuming(const std::vector<Term>& assumptions) const;
 
   /**
-   * Check validity.
-   * @return the result of the validity check.
+   * Check entailment of the given formula w.r.t. the current set of assertions.
+   * @param term the formula to check entailment for
+   * @return the result of the entailment check.
    */
-  Result checkValid() const;
+  Result checkEntailed(Term term) const;
 
   /**
-   * Check validity assuming the given formula.
-   * @param assumption the formula to assume
-   * @return the result of the validity check.
-   */
-  Result checkValidAssuming(Term assumption) const;
-
-  /**
-   * Check validity assuming the given formulas.
-   * @param assumptions the formulas to assume
-   * @return the result of the validity check.
+   * Check entailment of the given set of given formulas w.r.t. the current
+   * set of assertions.
+   * @param terms the terms to check entailment for
+   * @return the result of the entailmentcheck.
    */
-  Result checkValidAssuming(const std::vector<Term>& assumptions) const;
+  Result checkEntailed(const std::vector<Term>& terms) const;
 
   /**
    * Create datatype sort.
@@ -2818,18 +2826,20 @@ class CVC4_PUBLIC Solver
   template <typename T>
   Term mkValHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
-  Term mkRealFromStrHelper(std::string s) const;
+  Term mkRealFromStrHelper(const std::string& s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
-  Term mkBVFromStrHelper(std::string s, uint32_t base) const;
+  Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
   /* Helper for mkBitVector functions that take a string and a size as
    * arguments. */
-  Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const;
+  Term mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const;
   /* Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
   /* Helper for setLogic. */
   void setLogicHelper(const std::string& logic) const;
   /* Helper for mkTerm functions that create Term from a Kind */
   Term mkTermFromKind(Kind kind) const;
+  /* Helper for mkChar functions that take a string as argument. */
+  Term mkCharFromStrHelper(const std::string& s) const;
 
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index d399ad616..f8e1fb90c 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2175,15 +2175,37 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   REGEXP_RANGE,
   /**
-   * Regexp loop.
-   * Parameters: 2 (3)
-   *   -[1]: Term of sort RegExp
-   *   -[2]: Lower bound for the number of repetitions of the first argument
-   *   -[3]: Upper bound for the number of repetitions of the first argument
+   * Operator for regular expression repeat.
+   * Parameters: 1
+   *   -[1]: The number of repetitions
    * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkOp(Kind kind, uint32_t param)
+   *
+   * Apply regular expression loop.
+   * Parameters: 2
+   *   -[1]: Op of kind REGEXP_REPEAT
+   *   -[2]: Term of regular expression sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
+   */
+  REGEXP_REPEAT,
+  /**
+   * Operator for regular expression loop, from lower bound to upper bound
+   * number of repetitions.
+   * Parameters: 2
+   *   -[1]: The lower bound
+   *   -[2]: The upper bound
+   * Create with:
+   *   mkOp(Kind kind, uint32_t param, uint32_t param)
+   *
+   * Apply regular expression loop.
+   * Parameters: 2
+   *   -[1]: Op of kind REGEXP_LOOP
+   *   -[2]: Term of regular expression sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   REGEXP_LOOP,
   /**
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index bbff6f58b..d81d0c0bf 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -87,9 +87,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isSat() except +
         bint isUnsat() except +
         bint isSatUnknown() except +
-        bint isValid() except +
-        bint isInvalid() except +
-        bint isValidUnknown() except +
+        bint isEntailed() except +
+        bint isNotEntailed() except +
+        bint isEntailmentUnknown() except +
         string getUnknownExplanation() except +
         string toString() except +
 
@@ -168,8 +168,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         void assertFormula(Term term) except +
         Result checkSat() except +
         Result checkSatAssuming(const vector[Term]& assumptions) except +
-        Result checkValid() except +
-        Result checkValidAssuming(const vector[Term]& assumptions) except +
+        Result checkEntailed(const vector[Term]& assumptions) except +
         Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors)
         Term declareFun(const string& symbol, Sort sort) except +
         Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 188753122..60bd89cbd 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -749,19 +749,11 @@ cdef class Solver:
             explanation = r.getUnknownExplanation().decode()
         return  Result(name, explanation)
 
-    def checkValid(self):
-        cdef c_Result r = self.csolver.checkValid()
-        name = r.toString().decode()
-        explanation = ""
-        if r.isValidUnknown():
-            explanation = r.getUnknownExplanation().decode()
-        return Result(name, explanation)
-
     @expand_list_arg(num_req_args=0)
-    def checkValidAssuming(self, *assumptions):
+    def checkEntailed(self, *assumptions):
         '''
             Supports the following arguments:
-                 Result checkValidAssuming(List[Term] assumptions)
+                 Result checkEntailed(List[Term] assumptions)
 
                  where assumptions can also be comma-separated arguments of
                  type (boolean) Term
@@ -771,10 +763,10 @@ cdef class Solver:
         cdef vector[c_Term] v
         for a in assumptions:
             v.push_back((<Term?> a).cterm)
-        r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v)
+        r = self.csolver.checkEntailed(<const vector[c_Term]&> v)
         name = r.toString().decode()
         explanation = ""
-        if r.isValidUnknown():
+        if r.isEntailmentUnknown():
             explanation = r.getUnknownExplanation().decode()
         return Result(name, explanation)