This method unnecessarily complicates the usage of CDHashMap. It had one usage in the current code, for dealing with global declarations. However, this was an entirely artificial use case, as one should properly manage scopes when this option is true (i.e. global-declarations simply disables user-level scoping in the symbol table).
It also simplifies the symbol table so that it doesn't automatically push a global outermost scope. Instead, this scope is pushed when the logic is declared, so that background symbols are correctly added at level 0.
Fixes #4767.
CDOhash_map(Context* context,
CDHashMap<Key, Data, HashFcn>* map,
const Key& key,
- const Data& data,
- bool atLevelZero = false)
+ const Data& data)
: ContextObj(false, context), d_value(key, data), d_map(NULL)
{
- if (atLevelZero)
- {
- // "Initializing" map insertion: this entry will never be
- // removed from the map, it's inserted at level 0 as an
- // "initializing" element. See
- // CDHashMap<>::insertAtContextLevelZero().
- mutable_data() = data;
- }
- else
- {
- // Normal map insertion: first makeCurrent(), then set the data
- // and then, later, the map. Order is important; we can't
- // initialize d_map in the constructor init list above, because
- // we want the restore of d_map to NULL to signal us to remove
- // the element from the map.
+ // Normal map insertion: first makeCurrent(), then set the data
+ // and then, later, the map. Order is important; we can't
+ // initialize d_map in the constructor init list above, because
+ // we want the restore of d_map to NULL to signal us to remove
+ // the element from the map.
- set(data);
- }
+ set(data);
d_map = map;
CDOhash_map*& first = d_map->d_first;
return res.second;
}
- /**
- * Version of insert() for CDHashMap<> that inserts data value d at
- * context level zero. This is a special escape hatch for inserting
- * "initializing" data into the map. Imagine something happens at a
- * deep context level L that causes insertion into a map, such that
- * the object should have an "initializing" value v1 below context
- * level L, and a "current" value v2 at context level L. Then you
- * can (assuming key k):
- *
- * map.insertAtContextLevelZero(k, v1);
- * map.insert(k, v2);
- *
- * The justification for this "escape hatch" has to do with
- * variables and assignments in theories (e.g., in arithmetic).
- * Let's say you introduce a new variable x at some deep decision
- * level (thanks to lazy registration, or a splitting lemma, or
- * whatever). x might be mapped to something, but for theory
- * implementation simplicity shouldn't disappear from the map on
- * backjump; rather, it can take another (legal) value, or a special
- * value to indicate it needs to be recomputed.
- *
- * It is an error (checked via AlwaysAssert()) to
- * insertAtContextLevelZero() a key that already is in the map.
- */
- void insertAtContextLevelZero(const Key& k, const Data& d)
- {
- AlwaysAssert(d_map.find(k) == d_map.end());
-
- Element* obj =
- new (true) Element(d_context, this, k, d, true /* atLevelZero */);
- d_map.insert(std::make_pair(k, obj));
- }
-
// FIXME: no erase(), too much hassle to implement efficiently...
using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
return super::key_end();
}
- void insertAtContextLevelZero(const V& v) {
- return super::insertAtContextLevelZero(v, true);
- }
-
}; /* class CDHashSet */
} // namespace context
* - Use insert_safe if you want to check if the element has been inserted
* and only insert if it has not yet been.
* - Does not accept TNodes as keys.
- * - Supports insertAtContextLevelZero() if the element is not in the map.
*/
#include <deque>
/** For restores, we need to keep track of the previous size. */
size_t d_size;
- /**
- * To support insertAtContextLevelZero() and restores,
- * we have called d_insertMap->d_pushFront().
- */
- size_t d_pushFronts;
-
/**
* Private copy constructor used only by save(). d_insertMap is
* not copied: only the base class information and
- * d_size and d_pushFronts are needed in restore.
+ * d_size are needed in restore.
*/
- CDInsertHashMap(const CDInsertHashMap& l) :
- ContextObj(l),
- d_insertMap(NULL),
- d_size(l.d_size),
- d_pushFronts(l.d_pushFronts)
+ CDInsertHashMap(const CDInsertHashMap& l)
+ : ContextObj(l), d_insertMap(nullptr), d_size(l.d_size)
{
Debug("CDInsertHashMap") << "copy ctor: " << this
<< " from " << &l
return data;
}
protected:
- /**
- * Implementation of mandatory ContextObj method restore:
- * restore to the previous size taking into account the number
- * of new pushFront calls have happened since saving.
- * The d_insertMap is untouched and d_pushFronts is also kept.
- */
+ /**
+ * Implementation of mandatory ContextObj method restore:
+ * restore to the previous size taking into account the number
+ * of new pushFront calls have happened since saving.
+ * The d_insertMap is untouched.
+ */
void restore(ContextObj* data) override
{
Debug("CDInsertHashMap")
<< " data == " << data << " d_insertMap == " << this->d_insertMap
<< std::endl;
size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
- size_t oldPushFronts =
- ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
- Assert(oldPushFronts <= d_pushFronts);
// The size to restore to.
- size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
+ size_t restoreSize = oldSize;
d_insertMap->pop_to_size(restoreSize);
d_size = restoreSize;
Assert(d_insertMap->size() == d_size);
/**
* Main constructor: d_insertMap starts as an empty map, with the size is 0
*/
- CDInsertHashMap(Context* context) :
- ContextObj(context),
- d_insertMap(new IHM()),
- d_size(0),
- d_pushFronts(0){
- Assert(d_insertMap->size() == d_size);
- }
+ CDInsertHashMap(Context* context)
+ : ContextObj(context), d_insertMap(new IHM()), d_size(0)
+ {
+ Assert(d_insertMap->size() == d_size);
+ }
/**
* Destructor: delete the d_insertMap
}
}
- /**
- * Version of insert() for CDMap<> that inserts data value d at
- * context level zero.
- *
- * It is an error to insertAtContextLevelZero()
- * a key that already is in the map.
- */
- void insertAtContextLevelZero(const Key& k, const Data& d){
- makeCurrent();
- ++d_size;
- ++d_pushFronts;
- d_insertMap->push_front(k, d);
- }
-
/** Returns true if k is a mapped key in the context. */
bool contains(const Key& k) const {
return d_insertMap->contains(k);
void SymbolManager::reset()
{
+ // reset resets the symbol table even when global declarations are true
d_symtabAllocated.reset();
d_implementation->reset();
}
void SymbolManager::resetAssertions()
{
d_implementation->resetAssertions();
- d_symtabAllocated.resetAssertions();
+ if (!d_globalDeclarations)
+ {
+ d_symtabAllocated.resetAssertions();
+ }
}
} // namespace cvc5
d_typeMap(&d_context),
d_overload_trie(&d_context)
{
- // use an outermost push, to be able to clear definitions not at level zero
- d_context.push();
}
- ~Implementation() { d_context.pop(); }
+ ~Implementation() {}
- bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload);
- void bindType(const string& name, api::Sort t, bool levelZero = false);
+ bool bind(const string& name, api::Term obj, bool doOverload);
+ void bindType(const string& name, api::Sort t);
void bindType(const string& name,
const vector<api::Sort>& params,
- api::Sort t,
- bool levelZero = false);
+ api::Sort t);
bool isBound(const string& name) const;
bool isBoundType(const string& name) const;
api::Term lookup(const string& name) const;
bool SymbolTable::Implementation::bind(const string& name,
api::Term obj,
- bool levelZero,
bool doOverload)
{
PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null api::Term");
Trace("sym-table") << "SymbolTable: bind " << name
- << ", levelZero=" << levelZero
<< ", doOverload=" << doOverload << std::endl;
if (doOverload) {
if (!bindWithOverloading(name, obj)) {
return false;
}
}
- if (levelZero) {
- d_exprMap.insertAtContextLevelZero(name, obj);
- } else {
d_exprMap.insert(name, obj);
- }
+
return true;
}
}
}
-void SymbolTable::Implementation::bindType(const string& name,
- api::Sort t,
- bool levelZero)
+void SymbolTable::Implementation::bindType(const string& name, api::Sort t)
{
- if (levelZero) {
- d_typeMap.insertAtContextLevelZero(name, make_pair(vector<api::Sort>(), t));
- } else {
d_typeMap.insert(name, make_pair(vector<api::Sort>(), t));
- }
}
void SymbolTable::Implementation::bindType(const string& name,
const vector<api::Sort>& params,
- api::Sort t,
- bool levelZero)
+ api::Sort t)
{
if (Debug.isOn("sort")) {
Debug("sort") << "bindType(" << name << ", [";
}
Debug("sort") << "], " << t << ")" << endl;
}
- if (levelZero) {
- d_typeMap.insertAtContextLevelZero(name, make_pair(params, t));
- } else {
+
d_typeMap.insert(name, make_pair(params, t));
- }
}
bool SymbolTable::Implementation::isBoundType(const string& name) const {
void SymbolTable::Implementation::popScope() {
// should not pop beyond level one
- if (d_context.getLevel() == 1)
+ if (d_context.getLevel() == 0)
{
throw ScopeException();
}
SymbolTable::~SymbolTable() {}
bool SymbolTable::bind(const string& name,
api::Term obj,
- bool levelZero,
bool doOverload)
{
- return d_implementation->bind(name, obj, levelZero, doOverload);
+ return d_implementation->bind(name, obj, doOverload);
}
-void SymbolTable::bindType(const string& name, api::Sort t, bool levelZero)
+void SymbolTable::bindType(const string& name, api::Sort t)
{
- d_implementation->bindType(name, t, levelZero);
+ d_implementation->bindType(name, t);
}
void SymbolTable::bindType(const string& name,
const vector<api::Sort>& params,
- api::Sort t,
- bool levelZero)
+ api::Sort t)
{
- d_implementation->bindType(name, params, t, levelZero);
+ d_implementation->bindType(name, params, t);
}
bool SymbolTable::isBound(const string& name) const
*
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
* @param doOverload set if the binding can overload the function name.
*
* Returns false if the binding was invalid.
*/
bool bind(const std::string& name,
api::Term obj,
- bool levelZero = false,
bool doOverload = false);
/**
*
* @param name an identifier
* @param t the type to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
*/
- void bindType(const std::string& name, api::Sort t, bool levelZero = false);
+ void bindType(const std::string& name, api::Sort t);
/**
* Bind a type to a name in the current scope. If <code>name</code>
* @param name an identifier
* @param params the parameters to the type
* @param t the type to bind to <code>name</code>
- * @param levelZero true to bind it globally (default is to bind it
- * locally within the current scope)
*/
void bindType(const std::string& name,
const std::vector<api::Sort>& params,
- api::Sort t,
- bool levelZero = false);
+ api::Sort t);
/**
* Check whether a name is bound to an expression with bind().
api::Term Parser::bindVar(const std::string& name,
const api::Sort& type,
- bool levelZero,
bool doOverload)
{
- bool globalDecls = d_symman->getGlobalDeclarations();
Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
api::Term expr = d_solver->mkConst(type, name);
- defineVar(name, expr, globalDecls || levelZero, doOverload);
+ defineVar(name, expr, doOverload);
return expr;
}
std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
const api::Sort& type,
- bool levelZero,
bool doOverload)
{
std::vector<api::Term> vars;
for (unsigned i = 0; i < names.size(); ++i) {
- vars.push_back(bindVar(names[i], type, levelZero, doOverload));
+ vars.push_back(bindVar(names[i], type, doOverload));
}
return vars;
}
void Parser::defineVar(const std::string& name,
const api::Term& val,
- bool levelZero,
bool doOverload)
{
Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
- if (!d_symtab->bind(name, val, levelZero, doOverload))
+ if (!d_symtab->bind(name, val, doOverload))
{
std::stringstream ss;
ss << "Cannot bind " << name << " to symbol of type " << val.getSort();
void Parser::defineType(const std::string& name,
const api::Sort& type,
- bool levelZero,
bool skipExisting)
{
if (skipExisting && isDeclared(name, SYM_SORT))
Assert(d_symtab->lookupType(name) == type);
return;
}
- d_symtab->bindType(name, type, levelZero);
+ d_symtab->bindType(name, type);
Assert(isDeclared(name, SYM_SORT));
}
void Parser::defineType(const std::string& name,
const std::vector<api::Sort>& params,
- const api::Sort& type,
- bool levelZero)
+ const api::Sort& type)
{
- d_symtab->bindType(name, params, type, levelZero);
+ d_symtab->bindType(name, params, type);
Assert(isDeclared(name, SYM_SORT));
}
api::Sort Parser::mkSort(const std::string& name)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- bool globalDecls = d_symman->getGlobalDeclarations();
api::Sort type = d_solver->mkUninterpretedSort(name);
- defineType(name, type, globalDecls);
+ defineType(name, type);
return type;
}
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- bool globalDecls = d_symman->getGlobalDeclarations();
api::Sort type = d_solver->mkSortConstructorSort(name, arity);
- defineType(name, vector<api::Sort>(arity), type, globalDecls);
+ defineType(name, vector<api::Sort>(arity), type);
return type;
}
d_solver->mkDatatypeSorts(datatypes, d_unresolved);
Assert(datatypes.size() == types.size());
- bool globalDecls = d_symman->getGlobalDeclarations();
for (unsigned i = 0; i < datatypes.size(); ++i) {
api::Sort t = types[i];
if (t.isParametricDatatype())
{
std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts();
- defineType(name, paramTypes, t, globalDecls);
+ defineType(name, paramTypes, t);
}
else
{
- defineType(name, t, globalDecls);
+ defineType(name, t);
}
std::unordered_set< std::string > consNames;
std::unordered_set< std::string > selNames;
if(!doOverload) {
checkDeclaration(constructorName, CHECK_UNDECLARED);
}
- defineVar(constructorName, constructor, globalDecls, doOverload);
+ defineVar(constructorName, constructor, doOverload);
consNames.insert(constructorName);
}else{
throw ParserException(constructorName + " already declared in this datatype");
{
checkDeclaration(testerName, CHECK_UNDECLARED);
}
- defineVar(testerName, tester, globalDecls, doOverload);
+ defineVar(testerName, tester, doOverload);
}
for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
{
if(!doOverload) {
checkDeclaration(selectorName, CHECK_UNDECLARED);
}
- defineVar(selectorName, selector, globalDecls, doOverload);
+ defineVar(selectorName, selector, doOverload);
selNames.insert(selectorName);
}else{
throw ParserException(selectorName + " already declared in this datatype");
void checkFunctionLike(api::Term fun);
/** Create a new cvc5 variable expression of the given type.
- *
- * It is inserted at context level zero in the symbol table if levelZero is
- * true, or if we are using global declarations.
*
* If a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
*/
api::Term bindVar(const std::string& name,
const api::Sort& type,
- bool levelZero = false,
bool doOverload = false);
/**
* Create a set of new cvc5 variable expressions of the given type.
*
- * It is inserted at context level zero in the symbol table if levelZero is
- * true, or if we are using global declarations.
- *
* For each name, if a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
* else if doOverload is false, the existing expression is shadowed by the
*/
std::vector<api::Term> bindVars(const std::vector<std::string> names,
const api::Sort& type,
- bool levelZero = false,
bool doOverload = false);
/**
const api::Sort& type);
/** Create a new variable definition (e.g., from a let binding).
- * levelZero is set if the binding must be done at level 0.
* If a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
* else if doOverload is false, the existing expression is shadowed by the
*/
void defineVar(const std::string& name,
const api::Term& val,
- bool levelZero = false,
bool doOverload = false);
/**
*
* @param name The name of the type
* @param type The type that should be associated with the name
- * @param levelZero If true, the type definition is considered global and
- * cannot be removed by popping the user context
* @param skipExisting If true, the type definition is ignored if the same
* symbol has already been defined. It is assumed that
* the definition is the exact same as the existing one.
*/
void defineType(const std::string& name,
const api::Sort& type,
- bool levelZero = false,
bool skipExisting = false);
/**
* @param name The name of the type
* @param params The type parameters
* @param type The type that should be associated with the name
- * @param levelZero If true, the type definition is considered global and
- * cannot be removed by poppoing the user context
*/
void defineType(const std::string& name,
const std::vector<api::Sort>& params,
- const api::Sort& type,
- bool levelZero = false);
+ const api::Sort& type);
/** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
void defineParameterizedType(const std::string& name,
else
{
api::Term func =
- PARSER_STATE->bindVar(name, t, false, true);
+ PARSER_STATE->bindVar(name, t, true);
cmd->reset(new DeclareFunctionCommand(name, func, t));
}
}
"version 2.0");
}
api::Term c =
- PARSER_STATE->bindVar(name, t, false, true);
+ PARSER_STATE->bindVar(name, t, true);
cmd->reset(new DeclareFunctionCommand(name, c, t)); }
/* get model */
}
// allow overloading
api::Term func =
- PARSER_STATE->bindVar(name, tt, false, true);
+ PARSER_STATE->bindVar(name, tt, true);
seq->addCommand(new DeclareFunctionCommand(name, func, tt));
sorts.clear();
}
}
// allow overloading
api::Term func =
- PARSER_STATE->bindVar(name, t, false, true);
+ PARSER_STATE->bindVar(name, t, true);
seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
void Smt2::addCoreSymbols()
{
- defineType("Bool", d_solver->getBooleanSort(), true, true);
- defineVar("true", d_solver->mkTrue(), true, true);
- defineVar("false", d_solver->mkFalse(), true, true);
+ defineType("Bool", d_solver->getBooleanSort(), true);
+ defineVar("true", d_solver->mkTrue(), true);
+ defineVar("false", d_solver->mkFalse(), true);
addOperator(api::AND, "and");
addOperator(api::DISTINCT, "distinct");
addOperator(api::EQUAL, "=");
api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
// allow overloading
- return bindVar(fname, ft, false, true);
+ return bindVar(fname, ft, true);
}
void Smt2::pushDefineFunRecScope(
if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
if(d_logic.areIntegersUsed()) {
- defineType("Int", d_solver->getIntegerSort(), true, true);
+ defineType("Int", d_solver->getIntegerSort(), true);
addArithmeticOperators();
if (!strictModeEnabled() || !d_logic.isLinear())
{
if (d_logic.areRealsUsed())
{
- defineType("Real", d_solver->getRealSort(), true, true);
+ defineType("Real", d_solver->getRealSort(), true);
addArithmeticOperators();
addOperator(api::DIVISION, "/");
if (!strictModeEnabled())
if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
const std::vector<api::Sort> types;
- defineType("Tuple", d_solver->mkTupleSort(types), true, true);
+ defineType("Tuple", d_solver->mkTupleSort(types), true);
addDatatypesOperators();
}
addOperator(api::TABLE_PRODUCT, "table.product");
}
if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
- defineType("String", d_solver->getStringSort(), true, true);
- defineType("RegLan", d_solver->getRegExpSort(), true, true);
- defineType("Int", d_solver->getIntegerSort(), true, true);
+ defineType("String", d_solver->getStringSort(), true);
+ defineType("RegLan", d_solver->getRegExpSort(), true);
+ defineType("Int", d_solver->getIntegerSort(), true);
defineVar("re.none", d_solver->mkRegexpNone());
defineVar("re.allchar", d_solver->mkRegexpAllchar());
}
if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
- defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true);
- defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true);
- defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true);
- defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true);
- defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true);
+ defineType("RoundingMode", d_solver->getRoundingModeSort(), true);
+ defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true);
+ defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true);
+ defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true);
+ defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true);
defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
defineVar("roundNearestTiesToEven",
addSepOperators();
}
+ // builtin symbols of the logic are declared at context level zero, hence
+ // we push the outermost scope here
+ pushScope(true);
+
std::string logic = sygus() ? d_logic.getLogicString() : name;
if (!fromCommand)
{
// if it has a kind, it's a builtin one and this function should not have been
// called
Assert(p.d_kind == api::NULL_EXPR);
- if (isDeclared(p.d_name))
- { // already appeared
- expr = getVariable(p.d_name);
- }
- else
+ expr = isTptpDeclared(p.d_name);
+ if (expr.isNull())
{
api::Sort t =
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
- expr = bindVar(p.d_name, t, true); // must define at level zero
+ expr = bindVar(p.d_name, t); // must define at level zero
+ d_auxSymbolTable[p.d_name] = expr;
preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
}
return expr;
}
+api::Term Tptp::isTptpDeclared(const std::string& name)
+{
+ if (isDeclared(name))
+ { // already appeared
+ return getVariable(name);
+ }
+ std::unordered_map<std::string, api::Term>::iterator it =
+ d_auxSymbolTable.find(name);
+ if (it != d_auxSymbolTable.end())
+ {
+ return it->second;
+ }
+ // otherwise null
+ return api::Term();
+}
+
api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
{
if (Debug.isOn("parser"))
if (p.d_kind == api::NULL_EXPR)
{
// A non-built-in function application, get the expression
- api::Term v;
- if (isDeclared(p.d_name))
- { // already appeared
- v = getVariable(p.d_name);
- }
- else
+ api::Term v = isTptpDeclared(p.d_name);
+ if (v.isNull())
{
std::vector<api::Sort> sorts(args.size(), d_unsorted);
api::Sort t =
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
t = d_solver->mkFunctionSort(sorts, t);
- v = bindVar(p.d_name, t, true); // must define at level zero
+ v = bindVar(p.d_name, t); // must define at level zero
+ d_auxSymbolTable[p.d_name] = v;
preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
}
// args might be rationals, in which case we need to create
private:
void addArithmeticOperators();
+ /** is the name declared, if so, return the term for that name */
+ api::Term isTptpDeclared(const std::string& name);
// In CNF variable are implicitly binded
// d_freevar collect them
// The set of expression that already have a bridge
std::unordered_set<api::Term> d_r_converted;
std::unordered_map<std::string, api::Term> d_distinct_objects;
+ /**
+ * TPTP automatically declares symbols as they are parsed inline. This
+ * requires using an auxiliary symbol table for such symbols. This must be
+ * independent of the main symbol table which is aware of quantifier
+ * scopes.
+ */
+ std::unordered_map<std::string, api::Term> d_auxSymbolTable;
std::vector< pANTLR3_INPUT_STREAM > d_in_created;
d_context->push();
ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
- map.insertAtContextLevelZero(23, 317);
map.insert(1, 45);
ASSERT_TRUE(
- elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}}));
map.insert(23, 324);
ASSERT_TRUE(
}
ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
d_context->pop();
}
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
d_context->pop();
}
- ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
}
TEST_F(TestContextBlackCDHashMap, simple_sequence_fewer_finds)
ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
- map.insertAtContextLevelZero(23, 317);
-
ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 317),
- "insertAtContextLevelZero");
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 472),
- "insertAtContextLevelZero");
map.insert(23, 472);
ASSERT_TRUE(
ASSERT_TRUE(
elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
- "insertAtContextLevelZero");
map.insert(23, 1024);
ASSERT_TRUE(
d_context->pop();
}
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
- "insertAtContextLevelZero");
map.insert(23, 477);
ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
d_context->pop();
}
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), "insertAtContextLevelZero");
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
}
} // namespace test
} // namespace cvc5
projects / cvc5.git / commitdiff