Merge branch 'proof-new' into aletheError

NEWS.md

@@ -1,19 +1,45 @@
 This file contains a summary of important user-visible changes.
 
+cvc5 1.1.2
+==========
+
 ## New Features
 
-- Added support for nullable sorts and lift operator to the theory of datatypes.
+- Added support for **nullable** sorts and lift operator to the theory of **datatypes**.
+- Adds a new strategy `--sub-cbqi` (disabled by default) for **quantifier
+  instantiation** which uses subsolvers to compute unsat cores of instantiations
+  that are used in proofs of unsatisfiability.
 
 ## Changes
 
+- SAT clauses are no longer marked as removable in MiniSat. This change
+  **improves performance** overall on quantifier-free logics with arithmetic and
+  strings.
 - **API**
   * Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now
     deprecated and replaced by `std::to_string(Kind)` and
     `std::to_string(SortKind)`. They will be removed in the next minor release.
+- Minor changes to the output format for proofs. Proofs in the AletheLF
+  proof format generated by cvc5 now correspond directly to their representation
+  in proof objects obtained in via the API (the `Proof` class). Moreover,
+  proofs now use SMT-LIB compliant syntax for quantified formulas and unary
+  arithmetic negation.
+- The option `--safe-options` now disallows cases where more than one regular
+  option is used.
+- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive
+  mode.
+- Renamed `bag.duplicate_removal` to `bag.setof`.
 
 cvc5 1.1.1
 ==========
 
+## New Features
+
+- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS**
+  inputs. This allows functions-to-synthesize to include previous
+  functions-to-synthesize in their grammars. This feature is enabled by default
+  for all SyGuS inputs.
+
 ## Changes
 
 - Fixed a bug when piping input from stdin, which caused cvc5 to have degraded

docs/theories/bags.rst

@@ -33,7 +33,7 @@ a `cvc5::Solver solver` object.
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Difference subtract  | ``(bag.difference_subtract X Y)``            | ``Term t = solver.mkTerm(Kind::BAG_DIFFERENCE_SUBTRACT, {X, Y});``      |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Duplicate elimination| ``(bag.duplicate_removal X)``                | ``Term t = solver.mkTerm(Kind::BAG_DUPLICATE_REMOVAL, {X});``           |
+| Duplicate elimination| ``(bag.setof X)``                            | ``Term t = solver.mkTerm(Kind::BAG_SETOF, {X});``                       |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Membership           | ``(bag.member x X)``                         | ``Term x = solver.mkConst(solver.getStringSort(), "x");``               |
 |                      |                                              |                                                                         |
@@ -70,7 +70,7 @@ The semantics of supported bag operators is given in the table below.
 +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
 | difference remove :math:`m_1 \setminus\setminus m_2`| bag.difference_remove   | :math:`\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)` |
 +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
-| duplicate elimination  :math:`\delta(m)`            | bag.duplicate_removal   | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)`                      |
+| setof :math:`\delta(m)`                             | bag.setof               | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)`                      |
 +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
 | subbag :math:`m_1 \subseteq m_2`                    | bag.subbag              | :math:`\forall e. \; m_1(e) \leq m_2(e)`                                           |
 +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+

include/cvc5/cvc5_kind.h

@@ -3812,7 +3812,7 @@ enum ENUM(Kind) : int32_t
    */
   EVALUE(BAG_MEMBER),
   /**
-   * Bag duplicate removal.
+   * Bag setof.
    *
    * Eliminate duplicates in a given bag. The returned bag contains exactly the
    * same elements in the given bag, but with multiplicity one.
@@ -3835,7 +3835,7 @@ enum ENUM(Kind) : int32_t
    *              future versions.
    * \endrst
    */
-  EVALUE(BAG_DUPLICATE_REMOVAL),
+  EVALUE(BAG_SETOF),
   /**
    * Bag make.
    *
@@ -3908,73 +3908,7 @@ enum ENUM(Kind) : int32_t
    *              future versions.
    * \endrst
    */
-  EVALUE(BAG_CHOOSE),
-  /**
-   * Bag is singleton tester.
-   *
-   * - Arity: ``1``
-   *
-   *   - ``1:`` Term of bag Sort
-   *
-   * - Create Term of this Kind with:
-   *
-   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
-   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
-   *
-   * - Create Op of this kind with:
-   *
-   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
-   *
-   * \rst
-   * .. warning:: This kind is experimental and may be changed or removed in
-   *              future versions.
-   * \endrst
-   */
-  EVALUE(BAG_IS_SINGLETON),
-  /**
-   * Conversion from set to bag.
-   *
-   * - Arity: ``1``
-   *
-   *   - ``1:`` Term of set Sort
-   *
-   * - Create Term of this Kind with:
-   *
-   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
-   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
-   *
-   * - Create Op of this kind with:
-   *
-   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
-   *
-   * \rst
-   * .. warning:: This kind is experimental and may be changed or removed in
-   *              future versions.
-   * \endrst
-   */
-  EVALUE(BAG_FROM_SET),
-  /**
-   * Conversion from bag to set.
-   *
-   * - Arity: ``1``
-   *
-   *   - ``1:`` Term of bag Sort
-   *
-   * - Create Term of this Kind with:
-   *
-   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
-   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
-   *
-   * - Create Op of this kind with:
-   *
-   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
-   *
-   * \rst
-   * .. warning:: This kind is experimental and may be changed or removed in
-   *              future versions.
-   * \endrst
-   */
-  EVALUE(BAG_TO_SET),
+  EVALUE(BAG_CHOOSE),  
   /**
    * Bag map.
    *

proofs/alf/cvc5/theories/Bags.smt3

@@ -18,7 +18,7 @@
 (declare-const bag.member (-> (! Type :var T :implicit) T (Bag T) Bool))
 (declare-const bag.card (-> (! Type :var T :implicit) (Bag T) Int))
 (declare-const bag.choose (-> (! Type :var T :implicit) (Bag T) T))
-(declare-const bag.duplicate_removal (-> (! Type :var T :implicit) (Bag T) (Bag T)))
+(declare-const bag.setof (-> (! Type :var T :implicit) (Bag T) (Bag T)))
 (declare-const bag.is_singleton (-> (! Type :var T :implicit) (Bag T) Bool))
 
 (declare-const bag.filter (-> (! Type :var T :implicit) (-> T Bool) (Bag T) (Bag T)))

proofs/lfsc/signatures/theory_def.plf

@@ -545,8 +545,8 @@
 (define bag.count (# x term (# y term (apply (apply f_bag.count x) y))))
 (declare f_bag term)
 (define bag (# x term (# y term (apply (apply f_bag x) y))))
-(declare f_bag.duplicate_removal term)
-(define bag.duplicate_removal (# x term (apply f_bag.duplicate_removal x)))
+(declare f_bag.setof term)
+(define bag.setof (# x term (apply f_bag.setof x)))
 (declare f_bag.card term)
 (define bag.card (# x term (apply f_bag.card x)))
 (declare f_bag.choose term)

src/CMakeLists.txt

@@ -252,6 +252,8 @@ libcvc5_add_sources(
   prop/kissat.h
   prop/learned_db.cpp
   prop/learned_db.h
+  prop/lemma_inprocess.cpp
+  prop/lemma_inprocess.h
   prop/minisat/core/Dimacs.h
   prop/minisat/core/Solver.cc
   prop/minisat/core/Solver.h

src/api/cpp/cvc5.cpp

@@ -355,15 +355,11 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
         KIND_ENUM(Kind::BAG_SUBBAG, internal::Kind::BAG_SUBBAG),
         KIND_ENUM(Kind::BAG_COUNT, internal::Kind::BAG_COUNT),
         KIND_ENUM(Kind::BAG_MEMBER, internal::Kind::BAG_MEMBER),
-        KIND_ENUM(Kind::BAG_DUPLICATE_REMOVAL,
-                  internal::Kind::BAG_DUPLICATE_REMOVAL),
+        KIND_ENUM(Kind::BAG_SETOF, internal::Kind::BAG_SETOF),
         KIND_ENUM(Kind::BAG_MAKE, internal::Kind::BAG_MAKE),
         KIND_ENUM(Kind::BAG_EMPTY, internal::Kind::BAG_EMPTY),
         KIND_ENUM(Kind::BAG_CARD, internal::Kind::BAG_CARD),
         KIND_ENUM(Kind::BAG_CHOOSE, internal::Kind::BAG_CHOOSE),
-        KIND_ENUM(Kind::BAG_IS_SINGLETON, internal::Kind::BAG_IS_SINGLETON),
-        KIND_ENUM(Kind::BAG_FROM_SET, internal::Kind::BAG_FROM_SET),
-        KIND_ENUM(Kind::BAG_TO_SET, internal::Kind::BAG_TO_SET),
         KIND_ENUM(Kind::BAG_MAP, internal::Kind::BAG_MAP),
         KIND_ENUM(Kind::BAG_FILTER, internal::Kind::BAG_FILTER),
         KIND_ENUM(Kind::BAG_FOLD, internal::Kind::BAG_FOLD),
@@ -752,14 +748,11 @@ const static std::unordered_map<internal::Kind,
         {internal::Kind::BAG_SUBBAG, Kind::BAG_SUBBAG},
         {internal::Kind::BAG_COUNT, Kind::BAG_COUNT},
         {internal::Kind::BAG_MEMBER, Kind::BAG_MEMBER},
-        {internal::Kind::BAG_DUPLICATE_REMOVAL, Kind::BAG_DUPLICATE_REMOVAL},
+        {internal::Kind::BAG_SETOF, Kind::BAG_SETOF},
         {internal::Kind::BAG_MAKE, Kind::BAG_MAKE},
         {internal::Kind::BAG_EMPTY, Kind::BAG_EMPTY},
         {internal::Kind::BAG_CARD, Kind::BAG_CARD},
         {internal::Kind::BAG_CHOOSE, Kind::BAG_CHOOSE},
-        {internal::Kind::BAG_IS_SINGLETON, Kind::BAG_IS_SINGLETON},
-        {internal::Kind::BAG_FROM_SET, Kind::BAG_FROM_SET},
-        {internal::Kind::BAG_TO_SET, Kind::BAG_TO_SET},
         {internal::Kind::BAG_MAP, Kind::BAG_MAP},
         {internal::Kind::BAG_FILTER, Kind::BAG_FILTER},
         {internal::Kind::BAG_FOLD, Kind::BAG_FOLD},

src/options/theory_options.toml

@@ -66,3 +66,44 @@ name   = "Theory Layer"
 [[option.mode.CARE_GRAPH]]
   name = "care-graph"
   help = "Use care graphs for theory combination."
+
+[[option]]
+  name       = "lemmaInprocess"
+  category   = "expert"
+  long       = "lemma-inprocess=MODE"
+  type       = "LemmaInprocessMode"
+  default    = "NONE"
+  help       = "Modes for inprocessing lemmas."
+  help_mode  = "Modes for inprocessing lemmas."
+[[option.mode.FULL]]
+  name = "full"
+  help = "Full inprocessing."
+[[option.mode.LIGHT]]
+  name = "light"
+  help = "Light inprocessing."
+[[option.mode.NONE]]
+  name = "none"
+  help = "No inprocessing."
+
+[[option]]
+  name       = "lemmaInprocessSubsMode"
+  category   = "expert"
+  long       = "lemma-inprocess-subs=MODE"
+  type       = "LemmaInprocessSubsMode"
+  default    = "SIMPLE"
+  help       = "Modes for substitutions for inprocessing lemmas."
+  help_mode  = "Modes for substitutions for inprocessing lemmas."
+[[option.mode.ALL]]
+  name = "all"
+  help = "All substitutions."
+[[option.mode.SIMPLE]]
+  name = "simple"
+  help = "Simple substitutions."
+
+[[option]]
+  name       = "lemmaInprocessInferEqLit"
+  category   = "expert"
+  long       = "lemma-inprocess-infer-eq-lit"
+  type       = "bool"
+  default    = "false"
+  help       = "Infer equivalent literals when using lemma inprocess"

src/parser/smt2/smt2_state.cpp

@@ -898,13 +898,10 @@ void Smt2State::setLogic(std::string name)
     addOperator(Kind::BAG_SUBBAG, "bag.subbag");
     addOperator(Kind::BAG_COUNT, "bag.count");
     addOperator(Kind::BAG_MEMBER, "bag.member");
-    addOperator(Kind::BAG_DUPLICATE_REMOVAL, "bag.duplicate_removal");
+    addOperator(Kind::BAG_SETOF, "bag.setof");
     addOperator(Kind::BAG_MAKE, "bag");
     addOperator(Kind::BAG_CARD, "bag.card");
     addOperator(Kind::BAG_CHOOSE, "bag.choose");
-    addOperator(Kind::BAG_IS_SINGLETON, "bag.is_singleton");
-    addOperator(Kind::BAG_FROM_SET, "bag.from_set");
-    addOperator(Kind::BAG_TO_SET, "bag.to_set");
     addOperator(Kind::BAG_MAP, "bag.map");
     addOperator(Kind::BAG_FILTER, "bag.filter");
     addOperator(Kind::BAG_FOLD, "bag.fold");

src/printer/smt2/smt2_printer.cpp

@@ -1216,13 +1216,10 @@ std::string Smt2Printer::smtKindString(Kind k)
     case Kind::BAG_SUBBAG: return "bag.subbag";
     case Kind::BAG_COUNT: return "bag.count";
     case Kind::BAG_MEMBER: return "bag.member";
-    case Kind::BAG_DUPLICATE_REMOVAL: return "bag.duplicate_removal";
+    case Kind::BAG_SETOF: return "bag.setof";
     case Kind::BAG_MAKE: return "bag";
     case Kind::BAG_CARD: return "bag.card";
     case Kind::BAG_CHOOSE: return "bag.choose";
-    case Kind::BAG_IS_SINGLETON: return "bag.is_singleton";
-    case Kind::BAG_FROM_SET: return "bag.from_set";
-    case Kind::BAG_TO_SET: return "bag.to_set";
     case Kind::BAG_MAP: return "bag.map";
     case Kind::BAG_FILTER: return "bag.filter";
     case Kind::BAG_FOLD: return "bag.fold";

src/proof/alethe/alethe_post_processor.cpp

@@ -2760,5 +2760,11 @@ bool AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf,
   return true;
 }
 
+}  // namespace proof
+}  // namespace cvc5::internal
+
+  return true;
+}
+
 }  // namespace proof
 }  // namespace cvc5::internal

src/proof/trust_node.cpp

@@ -74,6 +74,11 @@ TrustNode TrustNode::mkReplaceGenTrustNode(const TrustNode& orig,
   return TrustNode(orig.getKind(), orig.getProven(), g);
 }
 
+TrustNode TrustNode::mkTrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
+{
+  return TrustNode(tnk, p, g);
+}
+
 TrustNode TrustNode::null()
 {
   return TrustNode(TrustNodeKind::INVALID, Node::null());

src/proof/trust_node.h

@@ -96,6 +96,10 @@ class TrustNode
   /** Make a trust node, replacing the original generator */
   static TrustNode mkReplaceGenTrustNode(const TrustNode& orig,
                                          ProofGenerator* g);
+  /** Make a trust node with the given explicit arguments. */
+  static TrustNode mkTrustNode(TrustNodeKind tnk,
+                               Node p,
+                               ProofGenerator* g = nullptr);
   /** The null proven node */
   static TrustNode null();
   ~TrustNode() {}