relation_store.hpp 文件参考

RelationStore class for storing relational constraints between symbolic expressions. 更多...

#include <vector>
#include <string>
#include <memory>
#include "symbolic.hpp"
#include "assumption.hpp"
#include "result.hpp"
#include <cstdint>
#include <array>
#include <cstddef>
#include <optional>

relation_store.hpp 的引用(Include)关系图:

此图展示该文件被哪些文件直接或间接地引用了:

浏览该文件的源代码.

类
struct	LMCAS::Relation
	A stored relational constraint between two symbolic expressions. 更多...

命名空间
namespace	LMCAS

类型定义
using	LMCAS::RelationStoreResult = Result<void>

函数
class	LMCAS::__attribute__ ((visibility("default"))) AssumptionContext
	Scoped assumption context with push/pop management.

详细描述

RelationStore class for storing relational constraints between symbolic expressions.

Stores inequality relations (GT, LT, GEQ, LEQ, NEQ) between SymbolicExpr instances. When a simple "variable op 0" pattern is detected, the corresponding sign property is automatically propagated to the PropertyStore.

在文件 relation_store.hpp 中定义.

---

类说明

LMCAS::Relation

struct LMCAS::Relation

A stored relational constraint between two symbolic expressions.

在文件 relation_store.hpp 第 32 行定义.

LMCAS::Relation 的协作图:

类成员
SymbolicExpr	lhs	Left-hand side expression
RelationOp	op	Relational operator (GT, LT, GEQ, LEQ, NEQ, EQ)
SymbolicExpr	rhs	Right-hand side expression