1 
2 /*
3  * File FiniteModelMultiSorted.hpp.
4  *
5  * This file is part of the source code of the software program
6  * Vampire. It is protected by applicable
7  * copyright laws.
8  *
9  * This source code is distributed under the licence found here
10  * https://vprover.github.io/license.html
11  * and in the source directory
12  *
13  * In summary, you are allowed to use Vampire for non-commercial
14  * purposes but not allowed to distribute, modify, copy, create derivatives,
15  * or use in competitions.
16  * For other uses of Vampire please contact developers for a different
17  * licence, which we will make an effort to provide.
18  */
19 /**
20  * @file FiniteModelMultiSorted.hpp
21  * Defines class for finite models
22  *
23  * @since 6/01/2016 Manchester
24  * @author Giles
25  */
26 
27 #ifndef __FiniteModelMultiSorted__
28 #define __FiniteModelMultiSorted__
29 
30 #include "Lib/Allocator.hpp"
31 #include "Lib/DHMap.hpp"
32 
33 #include "Kernel/Unit.hpp"
34 #include "Kernel/Term.hpp"
35 
36 
37 namespace FMB {
38 
39 using namespace Lib;
40 using namespace Kernel;
41 
42 /**
43  *
44  *
45  */
46 class FiniteModelMultiSorted {
47  CLASS_NAME(FiniteModelMultiSorted);
48  USE_ALLOCATOR(FiniteModelMultiSorted);
49 
50  DHMap<unsigned,unsigned> _sizes;
51 
52 public:
53 
54  // sortSizes is a map from vampire sorts (defined in Kernel/Sorts) to the size of that sort
55  FiniteModelMultiSorted(DHMap<unsigned,unsigned> sortSizes);
56 
57  // Assume def is an equality literal with a
58  // function application on lhs and constant on rhs
59  void addConstantDefinition(unsigned f, unsigned res);
60  void addFunctionDefinition(unsigned f, const DArray<unsigned>& args, unsigned res);
61  // Assume def is non-equality ground literal
62  void addPropositionalDefinition(unsigned f, bool res);
63  void addPredicateDefinition(unsigned f, const DArray<unsigned>& args, bool res);
64 
65  bool isPartial();
66 
67  bool evaluate(Unit* unit);
68  unsigned evaluateGroundTerm(Term* term);
69  bool evaluateGroundLiteral(Literal* literal);
70 
71  vstring toString();
72 
73 private:
74 
75  Formula* partialEvaluate(Formula* formula);
76  // currently private as requires formula to be rectified
77  bool evaluate(Formula* formula,unsigned depth=0);
78 
79  // The model is partial if there is a operation with arity n that does not have
80  // coverage size^n in its related coverage map
81  bool _isPartial;
82  DHMap<unsigned,unsigned> _functionCoverage;
83  DHMap<unsigned,unsigned> _predicateCoverage;
84 
85  DArray<DArray<int>> sortRepr;
86 
87  DArray<unsigned> f_offsets;
88  DArray<unsigned> p_offsets;
89  DArray<unsigned> f_interpretation;
90  DArray<unsigned> p_interpretation; // 0 is undef, 1 false, 2 true
91 
92  // the pairs of <constant number, sort>
93  DHMap<pair<unsigned,unsigned>,Term*> _domainConstants;
94  DHMap<Term*,pair<unsigned,unsigned>> _domainConstantsRev;
95 public:
getDomainConstant(unsigned c,unsigned srt)96  Term* getDomainConstant(unsigned c, unsigned srt)
97  {
98    Term* t;
99    pair<unsigned,unsigned> pair = make_pair(c,srt);
100    if(_domainConstants.find(pair,t)) return t;
101    vstring name = "domCon_"+env.sorts->sortName(srt)+"_"+Lib::Int::toString(c);
102    unsigned f = env.signature->addFreshFunction(0,name.c_str());
103    env.signature->getFunction(f)->setType(OperatorType::getConstantsType(srt));
104    t = Term::createConstant(f);
105    _domainConstants.insert(pair,t);
106    _domainConstantsRev.insert(t,pair);
107 
108    return t;
109  }
getDomainConstant(Term * t)110  pair<unsigned,unsigned> getDomainConstant(Term* t)
111  {
112    pair<unsigned,unsigned> pair;
113    if(_domainConstantsRev.find(t,pair)) return pair;
114    USER_ERROR("Evaluated to "+t->toString()+" when expected a domain constant, probably a partial model");
115  }
isDomainConstant(Term * t)116  bool isDomainConstant(Term* t)
117  {
118    return _domainConstantsRev.find(t);
119  }
prepend(const char * prefix,vstring name)120  vstring prepend(const char* prefix, vstring name) {
121    if (name.empty()) {
122      return vstring(prefix);
123    } else if (name[0] == '\'') {
124      vstring dequoted = name.substr(1, name.length() - 1);
125      return vstring("'") + prefix + dequoted;
126    } else {
127      return prefix + name;
128    }
129  }
append(vstring name,const char * suffix)130  vstring append(vstring name, const char* suffix) {
131    if (name.empty()) {
132      return vstring(suffix);
133    } else if (name[0] == '\'') {
134      vstring dequoted = name.substr(0, name.length() - 1);
135      return dequoted + suffix + "'";
136    } else {
137      return name + suffix;
138    }
139  }
140 };
141 
142 
143 } // namespace FMB
144 #endif
145