PV2 PCSatgenerates an SMT problem from a pfwCSP spec, requires an external solver

Satisfiability checking tool for pfwCSP based on stratified Counterexample-guided Inductive Synthesis (CEGIS).

Application domain/field

Type of tool

Satisfiability checker (for pfwCSP)

Expected input

Format:

Expected output

sat, unsat or unknown?

Internals

Uses Z3 pfwCSP: new class of predicate Constraint Satisfaction Problems. This allows constraints that are arbitrary (i.e. possibly non-Horn) clauses modulo first-order theories over predicate variables that can be functional predicates, well-founded predicates or ordinary predicates. This is a generalization over Constrained Horn Clauses.

Comments

Note: the authors sometimes call PCSat a (second-order) constraint solver
CHC

Links

Repository (contains MuVal and PCSat): https://github.com/hiroshi-unno/coar

Last commit date

11 May 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_35 (CAV '21)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.