Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * encoding Nodes as cocoa ring elements.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifdef CVC5_USE_COCOA
      16                 :            : 
      17                 :            : #ifndef CVC5__THEORY__FF__COCOA_H
      18                 :            : #define CVC5__THEORY__FF__COCOA_H
      19                 :            : 
      20                 :            : // external includes
      21                 :            : #include <CoCoA/ring.H>
      22                 :            : #include <CoCoA/symbol.H>
      23                 :            : 
      24                 :            : // std includes
      25                 :            : #include <optional>
      26                 :            : #include <string>
      27                 :            : #include <unordered_map>
      28                 :            : #include <unordered_set>
      29                 :            : 
      30                 :            : // internal includes
      31                 :            : #include "expr/node.h"
      32                 :            : #include "theory/ff/cocoa_util.h"
      33                 :            : #include "theory/ff/core.h"
      34                 :            : #include "theory/ff/util.h"
      35                 :            : 
      36                 :            : namespace cvc5::internal {
      37                 :            : namespace theory {
      38                 :            : namespace ff {
      39                 :            : 
      40                 :            : /**
      41                 :            :  *  Create cocoa symbol, sanitizing varName.
      42                 :            :  *  If index is given, subscript the symbol by it.
      43                 :            :  */
      44                 :            : CoCoA::symbol cocoaSym(const std::string& varName,
      45                 :            :                        std::optional<size_t> index = {});
      46                 :            : 
      47                 :            : /**
      48                 :            :  * Class for encoding a Node as a Poly.
      49                 :            :  *
      50                 :            :  * Requires two passes over the nodes. On the first pass it collects variables,
      51                 :            :  * !=s, and bitsums. On the second, it encodes. The first stage is called
      52                 :            :  * "Stage::Scan", the second is "Stage::Encode".
      53                 :            :  *
      54                 :            :  * Two stages are necessary because when creating a CoCoA polynomial ring, one
      55                 :            :  * must declare all the variables up-front. So, before we create any polynomials
      56                 :            :  * (to encode terms), we must know all the (CoCoA) variables. CoCoA variables
      57                 :            :  * are used to encode cvc5 variables, bitsums, and witnesses of disequality (a
      58                 :            :  * != b is encoded as (a - b)w = 1, where w is the witness).
      59                 :            :  */
      60                 :            : class CocoaEncoder : public FieldObj
      61                 :            : {
      62                 :            :  public:
      63                 :            :   /** Create a new encoder, for this field. */
      64                 :            :   CocoaEncoder(NodeManager* nm, const FfSize& size);
      65                 :            :   /** Add a fact (one must call this twice per fact, once per stage). */
      66                 :            :   void addFact(const Node& fact);
      67                 :            :   /** Start Stage::Encode. */
      68                 :            :   void endScan();
      69                 :            :   /**
      70                 :            :    * Get the polys who's common zero we are finding (excluding bitsums).
      71                 :            :    * Available in Stage::Encode.
      72                 :            :    */
      73                 :       5290 :   const std::vector<Poly>& polys() const { return d_polys; }
      74                 :            :   /**
      75                 :            :    * Get the bitsum polys.
      76                 :            :    * These have form: x - b0 - 2*b1 - 4b2 ... - 2^n*b_n.
      77                 :            :    * Available in Stage::Encode.
      78                 :            :    */
      79                 :       4452 :   const std::vector<Poly>& bitsumPolys() const { return d_bitsumPolys; }
      80                 :            :   /**
      81                 :            :    * Get the poly for this term
      82                 :            :    * Available in Stage::Encode.
      83                 :            :    */
      84                 :       5109 :   const Poly& getTermEncoding(const Node& t) const { return d_cache.at(t); }
      85                 :            :   /**
      86                 :            :    * Get the bitsum terms (for the bitsumPolys).
      87                 :            :    * Available in Stage::Encode.
      88                 :            :    */
      89                 :            :   std::vector<Node> bitsums() const;
      90                 :            :   /**
      91                 :            :    * The coefficient ring of the poly ring we're encoding into.
      92                 :            :    * Available in Stage::Encode.
      93                 :            :    */
      94                 :         26 :   const CoCoA::ring& coeffRing() const { return d_coeffRing.value(); }
      95                 :            :   /**
      96                 :            :    * The poly ring we've encoded into.
      97                 :            :    * Available in Stage::Encode.
      98                 :            :    */
      99                 :       2792 :   const CoCoA::ring& polyRing() const { return d_polyRing.value(); }
     100                 :            :   /**
     101                 :            :    * A list of (indeterminant num, Node) pairs. Useful for extracting a model.
     102                 :            :    * Available in Stage::Encode.
     103                 :            :    */
     104                 :            :   std::vector<std::pair<size_t, Node>> nodeIndets() const;
     105                 :            :   /**
     106                 :            :    * Convert a (coefficient) Scalar to a FiniteFieldValue.
     107                 :            :    */
     108                 :            :   FiniteFieldValue cocoaFfToFfVal(const Scalar& elem) const;
     109                 :            :   /**
     110                 :            :    * Does some fact that imply this poly?
     111                 :            :    */
     112                 :            :   bool polyHasFact(const Poly& poly) const;
     113                 :            :   /**
     114                 :            :    * Get the fact that implies this poly.
     115                 :            :    */
     116                 :            :   const Node& polyFact(const Poly& poly) const;
     117                 :            : 
     118                 :            :  private:
     119                 :            :   /**
     120                 :            :    * Get a fresh symbol that starts with varName.
     121                 :            :    * If index is given, subscript the symbol by it.
     122                 :            :    */
     123                 :            :   CoCoA::symbol freshSym(const std::string& varName,
     124                 :            :                          std::optional<size_t> index = {});
     125                 :            :   /** a bitsum or a var */
     126                 :            :   const Node& symNode(CoCoA::symbol s) const;
     127                 :            :   /** have we assigned this symbol to some Node? */
     128                 :            :   bool hasNode(CoCoA::symbol s) const;
     129                 :            :   /** get the poly for this symbol */
     130                 :            :   const Poly& symPoly(CoCoA::symbol s) const;
     131                 :            :   /** encode this term as a poly (caching) */
     132                 :            :   void encodeTerm(const Node& t);
     133                 :            :   /** encode this fact as a poly that must be zero (caching) */
     134                 :            :   void encodeFact(const Node& f);
     135                 :            : 
     136                 :            :   /** Which pass we're in. */
     137                 :            :   enum class Stage
     138                 :            :   {
     139                 :            :     /** collecting: variable, !=, bitsum */
     140                 :            :     Scan,
     141                 :            :     /** encoding terms */
     142                 :            :     Encode,
     143                 :            :   };
     144                 :            : 
     145                 :            :   // configuration
     146                 :            : 
     147                 :            :   /** the stage that we're in; initially scanning */
     148                 :            :   Stage d_stage{Stage::Scan};
     149                 :            : 
     150                 :            :   // populated during Stage::Scan
     151                 :            : 
     152                 :            :   /** all nodes scanned */
     153                 :            :   std::unordered_set<Node> d_scanned{};
     154                 :            :   /** all variables seen */
     155                 :            :   std::unordered_set<std::string> d_vars{};
     156                 :            :   /** map: bitsum term to its symbol */
     157                 :            :   std::unordered_map<Node, CoCoA::symbol> d_bitsumSyms{};
     158                 :            :   /** map: variable term to its symbol */
     159                 :            :   std::unordered_map<Node, CoCoA::symbol> d_varSyms{};
     160                 :            :   /** map: term (a != b) to the symbol for the inverse of (a - b) */
     161                 :            :   std::unordered_map<Node, CoCoA::symbol> d_diseqSyms{};
     162                 :            :   /** all symbols */
     163                 :            :   std::vector<CoCoA::symbol> d_syms{};
     164                 :            :   /** map: symbol name to polynomial */
     165                 :            :   std::unordered_map<std::string, Poly> d_symPolys{};
     166                 :            :   /** map: symbol name to term */
     167                 :            :   std::unordered_map<std::string, Node> d_symNodes{};
     168                 :            : 
     169                 :            :   // populated at the end of Stage::Scan
     170                 :            : 
     171                 :            :   /** the coefficient ring */
     172                 :            :   std::optional<CoCoA::ring> d_coeffRing{};
     173                 :            :   /** the polynomial ring */
     174                 :            :   std::optional<CoCoA::ring> d_polyRing{};
     175                 :            : 
     176                 :            :   // populated during Stage::Encode
     177                 :            : 
     178                 :            :   /** encoding cache */
     179                 :            :   std::unordered_map<Node, Poly> d_cache{};
     180                 :            :   /** polynomials that must be zero (except bitsums) */
     181                 :            :   std::vector<Poly> d_polys{};
     182                 :            :   /** bitsum polynomials that must be zero */
     183                 :            :   std::vector<Poly> d_bitsumPolys{};
     184                 :            :   /** polys to the facts that imply them */
     185                 :            :   std::unordered_map<std::string, Node> d_polyFacts{};
     186                 :            : };
     187                 :            : 
     188                 :            : }  // namespace ff
     189                 :            : }  // namespace theory
     190                 :            : }  // namespace cvc5::internal
     191                 :            : 
     192                 :            : #endif /* CVC5__THEORY__FF__COCOA_H */
     193                 :            : 
     194                 :            : #endif /* CVC5_USE_COCOA */