/usr/include/cvc3/theory_array.h is in libcvc3-dev 2.4.1-5ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 | /*****************************************************************************/
/*!
* \file theory_array.h
*
* Author: Clark Barrett
*
* Created: Wed Feb 26 18:32:06 2003
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__include__theory_array_h_
#define _cvc3__include__theory_array_h_
#include "theory_core.h"
namespace CVC3 {
class ArrayProofRules;
typedef enum {
ARRAY = 2000,
READ,
WRITE,
// Array literal [ [type] e ]; creates a constant array holding 'e'
// in all elements: (CONST_ARRAY type e)
ARRAY_LITERAL
} ArrayKinds;
/*****************************************************************************/
/*!
*\class TheoryArray
*\ingroup Theories
*\brief This theory handles arrays.
*
* Author: Clark Barrett
*
* Created: Thu Feb 27 00:38:20 2003
*/
/*****************************************************************************/
class TheoryArray :public Theory {
ArrayProofRules* d_rules;
//! Backtracking list of array reads, for building concrete models.
CDList<Expr> d_reads;
//! Set of renaming theorems \f$\exists x. t = x\f$ indexed by t
ExprMap<Theorem> d_renameThms;
//! Flag to include array reads to the concrete model
const bool& d_applicationsInModel;
//! Flag to lift ite's over reads
const bool& d_liftReadIte;
//! Backtracking database of subterms of shared terms
CDMap<Expr,Expr> d_sharedSubterms;
//! Backtracking database of subterms of shared terms
CDList<Expr> d_sharedSubtermsList;
//! Used in checkSat
CDO<unsigned> d_index;
CDO<size_t> d_sharedIdx1, d_sharedIdx2;
//! Flag for use in checkSat
int d_inCheckSat;
//! Derived rule
// w(...,i,v1,...,) => w(......,i,v1')
// Returns Null Theorem if index does not appear
Theorem pullIndex(const Expr& e, const Expr& index);
public:
TheoryArray(TheoryCore* core);
~TheoryArray();
// Trusted method that creates the proof rules class (used in constructor).
// Implemented in array_theorem_producer.cpp
ArrayProofRules* createProofRules();
// Theory interface
void addSharedTerm(const Expr& e);
void assertFact(const Theorem& e);
void checkSat(bool fullEffort);
Theorem rewrite(const Expr& e);
void setup(const Expr& e);
void update(const Theorem& e, const Expr& d);
Theorem solve(const Theorem& e);
void checkType(const Expr& e);
Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
bool enumerate, bool computeSize);
void computeType(const Expr& e);
Type computeBaseType(const Type& t);
void computeModelTerm(const Expr& e, std::vector<Expr>& v);
void computeModel(const Expr& e, std::vector<Expr>& vars);
Expr computeTCC(const Expr& e);
virtual Expr parseExprOp(const Expr& e);
ExprStream& print(ExprStream& os, const Expr& e);
Expr getBaseArray(const Expr& e) const;
};
// Array testers
inline bool isArray(const Type& t) { return t.getExpr().getKind() == ARRAY; }
inline bool isRead(const Expr& e) { return e.getKind() == READ; }
inline bool isWrite(const Expr& e) { return e.getKind() == WRITE; }
inline bool isArrayLiteral(const Expr& e)
{ return (e.isClosure() && e.getKind() == ARRAY_LITERAL); }
// Array constructors
inline Type arrayType(const Type& type1, const Type& type2)
{ return Type(Expr(ARRAY, type1.getExpr(), type2.getExpr())); }
// Expr read(const Expr& arr, const Expr& index);
// Expr write(const Expr& arr, const Expr& index, const Expr& value);
Expr arrayLiteral(const Expr& ind, const Expr& body);
} // end of namespace CVC3
#endif
|