-
4 votesanswersviews
寻找一个好的开源电子邮件服务器[关闭]
我正在开发一个项目，要求我编写自己的电子邮件服务器 . 我想知道是否有人对使用.NET编写的开源电子邮件服务器有任何好的建议，我可以将其作为起点 . 如果已经内置了用于发送短信的内容，则奖励积分 . -
0 votesanswersviews
点网的开源替代[重复]
可能重复：.net开源和运行平台选择 任何人都可以告诉我哪个是.NET的完美开源替代品 . -
15 votesanswersviews
Typemock Isolator的开源/免费替代品
是否有Typemock Isolator .NET的F / OSS替代品？ -
4 votesanswersviews
示例开源WPF触摸应用程序？
我正在寻找一些专门为触摸设计的WPF应用程序 . 他们最好是开源的 . 我真的不关心应用程序功能，我只想获得一些我将要编写的Win7 WPF触控应用程序的设计思路 . 我想看看WPF touch可以做些什么 . 谢谢 -
7 votesanswersviews
在位向量算法的决策过程中使用术语重写
我正在研究一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于某些决策程序（例如基于钻头爆破的程序）的先前步骤是有用的 . 术语重写可以完全解决问题，或者产生更简单的等效问题，因此两者的组合可以导致相当大的加速 . 我知道许多SMT求解器实现了这种策略（例如Boolector，Beaver，Alt-Ergo或Z3），但是很难找到详细描述这些重写步骤的论文/技术报告/等 . 一... -
0 votesanswersviews
寻找开源WCF代理生成器[关闭]
是否有任何WCF的开源代理生成器？ Visual Studio内置的那个很糟糕，我想要一个更好或者可以修改它的一个 . 例如，我真的需要OnXxxChanging和OnXxxChanged部分方法 . -
0 votesanswersviews
可以通过命名表达式实现软约束吗？
我想知道是否可以使用命名表达式来实现软约束，而无需明确使用手动“跟踪”变量 . 在消息Soft/Hard constraints in Z3中，Leonardo解释了如何使用辅助布尔值以手动方式实现软约束 . 在以下消息：z3 behaviour changing on request for unsat core中，莱昂纳多说命名表达式基本上被视为模型查找的含义 . 使用上面第一条消... -
0 votesanswersviews
Python相当于Z3_API Z3_benchmark_to_smtlib_string的第7个参数
我们目前在python上使用z3来检查程序跟踪的可行性 . 基于跟踪我们创建z3公式和断言，我们的下一个方法是使用SMT2作为中间语言通过Z3_benchmark_to_smtlib_string将这些断言提供给iZ3和smtinterpol . 一个小例子：x = Int（'x'）y = Int（'y'） s = Solver() # Assertions s.assert_and_track... -
2 votesanswersviews
订单理论的定制理论求解器？
我的程序，反应有限状态系统的有限合成器，产生SMT查询以注释（未解释的）系统的产品自动机和规范 . 本质上，它是一个使用未解释函数检查的模型 . 如果注释存在=> Z3找到的模型满足规范 . 查询包含： 数据类型（用于编码系统和规范自动机的状态） =（更大），>（严格地）（指定自动机系统*规范的状态的排序函数，用于搜索具有不良状态的套索）或换句话说，对该自动机的状态的排序， ... -
1 votesanswersviews
Z3 - check-sat-using的参数
抱歉，如果这是一个愚蠢的问题 - 我对使用Z3（以及一般的SMT）很陌生 - 但我有点难过 . 假设我有两个SMT2输入语言文件，略有不同，总结如下： (define-fun T ((i Int)) Bool (... - too long to paste completely, but does define $prop) (assert (T 0)) (declare-fun assum1 ... -
0 votesanswersviews
使用C，使用Z3_parse_smtlib2_string在Z3中获取Unsat Core
我需要使用 Z3_parse_smtlib2_string 使用C API将一些SMTLIB字符串解析为Z3，并使用Z3 C API来查找不满核心 . 我知道还有其他方法可以找到更容易且不那么繁琐的here和here描述的不饱和核心，但我真的希望能够仅使用从字符串解析到Z3的数据结构来做到这一点 . 原因是我试图使用Z3自动化某些东西 . 很明显，如果我将这个SMTLIB程序传递给Z3，那就是UN... -
3 votesanswersviews
SMT求解器中约束强化的效率
解决优化问题的一种方法是使用SMT求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到命题不再可满足为止 . 例如，http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf讨论了这种方法 . 这种方法有效吗... -
0 votesanswersviews
跟踪非线性实数算术断言使用含义与：命名机制给出不同的答案
在尝试解决大型非线性实际算术问题时，我使用答案文字和显式含义来跟踪每个断言，如其他帖子中所建议的那样 . 它应该等同于使用SMT2格式的（！（...）：named p1）语法 . 但是，似乎两种方法在内部都有不同的处理方式 . 以下SMT2代码给出了UNKNOWN结果，解释为“（不完整（理论算术））”： (set-option :print-success false) (set-option ... -
0 votesanswersviews
具有前提的非线性实数算法的可解性
一个小例子表明，当NRA断言由与（sat p1 ... pn）检查相关的前提pi标记时，非线性实数算术（NRA）求解器受到阻碍 . 以下SMT2示例返回具有正确模型的SAT： (declare-const p1 Bool) (declare-const p2 Bool) (declare-const p3 Bool) (declare-const p4 Bool) (declare-const ... -
2 votesanswersviews
支持在SAT时获取模型（类似于CVC4中的--dump-models）
在开源之后我刚开始玩Z3求解器 . 我目前使用Z3作为命令行黑盒工具，如果模型是SAT，我希望它可以转储反例 . 我主要通过QF_NIA和QF_LIA查询 . 我注意到在Z3中不存在等同于CVC4s --dump-models的选项 . 我可以在SMT2lib文件中写入（check-sat）之后写入（dump-model），但如果公式实际上不满意则会出错 . SMT2 lib的语言虽然看起来很低调... -
0 votesanswersviews
Z3 Java API - 获得不满的核心
我试图弄清楚如何使用Java API for Z3获得不饱和核心 . 我们的场景如下（代码在下面，在rise4fun中工作）： 我们以编程方式创建SMT2输入 输入包含函数定义，数据类型声明和断言 我们使用parseSMTLIB2String API解析它 我们确保上下文和解算器具有unsat_core - > true Z3为提供的输入返回UNSAT，这是正确的 ... -
3 votesanswersviews
Z3：非线性算术和量词 - 错误的结果？
这是一个生成“sat”的Z3查询 . （我正在运行Z3版本4.8.0，结果在rise4fun Web界面中是相同的 . ） (assert (forall ((x Real)) (exists ((y Real)) (and (<= 0.0 y) (<= y 1.0) (<= x (* y y)))))) (check-sat) ... -
3 votesanswersviews
列表的理论是可判定的吗？
我想知道列表的z3理论是否可判定？看起来我们只能证明事实是不完整但不能使用理论，所以我很好奇它是否真的可以判断 . 谢谢你的帮助 . -
3 votesanswersviews
使用理论插件和解算器
Z3的最新版本将 Z3_context 和 Z3_solver 的概念分离 . API主要反映了这些变化;例如 push 在上下文中被弃用，并被重新指定为将求解器作为额外参数 . 然而，理论界面尚未更新 . 理论仍然是从上下文创建的，据我所知，从未明确地附加到求解器上 . 人们可能会认为从上下文创建的理论将始终附加到从上下文创建的所有求解器，但从我们的经验来看，似乎并非如此 . 相反，用户定义的... -
1 votesanswersviews
以正确的策略加速z3-solver
我创建了大约20k的约束，在我的机器上解决它们大约需要3分钟 . 我有不同类型的约束，下面我举例并解释它们 . 我将断言上传到http://filebin.ca/vKcV1gvuGG3 . 我对解决更大的约束系统感兴趣，因此我想加快这个过程 . 我想问你是否有关于如何更快地解决问题的建议，例如：通过使用适当的策略 . 从策略教程我知道战术，但我似乎没有通过应用战术得到积极的差异...... li ... -
1 votesanswersviews
z3实存的存在论
Z3是否决定了非线性实数算术的存在性片段？也就是说，我可以将它作为一个决策程序用于测试带有和x的量词无关公式是否具有超过实数的解决方案？ -
0 votesanswersviews
在Z3中 Build 自定义理论
这个问题是对以下问题的跟进 . Procedural Attachment in Z3 我有一个谓词（我在这种情况下使用“更重”的名称）超过两个整数，我需要使用自定义算法进行评估 . 我编写了以下代码来完成它 . 但我发现传递给函数CMTh_reduce_app（）的参数不是实际的整数，而是整数类型的consts . 我需要的是2个整数，这样我就可以评估谓词并返回结果（现在函数CMTh_reduc... -
1 votesanswersviews
没有元组（declare-datatypes）？
我用SMT-LIB的Z3方言写了一个大型的库 . 不幸的是，我使用 (declare-datatypes) 来创建元组意味着我无法按照我的意愿将逻辑设置为 QF_AUFBV . 这有使我的脚本更慢（有时超时）的副作用比我以编程方式手动创建公式并使用 QF_ABV 解决 . 因此，我想从我的脚本中删除 (declare-datatypes) . 大多数数据类型可以编码为位向量 . 但是，库中最重... -
1 votesanswersviews
随机可满足模理论
有人知道Z3是否支持SSMT（即随机量词）或是否有计划添加它？ Reference paper -
6 votesanswersviews
用于位向量算术的SMT求解器
我正在计划一些C代码的符号执行实验，使用现成的SMT求解器，并想知道使用哪个求解器;看着例如SMT比赛的参赛者，只采用开源系统，将其缩小为Beaver，Boolector，CVC3，OpenSMT，Sateen，Sonolar，STP，Verit;这仍然是一个很长的名单 . 为了进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统只宣传处理一般整数算术的能力 . 原则上，前者对于C... -
3 votesanswersviews
Z3 / SMT：我什么时候应该选择push / pop来重置？
我使用Z3来解决符号 Actuator 产生的路径条件，它以深度优先顺序探索状态空间，与CUTE，DART或（可能）SAGE非常相似 . 我们正在尝试使用Z3的不同方法 . 在一个极端，我们将每个查询发送到Z3并立即（重置）它 . 另一方面，我们（推）每个额外的分支约束，并且（弹出）（pop）在回溯时正确削弱路径条件所需的最小值 . 问题是，在所有情况下，没有任何策略似乎比任何其他策略更好 . 推... -
2 votesanswersviews
将z3 C API ast（或解算器）对象转换为SMTLIB字符串
我正在玩z3和其他SMT求解器，并且想要检查其他求解器如boolector胜过z3的情况，反之亦然 . 为此，我需要一种方法将声明和断言转换为SMT-LIB2格式，而其他SMT求解器可以识别这种格式 . 例如，对于此示例 void print_as_smtlib2_string() { context c; expr x = c.int_const("x"); ... -
2 votesanswersviews
Z3位向量操作
如何使用'repeat'和'rotate_left'位向量操作？ 更一般地说，在哪里可以找到Z3使用的SMT2脚本格式的bitvector操作的详细文档？ 我发现的一切似乎只是去教程或破坏的链接：https://github.com/Z3Prover/z3/wiki/Documentationhttp://research.microsoft.com/en-us/um/redmond/projec... -
0 votesanswersviews
dReal SMT求解器反例
dReal SMT求解器是否会返回反例？我已经看到了以下示例： 生产环境 模型是真的，但我不知道如何生成反例 . 此外，dReach工具有一个--visualize选项，因此看起来dReal需要生成一些模型信息 . 但是，当我在.smt2文件上运行它时，我似乎找不到查看反例的方法 . -
1 votesanswersviews
在SMT中表达不关心的位向量
我想定义一个接受位向量的函数，如果某个位置的位满足某些值，则返回true . 例如：如果bitvector是1x00x01x，我需要返回true，其中x表示不关心 . 我目前的实施是： (define-fun function_i ((i (_ BitVec 8))) Bool (and true (= #b1 ((_ extract 1 1) i)) (=...