/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/test/ |
H A D | UnificationSpec.hs | 30 let (skolems, take n -> univars) 36 for (zip skolems univars) randomSwap 41 counterexample (show skolems) $ 45 (S.fromList $ mapMaybe tcGetTyVar_maybe skolems) 52 zip univars skolems <&> \(uni, skolem) ->
|
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/test/ |
H A D | UnificationSpec.hs | 30 let (skolems, take n -> univars) 36 for (zip skolems univars) randomSwap 41 counterexample (show skolems) $ 45 (S.fromList $ mapMaybe tcGetTyVar_maybe skolems) 52 zip univars skolems <&> \(uni, skolem) ->
|
/dports/math/cvc4/CVC4-1.7/test/unit/expr/ |
H A D | node_black.h | 40 std::vector<Node> skolems; in makeNSkolemNodes() local 45 return skolems; in makeNSkolemNodes() 665 const std::vector<Node> skolems = in testForEachOverNodeAsNodes() local 667 Node add = d_nodeManager->mkNode(kind::PLUS, skolems); in testForEachOverNodeAsNodes() 672 TS_ASSERT(children.size() == skolems.size() && in testForEachOverNodeAsNodes() 677 const std::vector<Node> skolems = in testForEachOverNodeAsTNodes() local 684 TS_ASSERT(children.size() == skolems.size() && in testForEachOverNodeAsTNodes() 689 const std::vector<Node> skolems = in testForEachOverTNodeAsNode() local 697 TS_ASSERT(children.size() == skolems.size() && in testForEachOverTNodeAsNode() 702 const std::vector<Node> skolems = in testForEachOverTNodeAsTNodes() local [all …]
|
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/Judgements/ |
H A D | Theta.hs | 85 mkSubst skolems a b = 91 skolems' = skolems S.\\ tyvars function 109 allEvidenceToSubst skolems ((a, b) : evs) = 110 let subst = mkSubst skolems a b 112 $ allEvidenceToSubst skolems
|
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/Judgements/ |
H A D | Theta.hs | 85 mkSubst skolems a b = 91 skolems' = skolems S.\\ tyvars function 109 allEvidenceToSubst skolems ((a, b) : evs) = 110 let subst = mkSubst skolems a b 112 $ allEvidenceToSubst skolems
|
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/ |
H A D | Machinery.hs | 97 let skolems = S.fromList function 106 { ts_skolems = skolems 247 skolems <- gets ts_skolems 248 case tryUnifyUnivarsButNotSkolems skolems goal inst of 265 skolems <- gets ts_skolems 266 case tryUnifyUnivarsButNotSkolems skolems goal inst of 287 skolems <- gets ts_skolems 289 case S.size $ vars S.\\ skolems of
|
H A D | Auto.hs | 20 skolems <- gets ts_skolems 25 traceMX "skolems" skolems
|
H A D | GHC.hs | 389 tryUnifyUnivarsButNotSkolems skolems goal inst = 391 (bool BindMe Skolem . flip S.member skolems)
|
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/ |
H A D | Machinery.hs | 97 let skolems = S.fromList function 106 { ts_skolems = skolems 247 skolems <- gets ts_skolems 248 case tryUnifyUnivarsButNotSkolems skolems goal inst of 265 skolems <- gets ts_skolems 266 case tryUnifyUnivarsButNotSkolems skolems goal inst of 287 skolems <- gets ts_skolems 289 case S.size $ vars S.\\ skolems of
|
H A D | Auto.hs | 20 skolems <- gets ts_skolems 25 traceMX "skolems" skolems
|
H A D | GHC.hs | 389 tryUnifyUnivarsButNotSkolems skolems goal inst = 391 (bool BindMe Skolem . flip S.member skolems)
|
/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | search_theorem_producer.h | 41 const ExprMap<bool>& skolems); 43 const ExprMap<bool>& skolems);
|
H A D | search_theorem_producer.cpp | 413 const ExprMap<bool>& skolems) in checkSoundNoSkolems() argument 419 CHECK_SOUND(skolems.count(e) == 0, in checkSoundNoSkolems() 423 checkSoundNoSkolems(*it, visited, skolems); in checkSoundNoSkolems() 425 checkSoundNoSkolems(e.getBody(), visited, skolems); in checkSoundNoSkolems() 431 const ExprMap<bool>& skolems) in checkSoundNoSkolems() argument 437 checkSoundNoSkolems(t.getExpr(), visited, skolems); in checkSoundNoSkolems() 443 checkSoundNoSkolems(*it, visited, skolems); in checkSoundNoSkolems() 468 ExprMap<bool> skolems; in eliminateSkolemAxioms() local 484 skolems[sk_var] = true; in eliminateSkolemAxioms() 489 checkSoundNoSkolems(tFalse, visited, skolems); in eliminateSkolemAxioms()
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | skolemize.cpp | 50 bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) in getSkolemConstants() argument 56 skolems.insert(skolems.end(), it->second.begin(), it->second.end()); in getSkolemConstants()
|
H A D | skolemize.h | 74 bool getSkolemConstants(Node q, std::vector<Node>& skolems);
|
H A D | conjecture_generator.cpp | 585 std::vector<Node> skolems; in check() local 586 d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); in check() 589 for (unsigned j = 0; j < skolems.size(); j++) in check() 591 TNode k = skolems[j]; in check() 599 for (unsigned k = 0; k < skolems.size(); k++) in check() 601 Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "") in check()
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/sets/jan28/ |
H A D | TalkingAboutSets.hs.fqout.3577minimized.smt2 | 8 ; skolems due to the "two sets not being equal" axiom.
|
/dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
H A D | bv_subtheory_algebraic.cpp | 860 std::vector<Node> skolems; in skolemize() local 867 skolems.push_back(sk); in skolemize() 874 skolems.push_back(sk); in skolemize() 878 for (int i = skolems.size() - 1; i >= 0; --i) { in skolemize() 879 skolem_nb << skolems[i]; in skolemize() 882 Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb; in skolemize()
|
H A D | abstraction.cpp | 287 vector<Node>& skolems = d_signatureSkolems[bitwidth]; in getSignatureSkolem() local 290 Assert(skolems.size() + 1 >= index); in getSignatureSkolem() 291 if (skolems.size() == index) in getSignatureSkolem() 295 skolems.push_back(nm->mkSkolem(os.str(), in getSignatureSkolem() 300 return skolems[index]; in getSignatureSkolem()
|
/dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
H A D | theory_uf.cpp | 760 std::vector< Node > skolems; in getExtensionalityDeq() local 766 skolems.push_back( k ); in getExtensionalityDeq() 779 children.insert( children.end(), skolems.begin(), skolems.end() ); in getExtensionalityDeq()
|
/dports/textproc/py-rdflib/rdflib-5.0.0/rdflib/ |
H A D | term.py | 72 skolems = {} variable 309 if bnode_id in skolems: 310 return skolems[bnode_id] 313 skolems[bnode_id] = retval
|
/dports/lang/purescript/purescript-0.14.5/src/Language/PureScript/TypeChecker/Entailment/ |
H A D | Coercible.hs | 387 go (ConstrainedType sa Constraint{..} ty) | s1 `S.notMember` foldMap skolems constraintArgs = 464 skolems :: SourceType -> S.Set Int 465 skolems = everythingOnTypes (<>) go where function
|
/dports/math/cvc4/CVC4-1.7/src/options/ |
H A D | datatypes_options.toml | 41 help = "introduce reference skolems for shorter explanations"
|
/dports/math/vampire/vampire-4.5.1/Shell/ |
H A D | NewCNF.cpp | 1243 Stack<Formula*> skolems; in toClauses() local 1254 skolems.push(f); in toClauses() 1265 Formula* skolem = skolems.pop(); in toClauses()
|
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/ |
H A D | ChangeLog.md | 1366 - Discover skolems in the hypothesis, not just goal
|