assumption_context.hpp 文件参考

AssumptionContext class with scoped push/pop management. 更多...

#include "assumption.hpp"
#include "property_store.hpp"
#include "relation_store.hpp"
#include "result.hpp"
#include <vector>
#include <string>
#include <stdexcept>
#include <unordered_set>
#include <optional>
#include <sstream>
#include <type_traits>
#include <initializer_list>
#include <variant>

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

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

浏览该文件的源代码.

类
class	LMCAS::AssumptionDecl
	Declaration of an assumption to apply within a with_assumptions block. 更多...
struct	LMCAS::AssumptionDecl::DomainDeclaration
struct	LMCAS::AssumptionDecl::SignDeclaration

命名空间
namespace	LMCAS
namespace	LMCAS::detail
	多元 Hensel 提升（单变量步）

类型定义
using	LMCAS::AssumptionTriboolResult = Result<Tribool>
using	LMCAS::AssumptionVoidResult = Result<void>

函数
class	LMCAS::__attribute__ ((visibility("default"))) AssumptionContext
	Scoped assumption context with push/pop management.
AssumptionVoidResult	LMCAS::apply_assumption_decl_checked (AssumptionContext &ctx, const AssumptionDecl &decl)
template<typename F>
auto	LMCAS::with_assumptions (AssumptionContext &ctx, const std::vector< AssumptionDecl > &decls, F &&callable) -> std::enable_if_t< std::is_void_v< decltype(callable())>, AssumptionVoidResult >
template<typename F>
auto	LMCAS::with_assumptions (AssumptionContext &ctx, const std::vector< AssumptionDecl > &decls, F &&callable) -> std::enable_if_t<!std::is_void_v< decltype(callable())>, Result< decltype(callable())> >
	Execute a callable within a temporary assumption scope.
template<typename F>
auto	LMCAS::with_assumptions (AssumptionContext &ctx, std::initializer_list< AssumptionDecl > decls, F &&callable) -> decltype(with_assumptions(ctx, std::vector< AssumptionDecl >(decls), std::forward< F >(callable)))

详细描述

AssumptionContext class with scoped push/pop management.

Provides a scope stack where each scope has its own PropertyStore and RelationStore. Queries read through from the top scope down to the root, with child scope declarations shadowing parent declarations.

在文件 assumption_context.hpp 中定义.

---

类说明

LMCAS::AssumptionDecl::DomainDeclaration

struct LMCAS::AssumptionDecl::DomainDeclaration

在文件 assumption_context.hpp 第 428 行定义.

LMCAS::AssumptionDecl::DomainDeclaration 的协作图:

类成员
Domain	domain
string	symbol

LMCAS::AssumptionDecl::SignDeclaration

struct LMCAS::AssumptionDecl::SignDeclaration

在文件 assumption_context.hpp 第 433 行定义.

LMCAS::AssumptionDecl::SignDeclaration 的协作图:

类成员
Sign	sign
string	symbol